Theorem: add_comm (Fixtures/Debug/AddComm.lean)

State before:
n m : Nat
⊢ n + (m + 1) = m + 1 + n
Tactic:
have : Nat.succ (n + m) = Nat.succ (m + n) :=
  by apply congrArg; apply Nat.add_comm
State after:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = m + 1 + n

State before:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = m + 1 + n
Tactic:
rw [Nat.succ_add m n]
State after:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = Nat.succ (m + n)

State before:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = Nat.succ (m + n)
Tactic:
apply this
State after:
no goals

State before:
n m : Nat
⊢ Nat.succ (n + m) = Nat.succ (m + n)
Tactic:
apply congrArg
State after:
case h
n m : Nat
⊢ n + m = m + n

State before:
case h
n m : Nat
⊢ n + m = m + n
Tactic:
apply Nat.add_comm
State after:
no goals

State before:
n m : Nat
⊢ n + (m + 1) = m + 1 + n
Tactic:
have : Nat.succ (n + m) = Nat.succ (m + n) :=
  by apply congrArg; apply Nat.add_comm
State after:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = m + 1 + n

State before:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = m + 1 + n
Tactic:
rw [Nat.succ_add m n]
State after:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = Nat.succ (m + n)

State before:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = Nat.succ (m + n)
Tactic:
apply this
State after:
no goals

State before:
n m : Nat
⊢ Nat.succ (n + m) = Nat.succ (m + n)
Tactic:
apply congrArg
State after:
case h
n m : Nat
⊢ n + m = m + n

State before:
case h
n m : Nat
⊢ n + m = m + n
Tactic:
apply Nat.add_comm
State after:
no goals