-- Mathlib/CategoryTheory/Sites/Preserves.lean
theorem piComparison_fac :
    have : HasCoproduct X := ⟨⟨c, hc⟩⟩
    piComparison F (fun x ↦ op (X x)) = F.map (opCoproductIsoProduct' hc (productIsProduct _)).inv ≫
    Equalizer.Presieve.Arrows.forkMap F X c.inj

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
⊢ let_fun this := ⋯;
  (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj

Tactic:
have : HasCoproduct X := ⟨⟨c, hc⟩⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ let_fun this := ⋯;
  (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
hh : (Pi.lift fun i => (c.inj i).op) = (productIsProduct fun x => op (X x)).lift c.op
⊢ (piComparison F fun x => op (X x)) =
    F.map
        ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
          (hc.desc c).op ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom) ≫
      piComparison F fun i => op (X i)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
⊢ (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => F.map (c.inj i).op

Tactic:
rw [h, ← Category.assoc, ← Functor.map_comp]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
⊢ (piComparison F fun x => op (X x)) =
    F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => (c.inj i).op) ≫
      piComparison F fun i => op (X i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => F.map (c.inj i).op

Tactic:
have h : Pi.lift (fun i ↦ F.map (c.inj i).op) =
    F.map (Pi.lift (fun i ↦ (c.inj i).op)) ≫ piComparison F _ := by simp

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
⊢ (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => F.map (c.inj i).op

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
⊢ (Pi.lift fun i => (c.inj i).op) = (productIsProduct fun x => op (X x)).lift c.op

Tactic:
simp [Pi.lift, productIsProduct]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
hh : (Pi.lift fun i => (c.inj i).op) = (productIsProduct fun x => op (X x)).lift c.op
⊢ (piComparison F fun x => op (X x)) =
    F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => (c.inj i).op) ≫
      piComparison F fun i => op (X i)

Tactic:
rw [hh, ← desc_op_comp_opCoproductIsoProduct'_hom hc]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
hh : (Pi.lift fun i => (c.inj i).op) = (productIsProduct fun x => op (X x)).lift c.op
⊢ (piComparison F fun x => op (X x)) =
    F.map
        ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
          (hc.desc c).op ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom) ≫
      piComparison F fun i => op (X i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ let_fun this := ⋯;
  (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj

Tactic:
dsimp only [Equalizer.Presieve.Arrows.forkMap]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ (piComparison F fun x => op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => F.map (c.inj i).op