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

State before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
ext
State after:
case h.w
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
b✝ : α
x✝ : (forget ExtrDisc).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝

State before:
case h.w
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
b✝ : α
x✝ : (forget ExtrDisc).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
State after:
no goals