Is the indentation level wrong in the style guide?

Stream: mathlib4

[Geoffrey Irving]

The style guide says

After stating the theorem, we indent the lines in the subsequent proof by 2 spaces.

open Nat
theorem nat_case {P : Nat → Prop} (n : Nat) (H1 : P 0) (H2 : ∀ m, P (succ m)) : P n :=
  Nat.recOn n H1 (fun m IH ↦ H2 m)

and later it gives this example:

import Mathlib.Data.Nat.Basic

theorem Nat.add_right_inj {n m k : Nat} : n + m = n + k → m = k :=
Nat.recOn n
  (fun H : 0 + m = 0 + k ↦ calc
    m = 0 + m := Eq.symm (zero_add m)
    _ = 0 + k := H
    _ = k     := zero_add _)
  (fun (n : Nat) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k) ↦
    have H2 : succ (n + m) = succ (n + k) := calc
      succ (n + m) = succ n + m   := Eq.symm (succ_add n m)
      _            = succ n + k   := H
      _            = succ (n + k) := succ_add n k
    have H3 : n + m = n + k := succ.inj H2
    IH H3)

Should that Nat.recOn n be indented?

[Ruben Van de Velde]

Yes

[Geoffrey Irving]

I'll send a PR.

[Jireh Loreaux]

Yeah, everything there should be indented an extra two spaces.

[Geoffrey Irving]

https://github.com/leanprover-community/leanprover-community.github.io/pull/442