X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝ = a₂✝
⊢ ∀ {X Y : Compactum}, Function.Injective compactumToCompHaus.map
intro _ _ _ _ h
case f
X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝.f = a₂✝.f
X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝ = a₂✝
apply Monad.Algebra.Hom.ext
no goals
case f
X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝.f = a₂✝.f
apply congrArg (fun f => f.toFun) h