a b : Int
⊢ a ≤ b ∧ a ≠ b ↔ a ≤ b ∧ ¬b ≤ a
a b : Int
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
rw [Int.lt_iff_le_and_ne]
case mp
a b : Int
x✝ : a ≤ b ∧ a ≠ b
h : a ≤ b
h'✝ : a ≠ b
h' : b ≤ a
⊢ a = b

case mpr
a b : Int
x✝ : a ≤ b ∧ ¬b ≤ a
h : a ≤ b
h'✝ : ¬b ≤ a
h' : a = b
⊢ b ≤ a
a b : Int
⊢ a ≤ b ∧ a ≠ b ↔ a ≤ b ∧ ¬b ≤ a
constructor <;> refine fun ⟨h, h'⟩ => ⟨h, h'.imp fun h' => ?_⟩
no goals
case mp
a b : Int
x✝ : a ≤ b ∧ a ≠ b
h : a ≤ b
h'✝ : a ≠ b
h' : b ≤ a
⊢ a = b
exact Int.le_antisymm h h'
case mpr
a : Int
x✝ : a ≤ a ∧ ¬a ≤ a
h : a ≤ a
h' : ¬a ≤ a
⊢ a ≤ a
case mpr
a b : Int
x✝ : a ≤ b ∧ ¬b ≤ a
h : a ≤ b
h'✝ : ¬b ≤ a
h' : a = b
⊢ b ≤ a
subst h'
no goals
case mpr
a : Int
x✝ : a ≤ a ∧ ¬a ≤ a
h : a ≤ a
h' : ¬a ≤ a
⊢ a ≤ a
apply Int.le_refl