Theorem: descOpCompCoprodToProd (Sieves/ProdCoprod.lean)

State before:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
⊢ (Sigma.desc π).op ≫ (CoprodToProd Z).hom = Pi.lift fun a => (π a).op
Tactic:
refine' limit.hom_ext (fun a => _)
State after:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Sigma.desc π).op ≫ (CoprodToProd Z).hom) ≫ limit.π (Discrete.functor fun z => (Z z).op) a =
    (Pi.lift fun a => (π a).op) ≫ limit.π (Discrete.functor fun z => (Z z).op) a

State before:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Sigma.desc π).op ≫ (CoprodToProd Z).hom) ≫ limit.π (Discrete.functor fun z => (Z z).op) a =
    (Pi.lift fun a => (π a).op) ≫ limit.π (Discrete.functor fun z => (Z z).op) a
Tactic:
simp only [CoprodToProd, Category.assoc, limit.conePointUniqueUpToIso_hom_comp, oppositeFan_pt, 
  oppositeFan_π_app, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, ← op_comp, colimit.ι_desc]
State after:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Cofan.mk X π).ι.app { as := a.as }).op = (π a.as).op

State before:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Cofan.mk X π).ι.app { as := a.as }).op = (π a.as).op
Tactic:
rfl
State after:
no goals