α : Type u
β : Type v
γ : Type ?u.21406
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : (⋃ (x : α) (_ : x ∈ s), {x}) ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
α : Type u
β : Type v
γ : Type ?u.21406
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : s ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
rw [← biUnion_of_singleton s] at h'
case intro.intro
α : Type u
β : Type v
γ : Type ?u.21406
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : (⋃ (x : α) (_ : x ∈ s), {x}) ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
α : Type u
β : Type v
γ : Type ?u.21406
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : (⋃ (x : α) (_ : x ∈ s), {x}) ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
rcases(Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩
no goals
case intro.intro
α : Type u
β : Type v
γ : Type ?u.21406
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : (⋃ (x : α) (_ : x ∈ s), {x}) ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩