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

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