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

State before:
m : ℕ
⊢ zero = Quotient.mk Setoid (m, m)
Tactic:
rw [Int.zero]
State after:
m : ℕ
⊢ Quotient.mk Setoid (0, 0) = Quotient.mk Setoid (m, m)

State before:
m : ℕ
⊢ Quotient.mk Setoid (0, 0) = Quotient.mk Setoid (m, m)
Tactic:
apply Quotient.sound
State after:
case a
m : ℕ
⊢ (0, 0) ≈ (m, m)

State before:
case a
m : ℕ
⊢ (0, 0) ≈ (m, m)
Tactic:
rw [Int.Setoid_Iff]
State after:
case a
m : ℕ
⊢ (0, 0).fst + (m, m).snd = (m, m).fst + (0, 0).snd

State before:
case a
m : ℕ
⊢ (0, 0).fst + (m, m).snd = (m, m).fst + (0, 0).snd
Tactic:
simp
State after:
no goals