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

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

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