α : Type u
x y : α
h : pure x = pure y
⊢ x = y
α : Type u
⊢ Function.Injective pure
intro x y h
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure x
⊢ x = y
α : Type u
x y : α
h : pure x = pure y
⊢ x = y
have : {x} ∈ (pure x : Ultrafilter α) := singleton_mem_pure
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure y
⊢ x = y
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure x
⊢ x = y
rw [h] at this
no goals
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure y
⊢ x = y
exact (mem_singleton_iff.mp (mem_pure.mp this)).symm