chore: fix typos

doc/tour.md

@@ -60,7 +60,7 @@ end BasicFunctions
 
 ```lean
 -- Lean has first-class functions.
--- `twice` takes two argumes `f` and `a` where
+-- `twice` takes two arguments `f` and `a` where
 -- `f` is a function from natural numbers to natural numbers, and
 -- `a` is a natural number.
 def twice (f : Nat → Nat) (a : Nat) :=

doc/typeobjs.md

@@ -114,7 +114,7 @@ constant α : Type _
 #check α
 ```
 
-Several Lean 3 users use the shorhand `Type*` for `Type _`. The `Type*` notation is not builtin in Lean 4, but you can be easily define it using a `macro`.
+Several Lean 3 users use the shorhand `Type*` for `Type _`. The `Type*` notation is not builtin in Lean 4, but you can easily define it using a `macro`.
 ```lean
 macro "Type*" : term => `(Type _)
 

src/Init/Coe.lean

@@ -15,7 +15,7 @@ class Coe (α : Sort u) (β : Sort v) where
 class CoeTC (α : Sort u) (β : Sort v) where
   coe : α → β
 
-/- Expensive coercion that can only appear at the beggining of a sequence of coercions. -/
+/- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/
 class CoeHead (α : Sort u) (β : Sort v) where
   coe : α → β
 
@@ -115,7 +115,7 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
 /-
   Remark: one may question why we use `OfNat α` instead of `Coe Nat α`.
   Reason: `OfNat` is for implementing polymorphic numeric literals, and we may
-  want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
+  want to have numeric literals for a type α and **no** coercion from `Nat` to `α`. -/
 instance hasOfNatOfCoe [Coe α β] [OfNat α n] : OfNat β n where
   ofNat := coe (OfNat.ofNat n : α)