no goals
ι : Type ?u.137301
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
cases le_total b c with
| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
no goals
case inl
ι : Type ?u.137301
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
rw [Ico_filter_lt_of_right_le h, min_eq_left h]
no goals
case inr
ι : Type ?u.137301
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
rw [Ico_filter_lt_of_le_right h, min_eq_right h]