A lemma about ultrafilters

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have the following variant of exists_ultrafilter? I couldn't find anything similar.

lemma exists_ultrafilter' (S : set (set α)) (cond : ∀ T : finset (set α),
  ↑T ⊆ S → ⋂₀ (↑T : set (set α)) ≠ ∅) : ∃ F : filter α, S ⊆ F.sets ∧ is_ultrafilter F := sorry

[Adam Topaz]

If not, I could open a PR for this:
https://github.com/leanprover-community/mathlib/blob/b85798964d03672dc8c3123ccdd5a7fa2916f2eb/src/order/filter/ultrafilter.lean#L145

[Adam Topaz]

#4436