Theorem: ExtrDisc.IsIsotoFiniteCoproduct (Sieves/OpenEmbedding.lean)

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

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