Theorem: LoVe.Int.add_zero (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
i : Int
⊢ add zero i = i
Tactic:
induction i using Quotient.inductionOn with
| h pn =>
  cases pn with
  | mk p n => simp [Int.zero, Int.add_Eq]
State after:
no goals

State before:
case h
pn : ℕ × ℕ
⊢ add zero (Quotient.mk Setoid pn) = Quotient.mk Setoid pn
Tactic:
cases pn with
| mk p n => simp [Int.zero, Int.add_Eq]
State after:
no goals

State before:
case h.mk
p n : ℕ
⊢ add zero (Quotient.mk Setoid (p, n)) = Quotient.mk Setoid (p, n)
Tactic:
simp [Int.zero, Int.add_Eq]
State after:
no goals