case a
ι : Type ?u.141256
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝¹ b✝ a b c a✝ : α
⊢ a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (min b c)
ι : Type ?u.141256
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => x < c) (Ioo a b) = Ioo a (min b c)
ext
no goals
case a
ι : Type ?u.141256
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝¹ b✝ a b c a✝ : α
⊢ a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (min b c)
simp [and_assoc]