-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/LemmasAux.lean
theorem toNat_sub' (a : Int) (b : Nat) : (a - b).toNat = a.toNat - b

Proof state:
case h_1.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = ↑b
⊢ a - b✝ = b

Tactic:
omega

Result:
no goals

Proof state:
case h_2.h_2
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : -[a+1] - ↑b✝ = -[b+1]
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case h_1.h_2
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = -[b+1]
⊢ a - b✝ = 0

Tactic:
simp [Int.negSucc_eq] at h

Result:
case h_1.h_2
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = -(↑b + 1)
⊢ a - b✝ = 0

Proof state:
case h_1
b : Nat
x : Int
a : Nat
⊢ a - b =
    match ↑a - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Tactic:
split <;> rename_i y b h

Result:
case h_1.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = ofNat b
⊢ a - b✝ = b

case h_1.h_2
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = -[b+1]
⊢ a - b✝ = 0

Proof state:
case h_1.h_2
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = -(↑b + 1)
⊢ a - b✝ = 0

Tactic:
omega

Result:
no goals

Proof state:
case h_1
b : Nat
x : Int
a : Nat
⊢ a - b =
    match ofNat a - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Tactic:
simp only [Int.ofNat_eq_coe]

Result:
case h_1
b : Nat
x : Int
a : Nat
⊢ a - b =
    match ↑a - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Proof state:
case h_2.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : -[a+1] - ↑b✝ = ofNat b
⊢ 0 = b

Tactic:
simp [Int.negSucc_eq] at h

Result:
case h_2.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : -(↑a + 1) - ↑b✝ = ↑b
⊢ 0 = b

Proof state:
a : Int
b : Nat
⊢ (match a with
      | ofNat n => n
      | -[a+1] => 0) -
      b =
    match a - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Tactic:
split <;> rename_i x a

Result:
case h_1
b : Nat
x : Int
a : Nat
⊢ a - b =
    match ofNat a - ↑b with
    | ofNat n => n
    | -[a+1] => 0

case h_2
b : Nat
x : Int
a : Nat
⊢ 0 - b =
    match -[a+1] - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Proof state:
case h_2
b : Nat
x : Int
a : Nat
⊢ 0 =
    match -[a+1] - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Tactic:
split <;> rename_i y b h

Result:
case h_2.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : -[a+1] - ↑b✝ = ofNat b
⊢ 0 = b

case h_2.h_2
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : -[a+1] - ↑b✝ = -[b+1]
⊢ 0 = 0

Proof state:
case h_1.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = ofNat b
⊢ a - b✝ = b

Tactic:
simp at h

Result:
case h_1.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : ↑a - ↑b✝ = ↑b
⊢ a - b✝ = b

Proof state:
a : Int
b : Nat
⊢ (a - ↑b).toNat = a.toNat - b

Tactic:
symm

Result:
a : Int
b : Nat
⊢ a.toNat - b = (a - ↑b).toNat

Proof state:
case h_2
b : Nat
x : Int
a : Nat
⊢ 0 - b =
    match -[a+1] - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Tactic:
simp only [Nat.zero_sub]

Result:
case h_2
b : Nat
x : Int
a : Nat
⊢ 0 =
    match -[a+1] - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Proof state:
a : Int
b : Nat
⊢ a.toNat - b = (a - ↑b).toNat

Tactic:
simp only [Int.toNat]

Result:
a : Int
b : Nat
⊢ (match a with
      | ofNat n => n
      | -[a+1] => 0) -
      b =
    match a - ↑b with
    | ofNat n => n
    | -[a+1] => 0

Proof state:
case h_2.h_1
b✝ : Nat
x : Int
a : Nat
y : Int
b : Nat
h : -(↑a + 1) - ↑b✝ = ↑b
⊢ 0 = b

Tactic:
omega

Result:
no goals