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
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
c : Cocone F
t : (k : K) → IsColimit (F := F ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (F.obj j).map f ≫
      (c.ι.app j).app Y ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) } =
    { pt := s.pt.obj X, ι := whiskerRight s.ι (obj (evaluation K C) X) : Cocone (F ⋙ obj (evaluation K C) X) }.ι.app j ≫
      s.pt.map f
have erw : (F.obj j).map f ≫
    { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) : Cocone (F ⋙ obj (evaluation K C) Y) }.ι.app j =
  { pt := s.pt.obj X, ι := whiskerRight s.ι (obj (evaluation K C) X) : Cocone (F ⋙ obj (evaluation K C) X) }.ι.app j ≫
    s.pt.map f
Tactic: erw [(t Y).fac ⟨s.pt.obj _, whiskerRight s.ι _⟩ 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
c : Cocone F
t : (k : K) → IsColimit (F := F ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
        naturality := ⋯ } =
    s.ι.app j
have w : ∀ (k : K),
  NatTrans.app
      (c.ι.app j ≫
        { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
          naturality := sorry })
      k =
    (s.ι.app j).app 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
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : Cocone F
t : (k : K) → IsColimit (F := F ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) c)
s : Cocone F
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m =
    { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
      naturality := ⋯ }
have w₁ : ∀ (x : K),
  m.app x =
    NatTrans.app
      { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
        naturality := sorry }
      x
Tactic: ext 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 : J ⥤ Functor.{v₂, v, u₂, u} K C
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
⊢ Eq (α :=
    F.obj j₁ ⟶
      obj
        (obj (const J)
          { obj := fun (k : K) ↦ (c k).cocone.pt,
            map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
              (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι },
            map_id := ⋯, map_comp := ⋯ })
        j₂)
    (F.map g ≫ { app := fun (k : K) ↦ (c k).cocone.ι.app j₂, naturality := ⋯ })
    ({ app := fun (k : K) ↦ (c k).cocone.ι.app j₁, naturality := ⋯ } ≫
      map
        (obj (const J)
          { obj := fun (k : K) ↦ (c k).cocone.pt,
            map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
              (c k₁).isColimit.desc
                { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι : Cocone (F.flip.obj k₁) },
            map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
        g)
have w : ∀ (k : K),
  Eq (α :=
    (F.obj j₁).obj k ⟶
      obj.{v₂, v, u₂, u}
        (obj
          (obj (const J)
            { obj := fun (k : K) ↦ (c k).cocone.pt,
              map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι },
              map_id := sorry, map_comp := sorry })
          j₂)
        k)
    (NatTrans.app (F.map g ≫ { app := fun (k : K) ↦ (c k).cocone.ι.app j₂, naturality := sorry }) k)
    (NatTrans.app
      ({ app := fun (k : K) ↦ (c k).cocone.ι.app j₁, naturality := sorry } ≫
        map
          (obj (const J)
            { obj := fun (k : K) ↦ (c k).cocone.pt,
              map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                (c k₁).isColimit.desc
                  { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι : Cocone (F.flip.obj k₁) },
              map_id := sorry, map_comp := sorry : Functor.{v₂, v, u₂, u} K C })
          g)
      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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
X Y : J
f : X ⟶ Y
⊢ Eq (α := F.obj X ⟶ obj (obj (const J) (F.flip ⋙ colim)) Y)
    (F.map f ≫ { app := fun (Y_1 : K) ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := ⋯ })
    ({ app := fun (Y : K) ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ map (obj (const J) (F.flip ⋙ colim)) f)
have w : ∀ (x : K),
  Eq (α := (F.obj X).obj x ⟶ (obj (obj (const J) (F.flip ⋙ colim)) Y).obj x)
    (NatTrans.app (F.map f ≫ { app := fun (Y_1 : K) ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := sorry }) x)
    (NatTrans.app
      ({ app := fun (Y : K) ↦ colimit.ι (F.flip.obj Y) X, naturality := sorry } ≫ map (obj (const J) (F.flip ⋙ colim)) f) x)
Tactic: ext 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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
X Y : J
f : X ⟶ Y
x : K
⊢ Eq (α := (F.obj X).obj x ⟶ (obj (obj (const J) (F.flip ⋙ colim)) Y).obj x)
    (NatTrans.app (F.map f ≫ { app := fun (Y_1 : K) ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := ⋯ }) x)
    (NatTrans.app
      ({ app := fun (Y : K) ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ map (obj (const J) (F.flip ⋙ colim)) f) x)
have w : Eq (α := (F.obj X).obj x ⟶ colimit (F.flip.obj x)) ((F.map f).app x ≫ colimit.ι (F.flip.obj x) Y)
  (colimit.ι (F.flip.obj x) X)
Tactic: simp only [Functor.const_obj_obj, Functor.comp_obj, colim_obj, NatTrans.comp_app,
        Functor.const_obj_map, Category.comp_id]
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
X Y : J
f : X ⟶ Y
x : K
⊢ Eq (α := (F.obj X).obj x ⟶ colimit (F.flip.obj x)) ((F.map f).app x ≫ colimit.ι (F.flip.obj x) Y)
    (colimit.ι (F.flip.obj x) X)
have w : Eq (α := (F.flip.obj x).obj X ⟶ colimit (F.flip.obj x)) ((F.flip.obj x).map f ≫ colimit.ι (F.flip.obj x) Y)
  (colimit.ι (F.flip.obj x) X)
Tactic: change (F.flip.obj x).map f ≫ _ = _
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
X Y : J
f : X ⟶ Y
x : K
⊢ Eq (α := (F.flip.obj x).obj X ⟶ colimit (F.flip.obj x)) ((F.flip.obj x).map f ≫ colimit.ι (F.flip.obj x) Y)
    (colimit.ι (F.flip.obj x) X)
have w : Eq (α := (F.flip.obj x).obj X ⟶ colimit (F.flip.obj x)) (colimit.ι (F.flip.obj x) X) (colimit.ι (F.flip.obj x) X)
Tactic: rw [colimit.w]
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
⊢ IsColimit (pointwiseCocone F)
have apply : (combineCocones F fun (k : K) ↦
    { cocone := colimit.cocone (F.flip.obj k), isColimit := colimit.isColimit (F.flip.obj k) :
      ColimitCocone (F.flip.obj k) }) ≅
  pointwiseCocone F
Tactic: apply IsColimit.ofIsoColimit (combinedIsColimit _
    (fun k ↦ ⟨colimit.cocone _, colimit.isColimit _⟩))
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
⊢ Eq (α := (limit F).obj k ⟶ (F ⋙ obj (evaluation K C) k).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) k))
        (Iso.hom (limitObjIsoLimitCompEvaluation F k) : (limit F).obj k ⟶ limit (F ⋙ obj (evaluation K C) k))
        (limit.π (F ⋙ obj (evaluation K C) k) j :
          limit (F ⋙ obj (evaluation K C) k) ⟶ (F ⋙ obj (evaluation K C) k).obj j) :
      (limit F).obj k ⟶ (F ⋙ obj (evaluation K C) k).obj j)
    (NatTrans.app (limit.π F j) k : (limit F).obj k ⟶ (F.obj j).obj k)
have dsimp : Eq (α := (limit F).obj k ⟶ (F.obj j).obj k)
  (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) k))
    (Iso.hom (preservesLimitIso (obj (evaluation K C) k) F)) (limit.π (F ⋙ obj (evaluation K C) k) j))
  (NatTrans.app (limit.π F j) k)
Tactic: dsimp [limitObjIsoLimitCompEvaluation]
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
⊢ Eq (α := limit (F ⋙ obj (evaluation K C) k) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := (limit F).obj k)
        (Iso.inv (limitObjIsoLimitCompEvaluation F k) : limit (F ⋙ obj (evaluation K C) k) ⟶ (limit F).obj k)
        (NatTrans.app (limit.π F j) k : (limit F).obj k ⟶ (F.obj j).obj k) :
      limit (F ⋙ obj (evaluation K C) k) ⟶ (F.obj j).obj k)
    (limit.π (F ⋙ obj (evaluation K C) k) j : limit (F ⋙ obj (evaluation K C) k) ⟶ (F ⋙ obj (evaluation K C) k).obj j)
have dsimp : Eq (α := limit (F ⋙ obj (evaluation K C) k) ⟶ (F.obj j).obj k)
  (CategoryStruct.comp (Y := (limit F).obj k) (Iso.inv (preservesLimitIso (obj (evaluation K C) k) F))
      (NatTrans.app (limit.π F j) k) :
    limit (F ⋙ obj (evaluation K C) k) ⟶ (F.obj j).obj k)
  (limit.π (F ⋙ obj (evaluation K C) k) j : limit (F ⋙ obj (evaluation K C) k) ⟶ (F ⋙ obj (evaluation K C) k).obj j)
Tactic: dsimp [limitObjIsoLimitCompEvaluation]
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
⊢ Eq (α := limit (F ⋙ obj (evaluation K C) k) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := (limit F).obj k) (Iso.inv (preservesLimitIso (obj (evaluation K C) k) F))
        (NatTrans.app (limit.π F j) k) :
      limit (F ⋙ obj (evaluation K C) k) ⟶ (F.obj j).obj k)
    (limit.π (F ⋙ obj (evaluation K C) k) j : limit (F ⋙ obj (evaluation K C) k) ⟶ (F ⋙ obj (evaluation K C) k).obj j)
have rw : Eq (α := (limit F).obj k ⟶ (F.obj j).obj k) (NatTrans.app (limit.π F j) k)
  (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) k))
    (Iso.hom (preservesLimitIso (obj (evaluation K C) k) F)) (limit.π (F ⋙ obj (evaluation K C) k) j))
Tactic: rw [Iso.inv_comp_eq]
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
⊢ Eq (α := (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    ((limit F).map f ≫ Iso.hom (limitObjIsoLimitCompEvaluation F j) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
have w : ∀ (j_1 : J),
  CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
      ((limit F).map f ≫ Iso.hom (limitObjIsoLimitCompEvaluation F j) :
        (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
      (limit.π (F ⋙ obj (evaluation K C) j) j_1 :
        limit (F ⋙ obj (evaluation K C) j) ⟶ (F ⋙ obj (evaluation K C) j).obj j_1) =
    CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
      (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)))
      (limit.π (F ⋙ obj (evaluation K C) j) j_1)
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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
⊢ Eq (α := limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (Iso.inv (limitObjIsoLimitCompEvaluation F i) ≫ (limit F).map f :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
have rw : (limit F).map f =
  CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
    (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv,
    limit_map_limitObjIsoLimitCompEvaluation_hom]
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
rw :
  (limit F).map f =
    CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
      (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
      (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
          (limMap (F.whiskerLeft (map (evaluation K C) f)) :
            limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
          (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
        limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
⊢ Eq (α := limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (Iso.inv (limitObjIsoLimitCompEvaluation F i) ≫ (limit F).map f :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
have rw₁ : (limit F).map f =
  CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv,
    limit_map_limitObjIsoLimitCompEvaluation_hom]
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
rw :
  (limit F).map f =
    CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
      (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
      (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
          (limMap (F.whiskerLeft (map (evaluation K C) f)) :
            limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
          (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
        limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
rw₁ :
  (limit F).map f =
    CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
      (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
          (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
          (limMap (F.whiskerLeft (map (evaluation K C) f)) :
            limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
        (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
      (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j)
⊢ Eq (α := limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (Iso.inv (limitObjIsoLimitCompEvaluation F i) ≫ (limit F).map f :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
have rw₂ : Eq (α := (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
  ((limit F).map f ≫ Iso.hom (limitObjIsoLimitCompEvaluation F j) :
    (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
  (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
      (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
      (limMap (F.whiskerLeft (map (evaluation K C) f)) :
        limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
    (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv,
    limit_map_limitObjIsoLimitCompEvaluation_hom]
-- 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 : 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
⊢ f = g
have apply : 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: apply (cancel_mono (limitObjIsoLimitCompEvaluation H k).hom).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 : 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
⊢ 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))
have 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)
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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
j : J
⊢ 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)
have 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)
Tactic: ext d