case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l

case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
cases' le_total n l with hnl hln
no goals
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
  filter_lt_of_le_bot (le_refl l), append_nil]
no goals
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]