α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ {a}.val = {a}
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ {a}.val = {a}
rfl