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