Theorem: Pos.div2_eq (GMLInit/Data/Pos.lean)

State before:
n : Nat
⊢ 2 * (div2 (n + 2)).fst + ↑(div2 (n + 2)).snd = n + 2
Tactic:
simp only [div2]
State after:
n : Nat
⊢ 2 * ((div2 n).fst + 1) + ↑(div2 n).snd = n + 2

State before:
n : Nat
⊢ 2 * ((div2 n).fst + 1) + ↑(div2 n).snd = n + 2
Tactic:
rw [Nat.mul_succ]
State after:
n : Nat
⊢ 2 * (div2 n).fst + 2 + ↑(div2 n).snd = n + 2

State before:
n : Nat
⊢ 2 * (div2 n).fst + 2 + ↑(div2 n).snd = n + 2
Tactic:
rw [Nat.add_right_comm]
State after:
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd + 2 = n + 2

State before:
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd + 2 = n + 2
Tactic:
congr
State after:
case e_a
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd = n

State before:
case e_a
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd = n
Tactic:
exact div2_eq n
State after:
no goals