no goals
α : Type u
β : Type v
γ : Type ?u.20593
f g : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)
rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]