Theorem: FilterGame.Ultrafilter.coe_injective (FilterGame/Solutions/Ultrafilter.lean)

State before:
α : Type u_1
⊢ Function.Injective Coe.coe
Tactic:
intros f g h
State after:
α : Type u_1
f g : Ultrafilter α
h : Coe.coe f = Coe.coe g
⊢ f = g

State before:
α : Type u_1
f g : Ultrafilter α
h : Coe.coe f = Coe.coe g
⊢ f = g
Tactic:
cases f
State after:
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

State before:
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
Tactic:
cases g
State after:
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✝ }

State before:
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✝ }
Tactic:
congr
State after:
no goals