cases g
case mk
α : Type u_1
g : Ultrafilter α
as_filter✝ : Filter α
ne_bot✝ : as_filter✝ ≠ ⊥
le_of_le✝ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝ → as_filter✝ ≤ g
h : Coe.coe { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ } = Coe.coe g
⊢ { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ } = g
case mk.mk
α : Type u_1
as_filter✝¹ : Filter α
ne_bot✝¹ : as_filter✝¹ ≠ ⊥
le_of_le✝¹ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝¹ → as_filter✝¹ ≤ g
as_filter✝ : Filter α
ne_bot✝ : as_filter✝ ≠ ⊥
le_of_le✝ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝ → as_filter✝ ≤ g
h :
  Coe.coe { as_filter := as_filter✝¹, ne_bot := ne_bot✝¹, le_of_le := le_of_le✝¹ } =
    Coe.coe { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ }
⊢ { as_filter := as_filter✝¹, ne_bot := ne_bot✝¹, le_of_le := le_of_le✝¹ } =
    { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ }