no goals
α : Type u
β : Type v
γ : Type ?u.3235
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h₁ : NeBot f
h₂ : ∀ (g : Filter α), NeBot g → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : NeBot g
le_of_le✝ : ∀ (g_1 : Filter α), NeBot g_1 → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
congr