-- Mathlib/Data/ZMod/Basic.lean
theorem cast_add_eq_ite {n : ℕ} (a b : ZMod n) :
    (cast (a + b) : ℤ) =
      if (n : ℤ) ≤ cast a + cast b then (cast a + cast b - n : ℤ) else cast a + cast b

Proof state:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ cast a + cast b then cast a + cast b - ↑(n + 1) else cast a + cast b

Tactic:
change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _

Result:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑↑(a + b) = if ↑(n + 1) ≤ ↑↑a + ↑↑b then cast a + cast b - ↑(n + 1) else cast a + cast b

Proof state:
case zero
a b : ZMod 0
⊢ (a + b).cast = if ↑0 ≤ a.cast + b.cast then a.cast + b.cast - ↑0 else a.cast + b.cast

Tactic:
simp

Result:
case zero
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

Proof state:
case zero
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

Tactic:
rfl

Result:
no goals

Proof state:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) - ↑(n + 1) = cast a + cast b - ↑(n + 1)

Tactic:
congr

Result:
no goals

Proof state:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if ↑n + 1 ≤ ↑↑a + ↑↑b then cast a + cast b - (↑n + 1) else cast a + cast b

Tactic:
norm_cast

Result:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if n + 1 ≤ ↑a + ↑b then cast a + cast b - ↑(n + 1) else cast a + cast b

Proof state:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

Tactic:
rw [Nat.cast_sub h]

Result:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) - ↑(n + 1) = cast a + cast b - ↑(n + 1)

Proof state:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑↑(a + b) = if ↑(n + 1) ≤ ↑↑a + ↑↑b then cast a + cast b - ↑(n + 1) else cast a + cast b

Tactic:
simp only [Fin.val_add_eq_ite, Int.ofNat_succ, Int.ofNat_le]

Result:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if ↑n + 1 ≤ ↑↑a + ↑↑b then cast a + cast b - (↑n + 1) else cast a + cast b

Proof state:
case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
a b : ZMod n
⊢ (a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast

Tactic:
rcases n with - | n

Result:
case zero
a b : ZMod 0
⊢ (a + b).cast = if ↑0 ≤ a.cast + b.cast then a.cast + b.cast - ↑0 else a.cast + b.cast

case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ a.cast + b.cast then a.cast + b.cast - ↑(n + 1) else a.cast + b.cast

Proof state:
case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ a.cast + b.cast then a.cast + b.cast - ↑(n + 1) else a.cast + b.cast

Tactic:
change Fin (n + 1) at a b

Result:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ cast a + cast b then cast a + cast b - ↑(n + 1) else cast a + cast b

Proof state:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if n + 1 ≤ ↑a + ↑b then cast a + cast b - ↑(n + 1) else cast a + cast b

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b