Theorem: Int.neg_mk (Extra/Int/Lemmas.lean)

State before:
m n : Nat
⊢ -(m ⊖ n) = n ⊖ m
Tactic:
induction m, n with
| zero_zero => rw [zero_mk_zero]; rfl
| zero_succ n => rw [zero_mk_succ, succ_mk_zero]; rfl
| succ_zero m => rw [succ_mk_zero, zero_mk_succ]; rfl
| succ_succ m n ih => rw [succ_mk_succ, succ_mk_succ]; exact ih
State after:
no goals

State before:
case zero_zero

⊢ -(0 ⊖ 0) = 0 ⊖ 0
Tactic:
rw [zero_mk_zero]
State after:
case zero_zero

⊢ -0 = 0

State before:
case zero_zero

⊢ -0 = 0
Tactic:
rfl
State after:
no goals

State before:
case zero_succ
n : Nat
a✝ : -(0 ⊖ n) = n ⊖ 0
⊢ -(0 ⊖ n + 1) = n + 1 ⊖ 0
Tactic:
rw [zero_mk_succ, succ_mk_zero]
State after:
case zero_succ
n : Nat
a✝ : -(0 ⊖ n) = n ⊖ 0
⊢ - -[n+1] = ofNat (n + 1)

State before:
case zero_succ
n : Nat
a✝ : -(0 ⊖ n) = n ⊖ 0
⊢ - -[n+1] = ofNat (n + 1)
Tactic:
rfl
State after:
no goals

State before:
case succ_zero
m : Nat
a✝ : -(m ⊖ 0) = 0 ⊖ m
⊢ -(m + 1 ⊖ 0) = 0 ⊖ m + 1
Tactic:
rw [succ_mk_zero, zero_mk_succ]
State after:
case succ_zero
m : Nat
a✝ : -(m ⊖ 0) = 0 ⊖ m
⊢ -ofNat (m + 1) = -[m+1]

State before:
case succ_zero
m : Nat
a✝ : -(m ⊖ 0) = 0 ⊖ m
⊢ -ofNat (m + 1) = -[m+1]
Tactic:
rfl
State after:
no goals

State before:
case succ_succ
m n : Nat
ih : -(m ⊖ n) = n ⊖ m
⊢ -(m + 1 ⊖ n + 1) = n + 1 ⊖ m + 1
Tactic:
rw [succ_mk_succ, succ_mk_succ]
State after:
case succ_succ
m n : Nat
ih : -(m ⊖ n) = n ⊖ m
⊢ -(m ⊖ n) = n ⊖ m

State before:
case succ_succ
m n : Nat
ih : -(m ⊖ n) = n ⊖ m
⊢ -(m ⊖ n) = n ⊖ m
Tactic:
exact ih
State after:
no goals