-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem opCoproductIsoProduct'_comp_self {c c' : Cofan Z} {f : Fan (op <| Z ·)}
    (hc : IsColimit c) (hc' : IsColimit c') (hf : IsLimit f) :
    (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv =
    (hc.coconePointUniqueUpToIso hc').op.inv

Proof state:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
    (c.ι.app { as := j }).op

Tactic:
simp only [op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc,
  opCoproductIsoProduct'_inv_comp_inj]

Result:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = (c.ι.app { as := j }).op

Proof state:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c.inj j).op = (c.ι.app { as := j }).op

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    (hc.coconePointUniqueUpToIso hc').op.inv.unop

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }

Tactic:
apply Quiver.Hom.op_inj

Result:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
    (c.ι.app { as := j }).op

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
apply hc'.hom_ext

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ ∀ (j : Discrete α),
    c'.ι.app j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
      c'.ι.app j ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.ι.app { as := j } ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
change c'.inj _ ≫ _ = _

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
simp only [unop_op, unop_comp, Discrete.functor_obj, const_obj_obj, Iso.op_inv,
  Quiver.Hom.unop_op, IsColimit.comp_coconePointUniqueUpToIso_inv]

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }

Proof state:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = (c.ι.app { as := j }).op

Tactic:
rw [← opCoproductIsoProduct'_inv_comp_inj hc hf]

Result:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op = (c.ι.app { as := j }).op

Proof state:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op = (c.ι.app { as := j }).op

Tactic:
simp only [Iso.hom_inv_id_assoc]

Result:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c.inj j).op = (c.ι.app { as := j }).op

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ ∀ (j : Discrete α),
    c'.ι.app j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
      c'.ι.app j ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
intro ⟨j⟩

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.ι.app { as := j } ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop