Theorem: CompHaus.finiteCoproduct.ι_injective (CompHaus/ExplicitLimits.lean)

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
⊢ Function.Injective ↑(ι Z a)
Tactic:
intro x y hxy
State after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
x y : (forget CompHaus).obj (Z a)
hxy : ↑(ι Z a) x = ↑(ι Z a) y
⊢ x = y

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
x y : (forget CompHaus).obj (Z a)
hxy : ↑(ι Z a) x = ↑(ι Z a) y
⊢ x = y
Tactic:
exact eq_of_heq (Sigma.ext_iff.mp hxy).2
State after:
no goals