case h
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ insert a (Ioi a)
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ioi (pred a) = insert a (Ioi a)
ext x
case h
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ a = x ∨ a < x
case h
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ insert a (Ioi a)
simp only [insert, mem_setOf, @eq_comm _ x a, mem_Ioi, Set.insert]
no goals
case h
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ a = x ∨ a < x
exact pred_lt_iff_eq_or_lt_of_not_isMin ha