case a
ι : Type ?u.150465
α✝ : Type ?u.150468
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝¹ b✝ : α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b a✝ : α
⊢ a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (min a b)
ι : Type ?u.150465
α✝ : Type ?u.150468
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝ b✝ : α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ filter (fun x => x < b) (Iio a) = Iio (min a b)
ext
no goals
case a
ι : Type ?u.150465
α✝ : Type ?u.150468
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝¹ b✝ : α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b a✝ : α
⊢ a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (min a b)
simp [and_assoc]