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

State before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
State after:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)

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