awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPullbacks.{v₁, u₁} C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ Eq (α := pullback (f.app d) (g.app d) ⟶ G.obj d)
    (CategoryStruct.comp (Y := (pullback f g).obj d)
        (Iso.inv (pullbackObjIso f g d) : pullback (f.app d) (g.app d) ⟶ (pullback f g).obj d)
        (NatTrans.app (pullback.snd f g) d : (pullback f g).obj d ⟶ G.obj d) :
      pullback (f.app d) (g.app d) ⟶ G.obj d)
    (pullback.snd (f.app d) (g.app d) : pullback (f.app d) (g.app d) ⟶ G.obj d)

Tactic:
simp [pullbackObjIso]

Premises used: CategoryTheory.Limits.pullbackObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPushouts.{v₁, u₁} C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ Eq (α := G.obj d ⟶ pushout (f.app d) (g.app d))
    (CategoryStruct.comp (Y := (pushout f g).obj d) (NatTrans.app (pushout.inl f g) d : G.obj d ⟶ (pushout f g).obj d)
        (Iso.hom (pushoutObjIso f g d) : (pushout f g).obj d ⟶ pushout (f.app d) (g.app d)) :
      G.obj d ⟶ pushout (f.app d) (g.app d))
    (pushout.inl (f.app d) (g.app d) : G.obj d ⟶ pushout (f.app d) (g.app d))

Tactic:
simp [pushoutObjIso]

Premises used: CategoryTheory.Limits.pushoutObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPushouts.{v₁, u₁} C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ Eq (α := H.obj d ⟶ pushout (f.app d) (g.app d))
    (CategoryStruct.comp (Y := (pushout f g).obj d) (NatTrans.app (pushout.inr f g) d : H.obj d ⟶ (pushout f g).obj d)
        (Iso.hom (pushoutObjIso f g d) : (pushout f g).obj d ⟶ pushout (f.app d) (g.app d)) :
      H.obj d ⟶ pushout (f.app d) (g.app d))
    (pushout.inr (f.app d) (g.app d) : H.obj d ⟶ pushout (f.app d) (g.app d))

Tactic:
simp [pushoutObjIso]

Premises used: CategoryTheory.Limits.pushoutObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPushouts.{v₁, u₁} C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ Eq (α := G.obj d ⟶ (pushout f g).obj d)
    (CategoryStruct.comp (Y := pushout (f.app d) (g.app d))
        (pushout.inl (f.app d) (g.app d) : G.obj d ⟶ pushout (f.app d) (g.app d))
        (Iso.inv (pushoutObjIso f g d) : pushout (f.app d) (g.app d) ⟶ (pushout f g).obj d) :
      G.obj d ⟶ (pushout f g).obj d)
    (NatTrans.app (pushout.inl f g) d : G.obj d ⟶ (pushout f g).obj d)

Tactic:
simp [pushoutObjIso]

Premises used: CategoryTheory.Limits.pushoutObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPushouts.{v₁, u₁} C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ Eq (α := H.obj d ⟶ (pushout f g).obj d)
    (CategoryStruct.comp (Y := pushout (f.app d) (g.app d))
        (pushout.inr (f.app d) (g.app d) : H.obj d ⟶ pushout (f.app d) (g.app d))
        (Iso.inv (pushoutObjIso f g d) : pushout (f.app d) (g.app d) ⟶ (pushout f g).obj d) :
      H.obj d ⟶ (pushout f g).obj d)
    (NatTrans.app (pushout.inr f g) d : H.obj d ⟶ (pushout f g).obj d)

Tactic:
simp [pushoutObjIso]

Premises used: CategoryTheory.Limits.pushoutObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : (X : C) → IsTerminal.{v_2, u_2} (F.obj X)
refine :
  (X : C) →
    Iso (C :=
      Cone.{0, v_2, 0, u_2}
        (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
          (obj (evaluation C D) X)))
      (obj
        (Cone.postcompose
          (Iso.hom
            (emptyExt (empty D)
              (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
                (obj (evaluation C D) X)))))
        (asEmptyCone (F.obj X)))
      (mapCone (obj (evaluation C D) X) (asEmptyCone F))
⊢ IsTerminal F

Tactic:
refine evaluationJointlyReflectsLimits _
    fun X ↦ IsLimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits, CategoryTheory.Functor.emptyExt, CategoryTheory.Functor.comp, CategoryTheory.Functor.empty, CategoryTheory.Limits.asEmptyCone, CategoryTheory.evaluation, CategoryTheory.Functor.mapCone, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : (X : C) → IsTerminal.{v_2, u_2} (F.obj X)
X : C
⊢ Iso (C :=
    Cone.{0, v_2, 0, u_2}
      (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
        (obj (evaluation C D) X)))
    (obj
      (Cone.postcompose
        (Iso.hom
          (emptyExt (empty D)
            (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
              (obj (evaluation C D) X)))))
      (asEmptyCone (F.obj X)))
    (mapCone (obj (evaluation C D) X) (asEmptyCone F))

Tactic:
exact Cone.ext (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : (X : C) → IsInitial.{v_2, u_2} (F.obj X)
refine :
  (X : C) →
    Iso (C :=
      Cocone.{0, v_2, 0, u_2}
        (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
          (obj (evaluation C D) X)))
      (obj
        (Cocone.precompose
          (Iso.inv
            (emptyExt (empty D)
              (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
                (obj (evaluation C D) X)))))
        (asEmptyCocone (F.obj X)))
      (mapCocone (obj (evaluation C D) X) (asEmptyCocone F))
⊢ IsInitial F

Tactic:
refine evaluationJointlyReflectsColimits _
    fun X ↦ IsColimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits, CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Functor.emptyExt, CategoryTheory.Functor.comp, CategoryTheory.Functor.empty, CategoryTheory.Limits.asEmptyCocone, CategoryTheory.evaluation, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : (X : C) → IsInitial.{v_2, u_2} (F.obj X)
X : C
⊢ Iso (C :=
    Cocone.{0, v_2, 0, u_2}
      (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
        (obj (evaluation C D) X)))
    (obj
      (Cocone.precompose
        (Iso.inv
          (emptyExt (empty D)
            (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
              (obj (evaluation C D) X)))))
      (asEmptyCocone (F.obj X)))
    (mapCocone (obj (evaluation C D) X) (asEmptyCocone F))

Tactic:
exact Cocone.ext (Iso.refl _)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.FunctorToTypes
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, w, u₂, w + 1} K (Type w)
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst_2 : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
  (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t) :=
  isColimitOfPreserves (Functor.obj (evaluation K (Type w)) k) h
obtain :
  ∀ (j : J) (y : (F ⋙ Functor.obj (evaluation K (Type w)) k).obj j),
    ∃ (j_1 : J) (y_1 : (fun (X : Type w) ↦ X) ((F.obj j_1).obj k)),
      Eq (α := t.pt.obj k)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)) j) :
              (a : (fun (X : Type w) ↦ X) ((F ⋙ (evaluation K (Type w)).obj k).obj j)) →
                (fun (X : Type w) ↦ X) (((Functor.const J).obj (((evaluation K (Type w)).obj k).mapCocone t).pt).obj j))
            y :
          (fun (X : Type w) ↦ X)
            (Functor.obj.{v₁, w, u₁, w + 1}
              (Functor.obj (Functor.const J)
                (Cocone.pt (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
                  (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)))
              j))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((t.ι.app j_1).app k) :
              (a : (fun (X : Type w) ↦ X) ((F.obj j_1).obj k)) →
                (fun (X : Type w) ↦ X) ((((Functor.const J).obj t.pt).obj j_1).obj k))
            y_1 :
          (fun (X : Type w) ↦ X) ((Functor.obj (Functor.obj (Functor.const J) t.pt) j_1).obj k))
⊢ ∃ (j : J) (y : (fun (X : Type w) ↦ X) ((F.obj j).obj k)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((t.ι.app j).app k) :
          (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k)) →
            (fun (X : Type w) ↦ X) ((((Functor.const J).obj t.pt).obj j).obj k))
        y

Tactic:
obtain ⟨j, y, rfl⟩ := Types.jointly_surjective _ hev x

Premises used: CategoryTheory.Limits.Types.jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.FunctorToTypes
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, w, u₂, w + 1} K (Type w)
k : K
t : Cocone F
h : IsColimit t
inst_2 : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
  (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t) :=
  isColimitOfPreserves (Functor.obj (evaluation K (Type w)) k) h
j : J
y : (F ⋙ Functor.obj (evaluation K (Type w)) k).obj j
⊢ Eq (α := t.pt.obj k)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)) j) :
          (a : (fun (X : Type w) ↦ X) ((F ⋙ (evaluation K (Type w)).obj k).obj j)) →
            (fun (X : Type w) ↦ X) (((Functor.const J).obj (((evaluation K (Type w)).obj k).mapCocone t).pt).obj j))
        y :
      (fun (X : Type w) ↦ X)
        (Functor.obj.{v₁, w, u₁, w + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
              (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)))
          j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((t.ι.app j).app k) :
          (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k)) →
            (fun (X : Type w) ↦ X) ((((Functor.const J).obj t.pt).obj j).obj k))
        y :
      (fun (X : Type w) ↦ X) ((Functor.obj (Functor.obj (Functor.const J) t.pt) j).obj k))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorToTypes
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, w, u₂, w + 1} K (Type w)
k : K
t : Cocone F
h : IsColimit t
inst_2 : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
  (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t) :=
  isColimitOfPreserves (Functor.obj (evaluation K (Type w)) k) h
j : J
y : (F ⋙ Functor.obj (evaluation K (Type w)) k).obj j
⊢ ∃ (j_1 : J) (y_1 : (fun (X : Type w) ↦ X) ((F.obj j_1).obj k)),
    Eq (α := t.pt.obj k)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)) j) :
            (a : (fun (X : Type w) ↦ X) ((F ⋙ (evaluation K (Type w)).obj k).obj j)) →
              (fun (X : Type w) ↦ X) (((Functor.const J).obj (((evaluation K (Type w)).obj k).mapCocone t).pt).obj j))
          y :
        (fun (X : Type w) ↦ X)
          (Functor.obj.{v₁, w, u₁, w + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
                (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)))
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((t.ι.app j_1).app k) :
            (a : (fun (X : Type w) ↦ X) ((F.obj j_1).obj k)) →
              (fun (X : Type w) ↦ X) ((((Functor.const J).obj t.pt).obj j_1).obj k))
          y_1 :
        (fun (X : Type w) ↦ X) ((Functor.obj (Functor.obj (Functor.const J) t.pt) j_1).obj k))

Tactic:
exact ⟨j, y, by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.FunctorToTypes
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, w, u₂, w + 1} K (Type w)
inst_2 : ∀ (k : K), HasColimit (F.flip.obj k)
k : K
x : (colimit F).obj k
⊢ ∃ (j : J) (y : (fun (X : Type w) ↦ X) ((F.obj j).obj k)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F j) k) :
          (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k)) → (fun (X : Type w) ↦ X) ((colimit F).obj k))
        y

Tactic:
jointly_surjective _ _ (colimit.isColimit _) x

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.FunctorToTypes.jointly_surjective
-- Module: Mathlib.CategoryTheory.Limits.FunctorToTypes
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, w, u₂, w + 1} K (Type w)
inst_2 : HasColimit F
j : J
k k' : K
f : k ⟶ k'
x : (fun (X : Type w) ↦ X) ((F.obj j).obj k)
⊢ Eq (α := (fun (X : Type w) ↦ X) ((colimit F).obj k'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((colimit F).map f) :
          (a : (fun (X : Type w) ↦ X) ((colimit F).obj k)) → (fun (X : Type w) ↦ X) ((colimit F).obj k'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F j) k) :
              (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k)) → (fun (X : Type w) ↦ X) ((colimit F).obj k))
            x :
          (fun (X : Type w) ↦ X) ((colimit F).obj k)) :
      (fun (X : Type w) ↦ X) ((colimit F).obj k'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F j) k') :
          (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k')) → (fun (X : Type w) ↦ X) ((colimit F).obj k'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj j).map f) :
              (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k)) → (fun (X : Type w) ↦ X) ((F.obj j).obj k'))
            x :
          (fun (X : Type w) ↦ X) ((F.obj j).obj k')) :
      (fun (X : Type w) ↦ X) ((colimit F).obj k'))

Tactic:
ConcreteCategory.congr_hom ((colimit.ι F j).naturality _).symm _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
d : LimitCone F
⊢ HasLimit F

Tactic:
⟨Nonempty.intro d⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk'
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
J : Type v
inst_2 : Category.{v, v} J
⊢ HasLimitsOfShape J C

Tactic:
HasLimitsOfSize.has_limits_of_shape J

Premises used: CategoryTheory.Limits.HasLimitsOfSize.has_limits_of_shape
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J_1 C
J : Type u₁
inst_3 : Category.{v₁, u₁} J
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₁, v, u₁, u} J C
⊢ HasLimit F

Tactic:
HasLimitsOfShape.has_limit F

Premises used: CategoryTheory.Limits.HasLimitsOfShape.has_limit
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J_1 C
J : Type u₁
inst_3 : Category.{v₁, u₁} J
inst_4 : HasLimitsOfSize.{v₁, u₁, v, u} C
⊢ HasLimitsOfShape.{v₁, u₁, v, u} J C

Tactic:
HasLimitsOfSize.has_limits_of_shape J

Premises used: CategoryTheory.Limits.HasLimitsOfSize.has_limits_of_shape
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
j j' : J
hj : j = j'
subst : F.obj j = F.obj j
⊢ F.obj j = F.obj j'

Tactic:
subst hj
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
j j' : J
hj : j = j'
subst : Eq (α := limit F ⟶ F.obj j) (π F j ≫ eqToHom ⋯) (π F j)
⊢ Eq (α := limit F ⟶ F.obj j') (π F j ≫ eqToHom ⋯) (π F j')

Tactic:
subst hj
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
j : J
⊢ Eq (α := limit F ⟶ F.obj j) (π F j ≫ eqToHom ⋯) (π F j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
⊢ (cone F).pt = limit F

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit, rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
⊢ (cone F).π.app = π F

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
j j' : J
f : j ⟶ j'
⊢ Eq (α := limit F ⟶ F.obj j') (π F j ≫ F.map f) (π F j')

Tactic:
(limit.cone F).w f

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.limit, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
c : Cone F
⊢ Eq (α := c.pt ⟶ (cone F).pt) (IsLimit.lift (isLimit F) c) (lift F c)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
c : Cone F
j : J
⊢ CategoryStruct.comp (Y := limit F) (lift F c) (π F j) = c.π.app j

Tactic:
IsLimit.fac _ c j

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
inst_3 : HasLimit G
α : F ⟶ G
j : J
⊢ Eq (α := limit F ⟶ G.obj j) (CategoryStruct.comp (Y := limit G) (limMap α) (limit.π G j)) (limit.π F j ≫ α.app j)

Tactic:
limit.lift_π _ j

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
c : Cone F
⊢ Eq (α := c.pt ⟶ (cone F).pt) (ConeMorphism.hom (coneMorphism c)) (lift F c)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
c : Cone F
j : J
⊢ CategoryStruct.comp (Y := (cone F).pt) (ConeMorphism.hom (coneMorphism c)) (π F j) = c.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ CategoryStruct.comp (Y := (cone F).pt) (Iso.hom (hc.conePointUniqueUpToIso (isLimit F))) (π F j) = c.π.app j

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ CategoryStruct.comp (Y := (cone F).pt) (Iso.inv (IsLimit.conePointUniqueUpToIso (isLimit F) hc)) (π F j) = c.π.app j

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
t : Cone F
⊢ ∃! l : t.pt ⟶ limit F, ∀ (j : J), l ≫ π F j = t.π.app j

Tactic:
(limit.isLimit F).existsUnique _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.existsUnique
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
t : LimitCone F
j : J
dsimp : Eq (α := limit F ⟶ F.obj j) (t.isLimit.lift (cone F) ≫ t.cone.π.app j) (π F j)
⊢ Eq (α := limit F ⟶ F.obj j) (Iso.hom (isoLimitCone t) ≫ t.cone.π.app j) (π F j)

Tactic:
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.limit.isoLimitCone
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
t : LimitCone F
j : J
⊢ Eq (α := limit F ⟶ F.obj j) (t.isLimit.lift (cone F) ≫ t.cone.π.app j) (π F j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
t : LimitCone F
j : J
dsimp : CategoryStruct.comp (Y := limit F) (lift F t.cone) (π F j) = t.cone.π.app j
⊢ CategoryStruct.comp (Y := limit F) (Iso.inv (isoLimitCone t)) (π F j) = t.cone.π.app j

Tactic:
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.limit.isoLimitCone
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
t : LimitCone F
j : J
⊢ CategoryStruct.comp (Y := limit F) (lift F t.cone) (π F j) = t.cone.π.app j

Tactic:
simp