no goals
α : Type u
β : Type v
γ : Type ?u.15563
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
is : Set β
s : β → Set α
his : Set.Finite is
⊢ (⋃ (i : β) (_ : i ∈ is), s i) ∈ f ↔ ∃ i, i ∈ is ∧ s i ∈ f
simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), bex_image_iff]