-- Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
theorem colimitPointwiseProductToProductColimit_app (d : D) :
    (colimitPointwiseProductToProductColimit F).app d =
      (colimitObjIsoColimitCompEvaluation _ _).hom ≫
        (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
          colimitPointwiseProductToProductColimit _ ≫
            (Pi.mapIso fun _ => (colimitObjIsoColimitCompEvaluation _ _).symm).hom ≫
              (piObjIso _ _).inv

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
s : α
k : (i : α) → I i
⊢ colimit.ι (pointwiseProduct F ⋙ (evaluation D C).obj d) k ≫
      (((colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫
            (colimitPointwiseProductToProductColimit F).app d) ≫
          (piObjIso (fun x => colimit (F x)) d).hom) ≫
        Pi.π (fun x => (colimit (F x)).obj d) s =
    colimit.ι (pointwiseProduct F ⋙ (evaluation D C).obj d) k ≫
      (((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
            colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
          (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom) ≫
        Pi.π (fun x => (colimit (F x)).obj d) s

Tactic:
simp [← NatTrans.comp_app]

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ (colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫ (colimitPointwiseProductToProductColimit F).app d =
    (((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
          colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
        (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom) ≫
      (piObjIso (fun x => colimit (F x)) d).inv

Tactic:
rw [Iso.eq_comp_inv]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ ((colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫
        (colimitPointwiseProductToProductColimit F).app d) ≫
      (piObjIso (fun x => colimit (F x)) d).hom =
    ((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
        colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
      (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ ((colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫
        (colimitPointwiseProductToProductColimit F).app d) ≫
      (piObjIso (fun x => colimit (F x)) d).hom =
    ((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
        colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
      (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom

Tactic:
refine Pi.hom_ext _ _ (fun s => colimit.hom_ext (fun k => ?_))

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
s : α
k : (i : α) → I i
⊢ colimit.ι (pointwiseProduct F ⋙ (evaluation D C).obj d) k ≫
      (((colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫
            (colimitPointwiseProductToProductColimit F).app d) ≫
          (piObjIso (fun x => colimit (F x)) d).hom) ≫
        Pi.π (fun x => (colimit (F x)).obj d) s =
    colimit.ι (pointwiseProduct F ⋙ (evaluation D C).obj d) k ≫
      (((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
            colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
          (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom) ≫
        Pi.π (fun x => (colimit (F x)).obj d) s

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ (colimitPointwiseProductToProductColimit F).app d =
    (colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).hom ≫
      (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
        (colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
          (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom ≫
            (piObjIso (fun x => colimit (F x)) d).inv

Tactic:
rw [← Iso.inv_comp_eq]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ (colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫ (colimitPointwiseProductToProductColimit F).app d =
    (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
      (colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
        (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom ≫
          (piObjIso (fun x => colimit (F x)) d).inv

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ (colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫ (colimitPointwiseProductToProductColimit F).app d =
    (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
      (colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
        (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom ≫
          (piObjIso (fun x => colimit (F x)) d).inv

Tactic:
simp only [← Category.assoc]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
α : Type w
I : α → Type u₂
inst✝³ : (i : α) → Category.{w, u₂} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ (colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫ (colimitPointwiseProductToProductColimit F).app d =
    (((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
          colimitPointwiseProductToProductColimit fun s => F s ⋙ (evaluation D C).obj d) ≫
        (Pi.mapIso fun x => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom) ≫
      (piObjIso (fun x => colimit (F x)) d).inv