Theorem: LoVe.int.neg_neg (LoVe/Labs/Lab8Solution.lean)

State before:
a : Int
⊢ Int.neg (Int.neg a) = a
Tactic:
induction a using Quotient.inductionOn with
| h pn =>
  cases pn with
  | mk p n => apply Int.neg_eq
State after:
no goals

State before:
case h
pn : ℕ × ℕ
⊢ Int.neg (Int.neg (Quotient.mk Int.Setoid pn)) = Quotient.mk Int.Setoid pn
Tactic:
cases pn with
| mk p n => apply Int.neg_eq
State after:
no goals

State before:
case h.mk
p n : ℕ
⊢ Int.neg (Int.neg (Quotient.mk Int.Setoid (p, n))) = Quotient.mk Int.Setoid (p, n)
Tactic:
apply Int.neg_eq
State after:
no goals