Theorem: Profinite.IsIsotoFiniteCoproduct (Profinite/ExplicitLimits.lean)

State before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
State after:
no goals