Theorem: Profinite.Sigma.ιCompToFiniteCoproduct (Profinite/ExplicitLimits.lean)

State before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
⊢ Sigma.ι Z a ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a
Tactic:
simp [toFiniteCoproduct]
State after:
no goals