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

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

Tactic:
simp only [unop_op, unop_comp, Category.assoc, Discrete.functor_obj, Iso.op_inv,
  Quiver.Hom.unop_op, IsLimit.conePointUniqueUpToIso_inv_comp]

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

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

Tactic:
apply hf.hom_ext

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

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ (opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = f'.π.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
f f' : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ ((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op =
    (f'.π.app { as := j }).op

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

Tactic:
apply Quiver.Hom.unop_inj

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

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

Tactic:
simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]

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

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

Tactic:
rfl

Result:
no goals

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

Tactic:
intro ⟨j⟩

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

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

Tactic:
change _ ≫ f.proj _ = _

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

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

Tactic:
simp only [op_comp, op_unop, Quiver.Hom.op_unop, proj_comp_opProductIsoCoproduct'_hom]

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

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

Tactic:
rw [← proj_comp_opProductIsoCoproduct'_hom hf' hc]

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