case a
ι : Type ?u.109806
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}
ι : Type ?u.109806
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}
ext x
case a
ι : Type ?u.109806
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x = a ∧ x < b ↔ x = a
case a
ι : Type ?u.109806
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}
rw [mem_filter, mem_Ico, mem_singleton, and_right_comm, ← le_antisymm_iff, eq_comm]
no goals
case a
ι : Type ?u.109806
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x = a ∧ x < b ↔ x = a
exact and_iff_left_of_imp fun h => h.le.trans_lt hab