awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
j : J
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (F.obj j)
hx :
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ModuleCat.Hom.hom (colimit.ι F j) : (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        (r • x) :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
j' : J
i : j ⟶ j'
h :
  Eq (α := (↑(F.obj j') : Type (max t w)))
    ((ModuleCat.Hom.hom (F.map i) : (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w))) (r • x) :
      (↑(F.obj j') : Type (max t w)))
    (0 : (↑(F.obj j') : Type (max t w)))
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))

Tactic:
simpa [elementwise_of% (colimit.w F), map_zero] using congr(colimit.ι F _
    $(H (IsFiltered.sup {j, j', j''} { ⟨j, j', by simp, by simp, i⟩ })
      (IsFiltered.toSup _ _ <| by simp)
      (F.map (IsFiltered.toSup _ _ <| by simp) x)
      (by rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp,
        ModuleCat.comp_apply, ← map_smul, ← map_smul, h, map_zero])))

Premises used: map_zero, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
c : Cone F
⊢ ∀ {Y Z : J} (g : Y ⟶ Z), c.π.app Y ≫ F.map (map (𝟭 J) g) = c.π.app Z

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₁, v₂, u₁, u₂} J K
X : C
F : Functor.{v₂, v₃, u₂, u₃} K C
f : (Y : J) → X ⟶ F.obj (G.obj Y)
h : ∀ {Y Z : J} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z
⊢ ∀ ⦃X_1 Y : J⦄ (f_1 : X_1 ⟶ Y), map (obj (const J) X) f_1 ≫ f Y = f X_1 ≫ (G ⋙ F).map f_1

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cone F
⊢ c.toStructuredArrow ⋙ StructuredArrow.proj c.pt F = 𝟭 J

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cone F
⊢ c.toStructuredArrow ⋙ StructuredArrow.toUnder c.pt F ⋙ Under.forget c.pt = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
c : Cone F
j : J
⊢ Under.hom (obj (obj (const J) (Under.mk (𝟙 c.pt))) j) ≫ c.π.app j =
    ((c.toStructuredArrow ⋙ StructuredArrow.toUnder c.pt F).obj j).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
inst_4 : HasLimit F
j : J
⊢ CategoryStruct.comp (Y := Under.right.{v₃, u₃} (obj (obj (const J) (Under.mk (𝟙 (limit F)))) j))
      (Under.hom (obj (obj (const J) (Under.mk (𝟙 (limit F)))) j)) (π F j) =
    ((toStructuredArrow F ⋙ StructuredArrow.toUnder (limit F) F).obj j).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : CostructuredArrow (const J) F
f : X ⟶ Y
j : J
⊢ (map (const J) f.left ≫ Y.hom).app j = (X.hom ≫ map (fromPUnit F) f.right).app j

Tactic:
congr_fun (congr_arg NatTrans.app f.w) j

Premises used: CategoryTheory.CommaMorphism.w, congr_arg, congr_fun, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : CostructuredArrow (const J) F
f : X ⟶ Y
j : J
h :
  ({ pt := X.left, π := X.hom : Cone F }.pt ⟶ F.obj j) =
      (obj.{v₁, v₃, u₁, u₃} (obj (const J) X.left) j ⟶ (obj (fromPUnit F) Y.right).obj j) →
    { pt := X.left, π := X.hom : Cone F }.π.app j = (X.hom ≫ map (fromPUnit F) f.right).app j
⊢ f.left ≫ { pt := Y.left, π := Y.hom : Cone F }.π.app j = { pt := X.left, π := X.hom }.π.app j

Tactic:
convert! congr_fun (congr_arg NatTrans.app f.w) j

Premises used: CategoryTheory.CommaMorphism.w, congr_arg, congr_fun, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : CostructuredArrow (const J) F
f : X ⟶ Y
j : J
e_1 :
  ({ pt := X.left, π := X.hom : Cone F }.pt ⟶ F.obj j) =
    (obj.{v₁, v₃, u₁, u₃} (obj (const J) X.left) j ⟶ (obj (fromPUnit F) Y.right).obj j)
⊢ { pt := X.left, π := X.hom : Cone F }.π.app j = (X.hom ≫ map (fromPUnit F) f.right).app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
⊢ HasLimit F ↔ HasTerminal (Cone F)

Tactic:
⟨fun _ => (Cone.isLimitEquivIsTerminal _ (limit.isLimit F)).hasTerminal, fun h =>
    haveI : HasTerminal (Cone F) := h
    ⟨⟨⟨⊤_ _, (Cone.isLimitEquivIsTerminal _).symm terminalIsTerminal⟩⟩⟩⟩

Premises used: CategoryTheory.Limits.Cone, CategoryTheory.Limits.Cone.isLimitEquivIsTerminal, CategoryTheory.Limits.limit.cone, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.terminal, CategoryTheory.Limits.HasLimit.mk', Iff.intro, CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.Limits.LimitCone.mk, Equiv.symm, CategoryTheory.Limits.terminalIsTerminal, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
⊢ HasLimitsOfShape.{v₁, u₁, v₃, u₃} J C ↔ IsLeftAdjoint (C := C) (D := Functor.{v₁, v₃, u₁, u₃} J C) (const J)

Tactic:
calc
    HasLimitsOfShape J C ↔ ∀ F : J ⥤ C, HasLimit F :=
      ⟨fun h => h.has_limit, fun h => HasLimitsOfShape.mk⟩
    _ ↔ ∀ F : J ⥤ C, HasTerminal (Cone F) := forall_congr' hasLimit_iff_hasTerminal_cone
    _ ↔ ∀ F : J ⥤ C, HasTerminal (CostructuredArrow (const J) F) :=
      (forall_congr' fun F => (Cone.equivCostructuredArrow F).hasTerminal_iff)
    _ ↔ (IsLeftAdjoint (const J : C ⥤ _)) :=
      isLeftAdjoint_iff_hasTerminal_costructuredArrow.symm

Premises used: CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone, CategoryTheory.Equivalence.hasTerminal_iff, Trans.trans, CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrow, CategoryTheory.Limits.HasLimitsOfShape.mk, Iff.intro, forall_congr', CategoryTheory.Limits.HasLimitsOfShape.has_limit, Iff.symm, CategoryTheory.Limits.Cone.equivCostructuredArrow
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cone F
hc : IsLimit c
s : Cone F
⊢ hc.liftConeMorphism s = IsTerminal.from ((c.isLimitEquivIsTerminal : (a : IsLimit c) → IsTerminal c) hc) s

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.IsLimit.liftConeMorphism, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cone F
hc : IsTerminal c
s : Cone F
⊢ hc.from s = IsLimit.liftConeMorphism ((c.isLimitEquivIsTerminal.symm : (a : IsTerminal c) → IsLimit c) hc) s

Tactic:
(IsLimit.liftConeMorphism_eq_isTerminal_from (c.isLimitEquivIsTerminal.symm hc) s).symm

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.Limits.IsTerminal.ofUnique, False.elim, CategoryTheory.Limits.Cone.isLimitEquivIsTerminal, CategoryTheory.Limits.IsLimit.liftConeMorphism, CategoryTheory.Limits.asEmptyCone, Equiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
c : Cocone F
⊢ ∀ {Y Z : J} (g : Y ⟶ Z), F.map (map (𝟭 J) g) ≫ c.ι.app Z = c.ι.app Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₁, v₂, u₁, u₂} J K
F : Functor.{v₂, v₃, u₂, u₃} K C
X : C
f : (Y : J) → F.obj (G.obj Y) ⟶ X
h : ∀ {Y Z : J} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y
⊢ ∀ ⦃X_1 Y : J⦄ (f_1 : X_1 ⟶ Y), (G ⋙ F).map f_1 ≫ f Y = f X_1 ≫ map (obj (const J) X) f_1

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cocone F
⊢ c.toCostructuredArrow ⋙ CostructuredArrow.proj F c.pt = 𝟭 J

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cocone F
⊢ c.toCostructuredArrow ⋙ CostructuredArrow.toOver F c.pt ⋙ Over.forget c.pt = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
c : Cocone F
j : J
⊢ c.ι.app j ≫ Over.hom (obj (obj (const J) (Over.mk (𝟙 c.pt))) j) =
    ((c.toCostructuredArrow ⋙ CostructuredArrow.toOver F c.pt).obj j).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
inst_4 : HasColimit F
j : J
⊢ Eq (α :=
    Over.left (X := colimit F) (obj (toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) j) ⟶ colimit F)
    (CategoryStruct.comp (Y := Over.left.{v₃, u₃} (obj (obj (const J) (Over.mk (𝟙 (colimit F)))) j)) (ι F j)
      (Over.hom (obj (obj (const J) (Over.mk (𝟙 (colimit F)))) j)))
    (Over.hom (obj (toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : StructuredArrow F (const J)
f : X ⟶ Y
j : J
⊢ { pt := X.right, ι := X.hom : Cocone F }.ι.app j ≫ StructuredArrow.Hom.right f = { pt := Y.right, ι := Y.hom }.ι.app j

Tactic:
simp [dsimp% congr_app f.w j]

Premises used: CategoryTheory.congr_app, CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
⊢ HasColimit F ↔ HasInitial (Cocone F)

Tactic:
⟨fun _ => (Cocone.isColimitEquivIsInitial _ (colimit.isColimit F)).hasInitial, fun h =>
    haveI : HasInitial (Cocone F) := h
    ⟨⟨⟨⊥_ _, (Cocone.isColimitEquivIsInitial _).symm initialIsInitial⟩⟩⟩⟩

Premises used: CategoryTheory.Limits.Cocone, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.initialIsInitial, Nonempty.intro, CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.Cocone.isColimitEquivIsInitial, CategoryTheory.Limits.ColimitCocone.mk, Iff.intro, CategoryTheory.Limits.colimit.cocone, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.initial
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
⊢ HasColimitsOfShape.{v₁, u₁, v₃, u₃} J C ↔ IsRightAdjoint (C := Functor.{v₁, v₃, u₁, u₃} J C) (const J)

Tactic:
calc
    HasColimitsOfShape J C ↔ ∀ F : J ⥤ C, HasColimit F :=
      ⟨fun h => h.has_colimit, fun h => HasColimitsOfShape.mk⟩
    _ ↔ ∀ F : J ⥤ C, HasInitial (Cocone F) := forall_congr' hasColimit_iff_hasInitial_cocone
    _ ↔ ∀ F : J ⥤ C, HasInitial (StructuredArrow F (const J)) :=
      (forall_congr' fun F => (Cocone.equivStructuredArrow F).hasInitial_iff)
    _ ↔ (IsRightAdjoint (const J : C ⥤ _)) :=
      isRightAdjoint_iff_hasInitial_structuredArrow.symm

Premises used: Trans.trans, CategoryTheory.Equivalence.hasInitial_iff, CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.isRightAdjoint_iff_hasInitial_structuredArrow, Iff.intro, forall_congr', CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone, Iff.symm, CategoryTheory.Limits.HasColimitsOfShape.has_colimit, CategoryTheory.Limits.Cocone.equivStructuredArrow
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cocone F
hc : IsColimit c
s : Cocone F
⊢ hc.descCoconeMorphism s = IsInitial.to ((c.isColimitEquivIsInitial : (a : IsColimit c) → IsInitial c) hc) s

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsInitial.to, rfl, CategoryTheory.Limits.IsColimit.descCoconeMorphism
-- Module: Mathlib.CategoryTheory.Limits.ConeCategory
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
c : Cocone F
hc : IsInitial c
s : Cocone F
⊢ hc.to s = IsColimit.descCoconeMorphism ((c.isColimitEquivIsInitial.symm : (a : IsInitial c) → IsColimit c) hc) s

Tactic:
(IsColimit.descCoconeMorphism_eq_isInitial_to (c.isColimitEquivIsInitial.symm hc) s).symm

Premises used: False.elim, CategoryTheory.Limits.IsInitial.ofUnique, CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to, CategoryTheory.Limits.Cocone.isColimitEquivIsInitial, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.asEmptyCocone, Equiv.symm, Eq.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.descCoconeMorphism
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : Functor.{u_1, v₃, u_1, u₃} (Discrete PUnit.{u_1 + 1}) C
X Y : Discrete PUnit.{u_1 + 1}
f : X ⟶ Y
A B : PUnit.{u_1 + 1}
g : PLift ({ as := A : Discrete PUnit.{u_1 + 1} }.as = { as := B }.as)
⊢ Eq.{v₃ + 1} (α :=
    obj.{u_1, v₃, u_1, u₃}
        (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
        { as := A : Discrete PUnit.{u_1 + 1} } ⟶
      F.obj { as := B })
    (CategoryStruct.comp (Y :=
      obj.{u_1, v₃, u_1, u₃}
        (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
        { as := B : Discrete PUnit.{u_1 + 1} })
      (map (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
        { down := g })
      (match (motive :=
        (x : Discrete PUnit.{u_1 + 1}) →
          obj.{u_1, v₃, u_1, u₃}
              (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) x ⟶
            F.obj x)
        { as := B } with
      | { as := PUnit.unit } =>
        𝟙
          (obj.{u_1, v₃, u_1, u₃}
            (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
            { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })))
    ((match (motive :=
        (x : Discrete PUnit.{u_1 + 1}) →
          obj.{u_1, v₃, u_1, u₃}
              (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) x ⟶
            F.obj x)
        { as := A } with
      | { as := PUnit.unit } =>
        𝟙
          (obj.{u_1, v₃, u_1, u₃}
            (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
            { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) ≫
      F.map
        { down := g :
          ULift.{u_1, 0}
            (PLift ({ as := A : Discrete PUnit.{u_1 + 1} }.as = { as := B : Discrete PUnit.{u_1 + 1} }.as)) })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : Functor.{u_1, v₃, u_1, u₃} (Discrete PUnit.{u_1 + 1}) C
X Y : Discrete PUnit.{u_1 + 1}
f : X ⟶ Y
⊢ Eq.{v₃ + 1} (α :=
    obj.{u_1, v₃, u_1, u₃}
        (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) X ⟶
      F.obj Y)
    (map (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) f ≫
      match (motive :=
        (x : Discrete PUnit.{u_1 + 1}) →
          obj.{u_1, v₃, u_1, u₃}
              (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) x ⟶
            F.obj x)
        Y with
      | { as := PUnit.unit } =>
        𝟙
          (obj.{u_1, v₃, u_1, u₃}
            (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
            { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
    ((match (motive :=
        (x : Discrete PUnit.{u_1 + 1}) →
          obj.{u_1, v₃, u_1, u₃}
              (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) x ⟶
            F.obj x)
        X with
      | { as := PUnit.unit } =>
        𝟙
          (obj.{u_1, v₃, u_1, u₃}
            (obj (const (Discrete PUnit.{u_1 + 1})) (F.obj { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }))
            { as := PUnit.unit : Discrete PUnit.{u_1 + 1} })) ≫
      F.map f)

Tactic:
match X, Y, f with
              | .mk A, .mk B, .up g =>
                simp
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
c : Cone F
j j' : J
f : j ⟶ j'
⊢ c.π.app j ≫ F.map f = c.π.app j'

Tactic:
simpa using (c.π.naturality f).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
h :
  ∀ (X : Cone F),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
            (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
            (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
              { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
        X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun X
⊢ CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
      (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
      (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
        { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
          π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) }) =
    𝟙 (Cone F)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
X : Cone F
h :
  ∀ (pt : C) (π : obj (const J) pt ⟶ F),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
            (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
            (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
              { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
        { pt := pt, π := π : Cone F } =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun { pt := pt, π := π : Cone F }
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
          (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
          (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
            { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
              π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
      X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
pt : C
π : obj (const J) pt ⟶ F
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
          (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
          (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
            { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
              π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
      { pt := pt, π := π : Cone F } =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun { pt := pt, π := π : Cone F }

Tactic:
rfl