-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem desc_op_comp_opCoproductIsoProduct_hom [HasCoproduct Z] {X : C} (π : (a : α) → Z a ⟶ X) :
    (Sigma.desc π).op ≫ (opCoproductIsoProduct Z).hom = Pi.lift (fun a ↦ (π a).op)

Proof state:
case h.e'_2.h.h.e'_6.h.h.e'_5.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ :
  (op X ⟶ ∏ᶜ fun x => op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x => op (Z x)) (Pi.π fun x => op (Z x))).pt)
e_3✝¹ : op X = op (Cofan.mk X π).pt
e_4✝¹ : op (∐ Z) = op (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_3✝ : ∐ Z = (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_4✝ : X = (Cofan.mk X π).pt
⊢ Sigma.desc π = (coproductIsCoproduct Z).desc (Cofan.mk X π)

Tactic:
ext

Result:
case h.e'_2.h.h.e'_6.h.h.e'_5.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ :
  (op X ⟶ ∏ᶜ fun x => op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x => op (Z x)) (Pi.π fun x => op (Z x))).pt)
e_3✝¹ : op X = op (Cofan.mk X π).pt
e_4✝¹ : op (∐ Z) = op (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_3✝ : ∐ Z = (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_4✝ : X = (Cofan.mk X π).pt
b✝ : α
⊢ Sigma.ι Z b✝ ≫ Sigma.desc π = Sigma.ι Z b✝ ≫ (coproductIsCoproduct Z).desc (Cofan.mk X π)

Proof state:
case h.e'_3.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ :
  (op X ⟶ ∏ᶜ fun x => op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x => op (Z x)) (Pi.π fun x => op (Z x))).pt)
b✝ : α
⊢ (Pi.lift fun a => (π a).op) ≫ Pi.π (fun a => op (Z a)) b✝ =
    (productIsProduct fun x => op (Z x)).lift (Cofan.mk X π).op ≫ Pi.π (fun a => op (Z a)) b✝

Tactic:
simp [Pi.lift, productIsProduct]

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_6.h.h.e'_5.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ :
  (op X ⟶ ∏ᶜ fun x => op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x => op (Z x)) (Pi.π fun x => op (Z x))).pt)
e_3✝¹ : op X = op (Cofan.mk X π).pt
e_4✝¹ : op (∐ Z) = op (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_3✝ : ∐ Z = (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_4✝ : X = (Cofan.mk X π).pt
b✝ : α
⊢ Sigma.ι Z b✝ ≫ Sigma.desc π = Sigma.ι Z b✝ ≫ (coproductIsCoproduct Z).desc (Cofan.mk X π)

Tactic:
simp [Sigma.desc, coproductIsCoproduct]

Result:
no goals

Proof state:
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ :
  (op X ⟶ ∏ᶜ fun x => op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x => op (Z x)) (Pi.π fun x => op (Z x))).pt)
⊢ (Pi.lift fun a => (π a).op) = (productIsProduct fun x => op (Z x)).lift (Cofan.mk X π).op

Tactic:
ext

Result:
case h.e'_3.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ :
  (op X ⟶ ∏ᶜ fun x => op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x => op (Z x)) (Pi.π fun x => op (Z x))).pt)
b✝ : α
⊢ (Pi.lift fun a => (π a).op) ≫ Pi.π (fun a => op (Z a)) b✝ =
    (productIsProduct fun x => op (Z x)).lift (Cofan.mk X π).op ≫ Pi.π (fun a => op (Z a)) b✝