awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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 (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)
have 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)
Tactic: dsimp [colimitObjIsoColimitCompEvaluation]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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 (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))
have 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)
Tactic: dsimp [colimitObjIsoColimitCompEvaluation]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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 (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)
have 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))
Tactic: rw [← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
⊢ 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)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
⊢ Eq (α := (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (colimitObjIsoColimitCompEvaluation F i) : (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) i))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
have rw : Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
  (CategoryStruct.comp (Y := (colimit F).obj i)
      (Iso.inv (colimitObjIsoColimitCompEvaluation F i) : colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj i)
      ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
        (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
    colimit (F ⋙ obj (evaluation K C) i) ⟶ 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))
Tactic: rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv,
    colimitObjIsoColimitCompEvaluation_inv_colimit_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
rw :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := (colimit F).obj i)
        (Iso.inv (colimitObjIsoColimitCompEvaluation F i) : colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj i)
        ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
          (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ 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))
⊢ Eq (α := (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (colimitObjIsoColimitCompEvaluation F i) : (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) i))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
have rw₁ : Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
  ((Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f) ≫
      Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
    colimit (F ⋙ obj (evaluation K C) i) ⟶ 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))
Tactic: rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv,
    colimitObjIsoColimitCompEvaluation_inv_colimit_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
rw :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := (colimit F).obj i)
        (Iso.inv (colimitObjIsoColimitCompEvaluation F i) : colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj i)
        ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
          (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ 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))
rw₁ :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    ((Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f) ≫
        Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ 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))
⊢ Eq (α := (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (colimitObjIsoColimitCompEvaluation F i) : (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) i))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
have rw₂ : 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: rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv,
    colimitObjIsoColimitCompEvaluation_inv_colimit_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
⊢ f = g
have 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)
Tactic: apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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 (α := (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)
have 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)
Tactic: ext d
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
⊢ IsLimit (F.mapCone c)
have t : (k : K) → IsLimit (F := (G ⋙ F) ⋙ obj (evaluation K C) k) (mapCone (obj (evaluation K C) k) (F.mapCone c))
Tactic: apply evaluationJointlyReflectsLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (hypothesis)
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
⊢ IsLimit (F := (G ⋙ F) ⋙ obj (evaluation K C) X) (mapCone (obj (evaluation K C) X) (F.mapCone c))
have this : PreservesLimit G (F ⋙ obj (evaluation K C) X)
Tactic: haveI := H X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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)
⊢ IsLimit (F := (G ⋙ F) ⋙ obj (evaluation K C) X) (mapCone (obj (evaluation K C) X) (F.mapCone c))
have t : IsLimit ((F ⋙ obj (evaluation K C) X).mapCone c)
Tactic: change IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
⊢ IsColimit (F.mapCocone c)
have t : (k : K) → IsColimit (F := (G ⋙ F) ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) (F.mapCocone c))
Tactic: apply evaluationJointlyReflectsColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (hypothesis)
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), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
X : K
⊢ IsColimit (F := (G ⋙ F) ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) (F.mapCocone c))
have this : PreservesColimit G (F ⋙ obj (evaluation K C) X)
Tactic: haveI := H X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
X : K
this : PreservesColimit G (F ⋙ obj (evaluation K C) X)
⊢ IsColimit (F := (G ⋙ F) ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) (F.mapCocone c))
have t : IsColimit ((F ⋙ obj (evaluation K C) X).mapCocone c)
Tactic: change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
⊢ Eq (α := obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F ⟶ obj lim G)
    (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
      Iso.hom
        ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) G))
    (Iso.hom
        ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) F) ≫
      map lim η)
have w : ∀ (k : K),
  Eq (α :=
    (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶ (obj lim G).obj k)
    (NatTrans.app
      (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
        Iso.hom
          ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) G))
      k)
    (NatTrans.app
      (Iso.hom
          ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) F) ≫
        map lim η)
      k)
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
k : K
⊢ Eq (α :=
    (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶ (obj lim G).obj k)
    (NatTrans.app
      (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
        Iso.hom
          ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) G))
      k)
    (NatTrans.app
      (Iso.hom
          ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) F) ≫
        map lim η)
      k)
have w : ∀ (j : J),
  Eq (α :=
    (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶ (G.obj j).obj k)
    (CategoryStruct.comp (Y := (limit G).obj k)
      (NatTrans.app
        (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
          Iso.hom
            ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
              G))
        k)
      (NatTrans.app (limit.π G j) k))
    (CategoryStruct.comp (Y := (limit G).obj k)
      (NatTrans.app
          (Iso.hom
              ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
                F) ≫
            map lim η)
          k :
        (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
          (obj lim G).obj k)
      (NatTrans.app (limit.π G j) k))
Tactic: apply limit_obj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
⊢ Eq (α := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F ⟶ obj (flipFunctor K J C ⋙ lim) G)
    (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
      Iso.hom
        ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) G))
    (Iso.hom
        ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) F) ≫
      map (flipFunctor K J C ⋙ lim) η)
have w : ∀ (k : K),
  Eq (α :=
    (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
      (obj (flipFunctor K J C ⋙ lim) G).obj k)
    (NatTrans.app
      (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
        Iso.hom
          ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) G))
      k)
    (NatTrans.app
      (Iso.hom
          ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) F) ≫
        map (flipFunctor K J C ⋙ lim) η)
      k)
Tactic: ext k