a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
⊢ a < b
a b : Int
⊢ a < b ↔ a ≤ b ∧ a ≠ b
refine ⟨fun h => ⟨Int.le_of_lt h, Int.ne_of_lt h⟩, fun ⟨aleb, aneb⟩ => ?_⟩
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
⊢ a < b
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
⊢ a < b
let ⟨n, hn⟩ := le.dest aleb
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a < b
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
⊢ a < b
have : n ≠ 0 := aneb.imp fun eq => by rw [← hn, eq, ofNat_zero, Int.add_zero]
case h
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a + ↑(succ ?n) = b

case n
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ Nat
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a < b
apply lt.intro
no goals
case h
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a + ↑(succ ?n) = b

case n
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ Nat
rwa [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero this)] at hn
no goals
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
eq : n = 0
⊢ a = b
rw [← hn, eq, ofNat_zero, Int.add_zero]