no goals
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hbc : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a b
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]