awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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 := ⋯ }
      x

Tactic:
exact (t x).hom_ext fun j =>
      (congr_app (w j) x).trans
        ((t x).fac ⟨s.pt.obj _, whiskerRight s.ι ((evaluation K C).obj _)⟩ j).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.Cocone.ι, CategoryTheory.evaluation, Eq.symm, CategoryTheory.congr_app, CategoryTheory.Functor.obj, Eq.trans, CategoryTheory.Limits.Cocone.pt
-- 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
c : (k : K) → ColimitCocone (F.flip.obj k)
k : K
j : J
⊢ (c k).cocone.ι.app j ≫ (c k).isColimit.desc { pt := (c k).cocone.pt, ι := F.flip.map (𝟙 k) ≫ (c k).cocone.ι } =
    (c k).cocone.ι.app j ≫ 𝟙 (c k).cocone.pt

Tactic:
simp
-- 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
c : (k : K) → ColimitCocone (F.flip.obj k)
k₁ k₂ k₃ : K
f₁ : k₁ ⟶ k₂
f₂ : k₂ ⟶ k₃
j : J
⊢ Eq (α :=
    (F.flip.obj k₁).obj j ⟶
      { pt := (c k₃).cocone.pt, ι := F.flip.map (f₁ ≫ f₂) ≫ (c k₃).cocone.ι : Cocone (F.flip.obj k₁) }.pt)
    ((c k₁).cocone.ι.app j ≫
      (c k₁).isColimit.desc { pt := (c k₃).cocone.pt, ι := F.flip.map (f₁ ≫ f₂) ≫ (c k₃).cocone.ι })
    ((c k₁).cocone.ι.app j ≫
      CategoryStruct.comp (Y := (c k₂).cocone.pt)
        ((c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f₁ ≫ (c k₂).cocone.ι } :
          (c k₁).cocone.pt ⟶
            { pt := (c k₂).cocone.pt, ι := F.flip.map f₁ ≫ (c k₂).cocone.ι : Cocone (F.flip.obj k₁) }.pt)
        ((c k₂).isColimit.desc { pt := (c k₃).cocone.pt, ι := F.flip.map f₂ ≫ (c k₃).cocone.ι }))

Tactic:
simp
-- 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
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
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 := ⋯, map_comp := ⋯ })
            j₂)
          k)
      (NatTrans.app (F.map g ≫ { app := fun (k : K) ↦ (c k).cocone.ι.app j₂, naturality := ⋯ }) k)
      (NatTrans.app
        ({ 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)
        k)
⊢ 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)

Tactic:
ext k
-- 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
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
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 := ⋯, map_comp := ⋯ })
          j₂)
        k)
    (NatTrans.app (F.map g ≫ { app := fun (k : K) ↦ (c k).cocone.ι.app j₂, naturality := ⋯ }) k)
    (NatTrans.app
      ({ 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)
      k)

Tactic:
(c k).cocone.ι.naturality g

Premises used: CategoryTheory.Limits.ColimitCocone.cocone, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- 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
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
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 := ⋯, map_comp := ⋯ })
          j₂)
        k)
    (NatTrans.app (F.map g ≫ { app := fun (k : K) ↦ (c k).cocone.ι.app j₂, naturality := ⋯ }) k)
    (NatTrans.app
      ({ 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)
      k)

Tactic:
exact (c k).cocone.ι.naturality g

Premises used: CategoryTheory.Limits.ColimitCocone.cocone, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- 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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
X Y : J
f : X ⟶ Y
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 := ⋯ }) x)
      (NatTrans.app
        ({ app := fun (Y : K) ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ map (obj (const J) (F.flip ⋙ colim)) f)
        x)
⊢ 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)

Tactic:
ext 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
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
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)
⊢ 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)

Tactic:
simp only [Functor.const_obj_obj, Functor.comp_obj, colim_obj, NatTrans.comp_app,
        Functor.const_obj_map, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id, CategoryTheory.Limits.colim_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.const_obj_map
-- 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
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
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)
⊢ 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:
change (F.flip.obj x).map f ≫ _ = _

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- 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
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
w 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)
⊢ 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:
rw [colimit.w]

Premises used: CategoryTheory.Limits.colimit.w
-- 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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
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
⊢ IsColimit (pointwiseCocone F)

Tactic:
apply IsColimit.ofIsoColimit (combinedIsColimit _
    (fun k ↦ ⟨colimit.cocone _, colimit.isColimit _⟩))

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.combinedIsColimit, CategoryTheory.Functor.obj
-- 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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
⊢ (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:
exact Cocone.ext (Iso.refl _)

Premises used: CategoryTheory.Limits.Cocone.ext, 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), HasLimit (F.flip.obj k)
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := combineCones F fun _ => getLimitCone _
      isLimit := combinedIsLimit _ _ }

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Limits.combineCones, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.combinedIsLimit, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Functor.obj
-- 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)
⊢ HasColimit F

Tactic:
HasColimit.mk
    { cocone := combineCocones F fun _ => getColimitCocone _
      isColimit := combinedIsColimit _ _ }

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Limits.combineCocones, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.getColimitCocone, CategoryTheory.Limits.combinedIsColimit, CategoryTheory.Functor.obj
-- 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 : HasLimit (F.flip.obj k)
⊢ HasLimit (F ⋙ obj (evaluation K C) k)

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

Premises used: CategoryTheory.Limits.hasLimit_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), HasLimit (F.flip.obj k)
k : K
⊢ PreservesLimit F (obj (evaluation K C) k)

Tactic:
let X : (k : K) → LimitCone (F.flip.obj k) := fun k => getLimitCone (F.flip.obj k)
  preservesLimit_of_preserves_limit_cone (combinedIsLimit _ X) <|
    IsLimit.ofIsoLimit (limit.isLimit _) (evaluateCombinedCones F X k).symm

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Limits.evaluateCombinedCones, CategoryTheory.Functor.comp, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Iso.symm, CategoryTheory.Limits.combinedIsLimit, CategoryTheory.evaluation, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Functor.obj
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
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)
⊢ 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)

Tactic:
dsimp [limitObjIsoLimitCompEvaluation]

Premises used: CategoryTheory.Limits.limitObjIsoLimitCompEvaluation
-- 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 : 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 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:
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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
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)
⊢ 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)

Tactic:
dsimp [limitObjIsoLimitCompEvaluation]

Premises used: CategoryTheory.Limits.limitObjIsoLimitCompEvaluation
-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
j : J
k : K
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))
⊢ 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:
rw [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
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 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:
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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
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)
⊢ 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:
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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
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:
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 : 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
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))
⊢ f = g

Tactic:
apply (cancel_mono (limitObjIsoLimitCompEvaluation H k).hom).1

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation, Iff.mp, CategoryTheory.Iso.hom