no goals
ι : Type ?u.139276
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
cases le_total a c with
| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
no goals
case inl
ι : Type ?u.139276
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
rw [Ico_filter_le_of_left_le h, max_eq_right h]
no goals
case inr
ι : Type ?u.139276
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
rw [Ico_filter_le_of_le_left h, max_eq_left h]