a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
⊢ a = b
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ a = b
let ⟨n, hn⟩ := le.dest h₁
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
⊢ a = b
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
⊢ a = b
let ⟨m, hm⟩ := le.dest h₂
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : a + ↑n = b
⊢ a = b
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
⊢ a = b
have := hn
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : b + ↑(m + n) = b
⊢ a = b
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : a + ↑n = b
⊢ a = b
rw [← hm, Int.add_assoc, ← ofNat_add] at this
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this✝ : b + ↑(m + n) = b
this : m + n = 0
⊢ a = b
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : b + ↑(m + n) = b
⊢ a = b
have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm
no goals
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this✝ : b + ↑(m + n) = b
this : m + n = 0
⊢ a = b
rw [← hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a]