Theorem: Int.add_neg_eq_sub (Table/BuiltinExtensions.lean)

State before:
m n : Int
⊢ n < 0 → m + n = m - ofNat (abs n)
Tactic:
intros h
State after:
m n : Int
h : n < 0
⊢ m + n = m - ofNat (abs n)

State before:
m n : Int
h : n < 0
⊢ m + n = m - ofNat (abs n)
Tactic:
cases n with
| ofNat n => contradiction
| negSucc n =>
  simp only [abs]
  unfold HSub.hSub
  unfold instHSub
  unfold Sub.sub
  unfold Int.instSubInt
  unfold Int.sub
  simp only
  rw [neg_succ_eq_neg_ofNat_succ]
State after:
no goals

State before:
case ofNat
m : Int
n : Nat
h : ofNat n < 0
⊢ m + ofNat n = m - ofNat (abs (ofNat n))
Tactic:
contradiction
State after:
no goals

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (abs (negSucc n))
Tactic:
simp only [abs]
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (Nat.succ n)

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (Nat.succ n)
Tactic:
unfold HSub.hSub
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = instHSub.1 m (ofNat (Nat.succ n))

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = instHSub.1 m (ofNat (Nat.succ n))
Tactic:
unfold instHSub
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => Sub.sub a b }.1 m (ofNat (Nat.succ n))

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => Sub.sub a b }.1 m (ofNat (Nat.succ n))
Tactic:
unfold Sub.sub
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => instSubInt.1 a b }.1 m (ofNat (Nat.succ n))

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => instSubInt.1 a b }.1 m (ofNat (Nat.succ n))
Tactic:
unfold Int.instSubInt
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := Int.sub }.1 a b }.1 m (ofNat (Nat.succ n))

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := Int.sub }.1 a b }.1 m (ofNat (Nat.succ n))
Tactic:
unfold Int.sub
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := fun m n => m + -n }.1 a b }.1 m (ofNat (Nat.succ n))

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := fun m n => m + -n }.1 a b }.1 m (ofNat (Nat.succ n))
Tactic:
simp only
State after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m + -ofNat (Nat.succ n)

State before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m + -ofNat (Nat.succ n)
Tactic:
rw [neg_succ_eq_neg_ofNat_succ]
State after:
no goals