diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index d6154d0306..2c32090564 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -630,7 +630,7 @@ tedious steps. Here is a very simple example.
 
 Lean supports _dependent functions_. In type theory, they are also called dependent product types or Pi-types.
 The idea is quite simple, suppose we have a type =A : Type=, and a family of types =B : A → Type= which assigns to each =a : A= a type =B a=. So a dependent function is a function whose range varies depending on its arguments.
-In Lean, the dependent functions is written as =forall a : A, B a=,
+In Lean, a dependent function is written as =forall a : A, B a=,
 =Pi a : A, B a=, =∀ x : A, B a=, or =Π x : A, B a=. We usually use
 =forall= and =∀= for propositions, and =Pi= and =Π= for everything
 else. In the previous examples, we have seen many examples of
@@ -640,7 +640,7 @@ equality are all dependent functions.
 The universal quantifier is just a dependent function.
 In Lean, if we have a family of types =B : A → Prop=,
 then =∀ x : A, B a= has type =Prop=.
-This features complicates the Lean set-theoretic model, but it
+This feature complicates the Lean set-theoretic model, but it
 improves usability.
 Several theorem provers have a =forall elimination= (aka
 instantiation) proof rule.