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

case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
n m l : ℕ
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
cases' le_total n l with hnl hln
no goals
case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
rw [max_eq_right hnl, filter_le_of_le hnl]
no goals
case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
rw [max_eq_left hln, filter_le_of_le_bot hln]