awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ NatTrans.app (limit.π H j) k = g ≫ NatTrans.app (limit.π H j) k
w₁ :
  ∀ (j : J),
    CategoryStruct.comp (Y := limit (H ⋙ obj (evaluation K C) k))
        (f ≫ Iso.hom (limitObjIsoLimitCompEvaluation H k) : W ⟶ limit (H ⋙ obj (evaluation K C) k))
        (limit.π (H ⋙ obj (evaluation K C) k) j :
          limit (H ⋙ obj (evaluation K C) k) ⟶ (H ⋙ obj (evaluation K C) k).obj j) =
      CategoryStruct.comp (Y := limit (H ⋙ obj (evaluation K C) k))
        (g ≫ Iso.hom (limitObjIsoLimitCompEvaluation H k) : W ⟶ limit (H ⋙ obj (evaluation K C) k))
        (limit.π (H ⋙ obj (evaluation K C) k) j :
          limit (H ⋙ obj (evaluation K C) k) ⟶ (H ⋙ obj (evaluation K C) k).obj j)
⊢ Eq (α := W ⟶ limit (H ⋙ obj (evaluation K C) k))
    (f ≫ Iso.hom (limitObjIsoLimitCompEvaluation H k) : W ⟶ limit (H ⋙ obj (evaluation K C) k))
    (g ≫ Iso.hom (limitObjIsoLimitCompEvaluation H k) : W ⟶ limit (H ⋙ obj (evaluation K C) k))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ NatTrans.app (limit.π H j) k = g ≫ NatTrans.app (limit.π H j) k
j : J
⊢ CategoryStruct.comp (Y := limit (H ⋙ obj (evaluation K C) k))
      (f ≫ Iso.hom (limitObjIsoLimitCompEvaluation H k) : W ⟶ limit (H ⋙ obj (evaluation K C) k))
      (limit.π (H ⋙ obj (evaluation K C) k) j :
        limit (H ⋙ obj (evaluation K C) k) ⟶ (H ⋙ obj (evaluation K C) k).obj j) =
    CategoryStruct.comp (Y := limit (H ⋙ obj (evaluation K C) k))
      (g ≫ Iso.hom (limitObjIsoLimitCompEvaluation H k) : W ⟶ limit (H ⋙ obj (evaluation K C) k))
      (limit.π (H ⋙ obj (evaluation K C) k) j : limit (H ⋙ obj (evaluation K C) k) ⟶ (H ⋙ obj (evaluation K C) k).obj j)

Tactic:
simpa using w j
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v', v₂, u', u₂} D K
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
j : J
w :
  ∀ (d : D),
    Eq (α := (limit (F ⋙ obj (whiskeringLeft D K C) G)).obj d ⟶ (G ⋙ F.obj j).obj d)
      (NatTrans.app
          (CategoryStruct.comp (Y := G ⋙ limit F)
            (Iso.hom (limitCompWhiskeringLeftIsoCompLimit F G) : limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ limit F)
            (G.whiskerLeft (limit.π F j) : G ⋙ limit F ⟶ G ⋙ F.obj j))
          d :
        (limit (F ⋙ obj (whiskeringLeft D K C) G)).obj d ⟶ (G ⋙ F.obj j).obj d)
      (NatTrans.app (limit.π (F ⋙ obj (whiskeringLeft D K C) G) j) d :
        (limit (F ⋙ obj (whiskeringLeft D K C) G)).obj d ⟶ (G ⋙ F.obj j).obj d)
⊢ Eq (α := limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ F.obj j)
    (CategoryStruct.comp (Y := G ⋙ limit F)
        (Iso.hom (limitCompWhiskeringLeftIsoCompLimit F G) : limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ limit F)
        (G.whiskerLeft (limit.π F j) : G ⋙ limit F ⟶ G ⋙ F.obj j) :
      limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ F.obj j)
    (limit.π (F ⋙ obj (whiskeringLeft D K C) G) j :
      limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ (F ⋙ obj (whiskeringLeft D K C) G).obj j)

Tactic:
ext d
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v', v₂, u', u₂} D K
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
j : J
d : D
⊢ Eq (α := (limit (F ⋙ obj (whiskeringLeft D K C) G)).obj d ⟶ (G ⋙ F.obj j).obj d)
    (NatTrans.app
        (CategoryStruct.comp (Y := G ⋙ limit F)
          (Iso.hom (limitCompWhiskeringLeftIsoCompLimit F G) : limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ limit F)
          (G.whiskerLeft (limit.π F j) : G ⋙ limit F ⟶ G ⋙ F.obj j))
        d :
      (limit (F ⋙ obj (whiskeringLeft D K C) G)).obj d ⟶ (G ⋙ F.obj j).obj d)
    (NatTrans.app (limit.π (F ⋙ obj (whiskeringLeft D K C) G) j) d :
      (limit (F ⋙ obj (whiskeringLeft D K C) G)).obj d ⟶ (G ⋙ F.obj j).obj d)

Tactic:
simp [limitCompWhiskeringLeftIsoCompLimit]

Premises used: CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v', v₂, u', u₂} D K
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
j : J
⊢ Eq (α := G ⋙ limit F ⟶ (F ⋙ obj (whiskeringLeft D K C) G).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ obj (whiskeringLeft D K C) G))
        (Iso.inv (limitCompWhiskeringLeftIsoCompLimit F G) : G ⋙ limit F ⟶ limit (F ⋙ obj (whiskeringLeft D K C) G))
        (limit.π (F ⋙ obj (whiskeringLeft D K C) G) j :
          limit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ (F ⋙ obj (whiskeringLeft D K C) G).obj j) :
      G ⋙ limit F ⟶ (F ⋙ obj (whiskeringLeft D K C) G).obj j)
    (G.whiskerLeft (limit.π F j) : G ⋙ limit F ⟶ G ⋙ F.obj j)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
k : K
inst_4 : HasColimit (F.flip.obj k)
⊢ HasColimit (F ⋙ obj (evaluation K C) k)

Tactic:
hasColimit_of_iso (F := F.flip.obj k) (Iso.refl _)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_4 : ∀ (k : K), HasColimit (F.flip.obj k)
k : K
⊢ PreservesColimit F (obj (evaluation K C) k)

Tactic:
let X : (k : K) → ColimitCocone (F.flip.obj k) := fun k => getColimitCocone (F.flip.obj k)
  preservesColimit_of_preserves_colimit_cocone (combinedIsColimit _ X) <|
    IsColimit.ofIsoColimit (colimit.isColimit _) (evaluateCombinedCocones F X k).symm

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, CategoryTheory.evaluation, CategoryTheory.Limits.getColimitCocone, CategoryTheory.Limits.combinedIsColimit, CategoryTheory.Functor.obj, CategoryTheory.Limits.evaluateCombinedCocones
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
dsimp :
  Eq (α := (F.obj j).obj k ⟶ (colimit F).obj k)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) k))
      (colimit.ι (F ⋙ obj (evaluation K C) k) j :
        (F ⋙ obj (evaluation K C) k).obj j ⟶ colimit (F ⋙ obj (evaluation K C) k))
      (Iso.inv (preservesColimitIso (obj (evaluation K C) k) F) :
        colimit (F ⋙ obj (evaluation K C) k) ⟶ (colimit F).obj k))
    (NatTrans.app (colimit.ι F j) k)
⊢ Eq (α := (F ⋙ obj (evaluation K C) k).obj j ⟶ (colimit F).obj k)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) k))
        (colimit.ι (F ⋙ obj (evaluation K C) k) j :
          (F ⋙ obj (evaluation K C) k).obj j ⟶ colimit (F ⋙ obj (evaluation K C) k))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F k) : colimit (F ⋙ obj (evaluation K C) k) ⟶ (colimit F).obj k) :
      (F ⋙ obj (evaluation K C) k).obj j ⟶ (colimit F).obj k)
    (NatTrans.app (colimit.ι F j) k : (F.obj j).obj k ⟶ (colimit F).obj k)

Tactic:
dsimp [colimitObjIsoColimitCompEvaluation]

Premises used: CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
⊢ Eq (α := (F.obj j).obj k ⟶ (colimit F).obj k)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) k))
      (colimit.ι (F ⋙ obj (evaluation K C) k) j :
        (F ⋙ obj (evaluation K C) k).obj j ⟶ colimit (F ⋙ obj (evaluation K C) k))
      (Iso.inv (preservesColimitIso (obj (evaluation K C) k) F) :
        colimit (F ⋙ obj (evaluation K C) k) ⟶ (colimit F).obj k))
    (NatTrans.app (colimit.ι F j) k)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
dsimp :
  Eq (α := (F.obj j).obj k ⟶ colimit (F ⋙ obj (evaluation K C) k))
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
      (Iso.hom (preservesColimitIso (obj (evaluation K C) k) F)))
    (colimit.ι (F ⋙ obj (evaluation K C) k) j)
⊢ Eq (α := (F.obj j).obj k ⟶ colimit (F ⋙ obj (evaluation K C) k))
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k : (F.obj j).obj k ⟶ (colimit F).obj k)
        (Iso.hom (colimitObjIsoColimitCompEvaluation F k) : (colimit F).obj k ⟶ colimit (F ⋙ obj (evaluation K C) k)) :
      (F.obj j).obj k ⟶ colimit (F ⋙ obj (evaluation K C) k))
    (colimit.ι (F ⋙ obj (evaluation K C) k) j :
      (F ⋙ obj (evaluation K C) k).obj j ⟶ colimit (F ⋙ obj (evaluation K C) k))

Tactic:
dsimp [colimitObjIsoColimitCompEvaluation]

Premises used: CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
rw :
  Eq (α := (F.obj j).obj k ⟶ (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) k))
      (colimit.ι (F ⋙ obj (evaluation K C) k) j :
        (F ⋙ obj (evaluation K C) k).obj j ⟶ colimit (F ⋙ obj (evaluation K C) k))
      (Iso.inv (preservesColimitIso (obj (evaluation K C) k) F) :
        colimit (F ⋙ obj (evaluation K C) k) ⟶ (colimit F).obj k))
⊢ Eq (α := (F.obj j).obj k ⟶ colimit (F ⋙ obj (evaluation K C) k))
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
      (Iso.hom (preservesColimitIso (obj (evaluation K C) k) F)))
    (colimit.ι (F ⋙ obj (evaluation K C) k) j)

Tactic:
rw [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
⊢ Eq (α := (F.obj j).obj k ⟶ (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) k))
      (colimit.ι (F ⋙ obj (evaluation K C) k) j :
        (F ⋙ obj (evaluation K C) k).obj j ⟶ colimit (F ⋙ obj (evaluation K C) k))
      (Iso.inv (preservesColimitIso (obj (evaluation K C) k) F) :
        colimit (F ⋙ obj (evaluation K C) k) ⟶ (colimit F).obj k))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
i j : K
f : i ⟶ j
w :
  ∀ (j_1 : J),
    CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i))
        (colimit.ι (F ⋙ obj (evaluation K C) i) j_1 :
          (F ⋙ obj (evaluation K C) i).obj j_1 ⟶ colimit (F ⋙ obj (evaluation K C) i))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j) =
      CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i)) (colimit.ι (F ⋙ obj (evaluation K C) i) j_1)
        (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) j))
          (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
            colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
          (Iso.inv (colimitObjIsoColimitCompEvaluation F j) : colimit (F ⋙ obj (evaluation K C) j) ⟶ (colimit F).obj j))
⊢ Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
    (Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) j))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F j) : colimit (F ⋙ obj (evaluation K C) j) ⟶ (colimit F).obj j) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
i j : K
f : i ⟶ j
j_1 : J
⊢ CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i))
      (colimit.ι (F ⋙ obj (evaluation K C) i) j_1 :
        (F ⋙ obj (evaluation K C) i).obj j_1 ⟶ colimit (F ⋙ obj (evaluation K C) i))
      (Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f :
        colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j) =
    CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i)) (colimit.ι (F ⋙ obj (evaluation K C) i) j_1)
      (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) j))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F j) : colimit (F ⋙ obj (evaluation K C) j) ⟶ (colimit F).obj j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), NatTrans.app (colimit.ι H j) k ≫ f = NatTrans.app (colimit.ι H j) k ≫ g
apply :
  Eq (α := colimit (H ⋙ obj (evaluation K C) k) ⟶ W)
    (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ f : colimit (H ⋙ obj (evaluation K C) k) ⟶ W)
    (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ g : colimit (H ⋙ obj (evaluation K C) k) ⟶ W)
⊢ f = g

Tactic:
apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1

Premises used: Iff.mp, CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), NatTrans.app (colimit.ι H j) k ≫ f = NatTrans.app (colimit.ι H j) k ≫ g
w₁ :
  ∀ (j : J),
    CategoryStruct.comp (Y := colimit (H ⋙ obj (evaluation K C) k))
        (colimit.ι (H ⋙ obj (evaluation K C) k) j :
          (H ⋙ obj (evaluation K C) k).obj j ⟶ colimit (H ⋙ obj (evaluation K C) k))
        (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ f : colimit (H ⋙ obj (evaluation K C) k) ⟶ W) =
      CategoryStruct.comp (Y := colimit (H ⋙ obj (evaluation K C) k))
        (colimit.ι (H ⋙ obj (evaluation K C) k) j :
          (H ⋙ obj (evaluation K C) k).obj j ⟶ colimit (H ⋙ obj (evaluation K C) k))
        (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ g : colimit (H ⋙ obj (evaluation K C) k) ⟶ W)
⊢ Eq (α := colimit (H ⋙ obj (evaluation K C) k) ⟶ W)
    (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ f : colimit (H ⋙ obj (evaluation K C) k) ⟶ W)
    (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ g : colimit (H ⋙ obj (evaluation K C) k) ⟶ W)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), NatTrans.app (colimit.ι H j) k ≫ f = NatTrans.app (colimit.ι H j) k ≫ g
j : J
⊢ CategoryStruct.comp (Y := colimit (H ⋙ obj (evaluation K C) k))
      (colimit.ι (H ⋙ obj (evaluation K C) k) j :
        (H ⋙ obj (evaluation K C) k).obj j ⟶ colimit (H ⋙ obj (evaluation K C) k))
      (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ f : colimit (H ⋙ obj (evaluation K C) k) ⟶ W) =
    CategoryStruct.comp (Y := colimit (H ⋙ obj (evaluation K C) k))
      (colimit.ι (H ⋙ obj (evaluation K C) k) j :
        (H ⋙ obj (evaluation K C) k).obj j ⟶ colimit (H ⋙ obj (evaluation K C) k))
      (Iso.inv (colimitObjIsoColimitCompEvaluation H k) ≫ g : colimit (H ⋙ obj (evaluation K C) k) ⟶ W)

Tactic:
simpa using w j
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v', v₂, u', u₂} D K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
j : J
w :
  ∀ (d : D),
    Eq (α := ((F ⋙ obj (whiskeringLeft D K C) G).obj j).obj d ⟶ (G ⋙ colimit F).obj d)
      (NatTrans.app
          (CategoryStruct.comp (Y := colimit (F ⋙ obj (whiskeringLeft D K C) G))
            (colimit.ι (F ⋙ obj (whiskeringLeft D K C) G) j :
              (F ⋙ obj (whiskeringLeft D K C) G).obj j ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G))
            (Iso.hom (colimitCompWhiskeringLeftIsoCompColimit F G) :
              colimit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ colimit F))
          d :
        ((F ⋙ obj (whiskeringLeft D K C) G).obj j).obj d ⟶ (G ⋙ colimit F).obj d)
      (NatTrans.app (G.whiskerLeft (colimit.ι F j)) d :
        ((F ⋙ obj (whiskeringLeft D K C) G).obj j).obj d ⟶ (G ⋙ colimit F).obj d)
⊢ Eq (α := (F ⋙ obj (whiskeringLeft D K C) G).obj j ⟶ G ⋙ colimit F)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (whiskeringLeft D K C) G))
        (colimit.ι (F ⋙ obj (whiskeringLeft D K C) G) j :
          (F ⋙ obj (whiskeringLeft D K C) G).obj j ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G))
        (Iso.hom (colimitCompWhiskeringLeftIsoCompColimit F G) :
          colimit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ colimit F) :
      (F ⋙ obj (whiskeringLeft D K C) G).obj j ⟶ G ⋙ colimit F)
    (G.whiskerLeft (colimit.ι F j) : G ⋙ F.obj j ⟶ G ⋙ colimit F)

Tactic:
ext d
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v', v₂, u', u₂} D K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
j : J
d : D
⊢ Eq (α := ((F ⋙ obj (whiskeringLeft D K C) G).obj j).obj d ⟶ (G ⋙ colimit F).obj d)
    (NatTrans.app
        (CategoryStruct.comp (Y := colimit (F ⋙ obj (whiskeringLeft D K C) G))
          (colimit.ι (F ⋙ obj (whiskeringLeft D K C) G) j :
            (F ⋙ obj (whiskeringLeft D K C) G).obj j ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G))
          (Iso.hom (colimitCompWhiskeringLeftIsoCompColimit F G) :
            colimit (F ⋙ obj (whiskeringLeft D K C) G) ⟶ G ⋙ colimit F))
        d :
      ((F ⋙ obj (whiskeringLeft D K C) G).obj j).obj d ⟶ (G ⋙ colimit F).obj d)
    (NatTrans.app (G.whiskerLeft (colimit.ι F j)) d :
      ((F ⋙ obj (whiskeringLeft D K C) G).obj j).obj d ⟶ (G ⋙ colimit F).obj d)

Tactic:
simp [colimitCompWhiskeringLeftIsoCompColimit]

Premises used: CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v', v₂, u', u₂} D K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
j : J
⊢ Eq (α := G ⋙ F.obj j ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G))
    (CategoryStruct.comp (Y := G ⋙ colimit F) (G.whiskerLeft (colimit.ι F j) : G ⋙ F.obj j ⟶ G ⋙ colimit F)
        (Iso.inv (colimitCompWhiskeringLeftIsoCompColimit F G) :
          G ⋙ colimit F ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G)) :
      G ⋙ F.obj j ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G))
    (colimit.ι (F ⋙ obj (whiskeringLeft D K C) G) j :
      (F ⋙ obj (whiskeringLeft D K C) G).obj j ⟶ colimit (F ⋙ obj (whiskeringLeft D K C) G))

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesLimit G (F ⋙ obj (evaluation K C) k)
c : Cone G
hc : IsLimit c
t : (k : K) → IsLimit (F := (G ⋙ F) ⋙ obj (evaluation K C) k) (mapCone (obj (evaluation K C) k) (F.mapCone c))
⊢ IsLimit (F.mapCone c)

Tactic:
apply evaluationJointlyReflectsLimits

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesLimit G (F ⋙ obj (evaluation K C) k)
c : Cone G
hc : IsLimit c
X : K
⊢ PreservesLimit G (F ⋙ obj (evaluation K C) X)

Tactic:
haveI := H X
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesLimit G (F ⋙ obj (evaluation K C) k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ obj (evaluation K C) X)
t : IsLimit ((F ⋙ obj (evaluation K C) X).mapCone c)
⊢ IsLimit (F := (G ⋙ F) ⋙ obj (evaluation K C) X) (mapCone (obj (evaluation K C) X) (F.mapCone c))

Tactic:
change IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.IsLimit, CategoryTheory.evaluation, CategoryTheory.Functor.mapCone, CategoryTheory.Functor.obj