doc: fix typos/indentation

src/Init/Data/Nat/Basic.lean

@@ -182,7 +182,7 @@ protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   Nat.mul_comm n 1 ▸ Nat.mul_one n
 
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
-  induction n generalizing m k with
+  induction n with
   | zero      => repeat rw [Nat.zero_mul]
   | succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
 

src/Lean/Elab/Print.lean

@@ -83,7 +83,7 @@ private def printId (id : Syntax) : CommandElabM Unit := do
 
 @[builtin_command_elab «print»] def elabPrint : CommandElab
   | `(#print%$tk $id:ident) => withRef tk <| printId id
-  | `(#print%$tk $s:str) => logInfoAt tk s.getString
+  | `(#print%$tk $s:str)    => logInfoAt tk s.getString
   | _                       => throwError "invalid #print command"
 
 namespace CollectAxioms

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -72,7 +72,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
     throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
-   replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
+  replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
 
 private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
   TacticM Unit := do
@@ -94,23 +94,23 @@ private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i
 @[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure ()
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
-   let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
-   selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
+  let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
+  selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
-   let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
-   selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
+  let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
+  selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
-   match stx with
-   | `(conv| arg $[@%$tk?]? $i:num) =>
-      let i := i.getNat
-      if i == 0 then
-        throwError "invalid 'arg' conv tactic, index must be greater than 0"
-      let i := i - 1
-      let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
-      selectIdx "arg" mvarIds i
-   | _ => throwUnsupportedSyntax
+  match stx with
+  | `(conv| arg $[@%$tk?]? $i:num) =>
+    let i := i.getNat
+    if i == 0 then
+      throwError "invalid 'arg' conv tactic, index must be greater than 0"
+    let i := i - 1
+    let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
+    selectIdx "arg" mvarIds i
+  | _ => throwUnsupportedSyntax
 
 def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) := do
   match lhs with
@@ -141,35 +141,35 @@ def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId)
   | _ => return none
 
 private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :=
-   mvarId.withContext do
-     let (lhs, rhs) ← getLhsRhsCore mvarId
-     let lhs := (← instantiateMVars lhs).cleanupAnnotations
-     if let .forallE n d b bi := lhs then
-       let u ← getLevel d
-       let p : Expr := .lam n d b bi
-       let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
-       let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
-         let pa := b.instantiate1 a
-         let (qa, mvarNew) ← mkConvGoalFor pa
-         let q ← mkLambdaFVars #[a] qa
-         let h ← mkLambdaFVars #[a] mvarNew
-         let rhs' ← mkForallFVars #[a] qa
-         unless (← isDefEqGuarded rhs rhs') do
-           throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
-         return (q, h, mvarNew)
-       let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
-       mvarId.assign proof
-       return mvarNew.mvarId!
-     else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
-       return mvarId
-     else
-       let lhsType ← whnfD (← inferType lhs)
-       unless lhsType.isForall do
-         throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
-       let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
-       let userNames := if let some userName := userName? then [userName] else []
-       let (_, mvarId) ← mvarId.introN 1 userNames
-       markAsConvGoal mvarId
+  mvarId.withContext do
+    let (lhs, rhs) ← getLhsRhsCore mvarId
+    let lhs := (← instantiateMVars lhs).cleanupAnnotations
+    if let .forallE n d b bi := lhs then
+      let u ← getLevel d
+      let p : Expr := .lam n d b bi
+      let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
+      let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
+        let pa := b.instantiate1 a
+        let (qa, mvarNew) ← mkConvGoalFor pa
+        let q ← mkLambdaFVars #[a] qa
+        let h ← mkLambdaFVars #[a] mvarNew
+        let rhs' ← mkForallFVars #[a] qa
+        unless (← isDefEqGuarded rhs rhs') do
+          throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+        return (q, h, mvarNew)
+      let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
+      mvarId.assign proof
+      return mvarNew.mvarId!
+    else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
+      return mvarId
+    else
+      let lhsType ← whnfD (← inferType lhs)
+      unless lhsType.isForall do
+        throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
+      let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
+      let userNames := if let some userName := userName? then [userName] else []
+      let (_, mvarId) ← mvarId.introN 1 userNames
+      markAsConvGoal mvarId
 
 private def ext (userName? : Option Name) : TacticM Unit := do
   replaceMainGoal [← extCore (← getMainGoal) userName?]

src/Lean/Meta/AppBuilder.lean

@@ -337,7 +337,7 @@ def mkAppOptM (constName : Name) (xs : Array (Option Expr)) : MetaM Expr := do
     let (f, fType) ← mkFun constName
     mkAppOptMAux f xs 0 #[] 0 #[] fType
 
-/-- Similar to `mkAppOptM`, but takes an `Expr` instead of a constant name -/
+/-- Similar to `mkAppOptM`, but takes an `Expr` instead of a constant name. -/
 def mkAppOptM' (f : Expr) (xs : Array (Option Expr)) : MetaM Expr := do
   let fType ← inferType f
   withAppBuilderTrace f xs do withNewMCtxDepth do
@@ -396,7 +396,7 @@ def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=
   mkAppOptM ``Pure.pure #[monad, none, none, e]
 
 /--
-  `mkProjection s fieldName` return an expression for accessing field `fieldName` of the structure `s`.
+  `mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
   Remark: `fieldName` may be a subfield of `s`. -/
 partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
   let type ← inferType s

src/Lean/SubExpr.lean

@@ -84,7 +84,7 @@ The first coordinate in the array corresponds to the root of the expression tree
 def ofArray (ps : Array Nat) : Pos :=
   ps.foldl push root
 
-/-- Decodes a subexpression `Pos` as a sequence of coordinates `cs : Array Nat`. See `Pos.fromArray` for details.
+/-- Decodes a subexpression `Pos` as a sequence of coordinates `cs : Array Nat`. See `Pos.ofArray` for details.
 `cs[0]` is the coordinate for the root expression. -/
 def toArray (p : Pos) : Array Nat :=
   foldl Array.push #[] p