Theorem: ExtrDisc.finiteCoproduct.ιCompFromFiniteCoproduct (Sieves/OpenEmbedding.lean)

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