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

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

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
x y : (forget Profinite).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