awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
h : IsLimit c
⊢ IsGLB (Set.range F.obj) c.pt

Tactic:
⟨(conePt_mem_lowerBounds F c), fun _ k ↦ (h.lift (coneOfLowerBound F k)).le⟩

Premises used: Preorder.conePt_mem_lowerBounds, Quiver.Hom.le, IsGreatest, IsGLB, And.intro, Preorder.coneOfLowerBound, CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
⊢ HasLimit F ↔ ∃ (x : C), IsGLB (Set.range F.obj) x

Tactic:
⟨fun _ ↦ ⟨_, isGLB_of_isLimit _ (limit.isLimit _)⟩,
    fun ⟨_, h⟩ ↦ ⟨⟨limitConeOfIsGLB _ h⟩⟩⟩

Premises used: CategoryTheory.Limits.HasLimit, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.Cone.pt, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, _private.0.Preorder.hasLimit_iff_hasGLB.match_1, CategoryTheory.Limits.HasLimit.mk', Preorder.limitConeOfIsGLB, Iff.intro, Exists.intro, Preorder.isGLB_of_isLimit
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
x : C
this : ∀ (i : J) (p : F.obj i = x), x ≤ c.pt
⊢ x ∈ Set.range F.obj → x ≤ c.pt

Tactic:
⟨i, p⟩
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
x : C
i : J
p : F.obj i = x
rw : F.obj i ≤ c.pt
⊢ x ≤ c.pt

Tactic:
rw [← p]
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
x : C
i : J
p : F.obj i = x
⊢ F.obj i ≤ c.pt

Tactic:
(c.ι.app i).le

Premises used: Quiver.Hom.le, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
x : C
i : J
p : F.obj i = x
⊢ F.obj i ≤ c.pt

Tactic:
exact (c.ι.app i).le

Premises used: Quiver.Hom.le, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
h : IsColimit c
⊢ IsLUB (Set.range F.obj) c.pt

Tactic:
⟨(coconePt_mem_upperBounds F c), fun _ k ↦ (h.desc (coconeOfUpperBound F k)).le⟩

Premises used: Preorder.coconePt_mem_upperBounds, Quiver.Hom.le, IsLeast, CategoryTheory.Limits.IsColimit.desc, And.intro, IsLUB, Preorder.coconeOfUpperBound
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
⊢ HasColimit F ↔ ∃ (x : C), IsLUB (Set.range F.obj) x

Tactic:
⟨fun _ ↦ ⟨_, isLUB_of_isColimit _ (colimit.isColimit _)⟩,
    fun ⟨_, h⟩ ↦ ⟨⟨colimitCoconeOfIsLUB _ h⟩⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, _private.0.Preorder.hasColimit_iff_hasLUB.match_1, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', Preorder.isLUB_of_isColimit, Iff.intro, Exists.intro, CategoryTheory.Limits.HasColimit, CategoryTheory.Limits.colimit.cocone, Preorder.colimitCoconeOfIsLUB, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
inst_1 : OrderTop C
⊢ HasTerminal C

Tactic:
hasTerminal_of_unique ⊤

Premises used: CategoryTheory.Limits.hasTerminal_of_unique, Top.top
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
inst_1 : OrderBot C
⊢ HasInitial C

Tactic:
hasInitial_of_unique ⊥

Premises used: CategoryTheory.Limits.hasInitial_of_unique, Bot.bot
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeInf C
X Y : C
s : BinaryFan X Y
⊢ CategoryStruct.comp (Y := X ⊓ Y) ((fun (s : BinaryFan X Y) ↦ homOfLE ⋯) s) (homOfLE ⋯) = s.fst

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeInf C
X Y : C
s : BinaryFan X Y
⊢ CategoryStruct.comp (Y := X ⊓ Y) ((fun (s : BinaryFan X Y) ↦ homOfLE ⋯) s) (homOfLE ⋯) = s.snd

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeInf C
X Y : C
s : BinaryFan X Y
m : s.pt ⟶ X ⊓ Y
h : m ≫ homOfLE ⋯ = s.fst
h_1 : m ≫ homOfLE ⋯ = s.snd
⊢ m = (fun (s : BinaryFan X Y) ↦ homOfLE ⋯) s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeInf C
F : Discrete WalkingPair ⥤ C
⊢ HasLimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))

Tactic:
have : HasLimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isLimitBinaryFan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeInf C
F : Discrete WalkingPair ⥤ C
this : HasLimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasLimit F

Tactic:
apply hasLimit_of_iso (diagramIsoPair F).symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeSup C
X Y : C
s : BinaryCofan X Y
⊢ CategoryStruct.comp (Y := X ⊔ Y) (homOfLE ⋯) ((fun (s : BinaryCofan X Y) ↦ homOfLE ⋯) s) = s.inl

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeSup C
X Y : C
s : BinaryCofan X Y
⊢ CategoryStruct.comp (Y := X ⊔ Y) (homOfLE ⋯) ((fun (s : BinaryCofan X Y) ↦ homOfLE ⋯) s) = s.inr

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeSup C
X Y : C
s : BinaryCofan X Y
m : X ⊔ Y ⟶ s.pt
h : homOfLE ⋯ ≫ m = s.inl
h_1 : homOfLE ⋯ ≫ m = s.inr
⊢ m = (fun (s : BinaryCofan X Y) ↦ homOfLE ⋯) s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
⊢ HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))

Tactic:
have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso (diagramIsoPair F)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoPair
-- Module: Mathlib.CategoryTheory.Limits.Presentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
X : C
pres : ColimitPresentation.{t, w, v, u} J X
i j : J
f : i ⟶ j
⊢ pres.diag.map f ≫ pres.ι.app j = pres.ι.app i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Presentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
X : C
pres : ColimitPresentation.{t, w, v, u} J X
⊢ HasColimit pres.diag

Tactic:
⟨_, pres.isColimit⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Presentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
X : C
P : ColimitPresentation.{t, w, v, u} J X
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_3 : PreservesColimitsOfShape.{t, w, v, v_1, u, u_1} J F
⊢ ∀ (j : J),
    (F.mapCocone { pt := X, ι := P.ι : Cocone P.diag }).ι.app j ≫
        Iso.hom (Iso.refl (F.mapCocone { pt := X, ι := P.ι : Cocone P.diag }).pt) =
      { pt := F.obj X, ι := Functor.whiskerRight P.ι F ≫ Iso.hom (Functor.constComp J X F) }.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Presentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
X : C
pres : LimitPresentation.{t, w, v, u} J X
i j : J
f : i ⟶ j
⊢ pres.π.app i ≫ pres.diag.map f = pres.π.app j

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

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.LimitPresentation.π
-- Module: Mathlib.CategoryTheory.Limits.Presentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
X : C
pres : LimitPresentation.{t, w, v, u} J X
⊢ HasLimit pres.diag

Tactic:
⟨_, pres.isLimit⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Presentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : Category.{t, w} J_1
X_1 : C
J : Type w
inst_2 : Category.{t, w} J
X : C
P : LimitPresentation.{t, w, v, u} J X
D : Type u_1
inst_3 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_4 : PreservesLimitsOfShape.{t, w, v, v_1, u, u_1} J F
⊢ ∀ (j : J),
    (F.mapCone { pt := X, π := P.π : Cone P.diag }).π.app j =
      Iso.hom (Iso.refl (F.mapCone { pt := X, π := P.π : Cone P.diag }).pt) ≫
        { pt := F.obj X, π := Iso.inv (Functor.constComp J X F) ≫ Functor.whiskerRight P.π F : Cone (P.diag ⋙ F) }.π.app
          j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : PreservesLimit K F), a = b
⊢ Subsingleton (PreservesLimit K F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {c : Cone K} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : PreservesColimit K F), a = b
⊢ Subsingleton (PreservesColimit K F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {c : Cocone K} (hc : IsColimit c), Nonempty (IsColimit (F.mapCocone c))
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F), a = b
⊢ Subsingleton (PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {K : Functor.{w', v₁, w, u₁} J C}, PreservesLimit K F
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F), a = b
⊢ Subsingleton (PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {K : Functor.{w', v₁, w, u₁} J C}, PreservesColimit K F
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
⊢ Subsingleton (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {J : Type w} [inst_3 : Category.{w', w} J], PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
⊢ Subsingleton (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {J : Type w} [inst_3 : Category.{w', w} J], PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
𝒥 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
c : Cone K
h : IsLimit c
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C }}
    (h : IsLimit c)
    (s :
      Cone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
    (j : J),
    CategoryStruct.comp (Y :=
        Cone.pt (F :=
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
          (Functor.mapCone (𝟭 C) c))
        ((fun
              (s :
                Cone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w', v₁, w, u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C })
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt)
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } } :
                    Cone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w', v₁, w, u₁} J C } } ⟶
                c.pt))
          s)
        (NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) j) =
      s.π.app j
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (j : J),
    CategoryStruct.comp (Y := Cone.pt (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c))
        ((fun (s : Cone (K ⋙ 𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt) K } :
                    Cone K } ⟶
                c.pt))
          s)
        (NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) j) =
      s.π.app j

Tactic:
cases K
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
𝒥 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
c : Cone K
h : IsLimit c
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C }}
    (h : IsLimit c)
    (s :
      Cone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
    (m :
      s.pt ⟶
        Cone.pt (F :=
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
          (Functor.mapCone (𝟭 C) c)),
    (∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) j = s.π.app j) →
      m =
        (fun
              (s :
                Cone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w', v₁, w, u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C })
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt)
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } } :
                    Cone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w', v₁, w, u₁} J C } } ⟶
                c.pt))
          s
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (m : s.pt ⟶ Cone.pt (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c)),
    (∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) j = s.π.app j) →
      m =
        (fun (s : Cone (K ⋙ 𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt) K } :
                    Cone K } ⟶
                c.pt))
          s

Tactic:
cases K
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
𝒥 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
c : Cocone K
h : IsColimit c
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C }}
    (h : IsColimit c)
    (s :
      Cocone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
    (j : J),
    CategoryStruct.comp (Y :=
        Functor.obj.{w', v₁, w, u₁}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F :=
              { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
              (Functor.mapCocone (𝟭 C) c)))
          j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j)
        ((fun
              (s :
                Cocone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C)) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              c.pt ⟶
                Cocone.pt.{w', v₁, w, u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp })
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s) =
      s.ι.app j
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    CategoryStruct.comp (Y :=
        Functor.obj.{w', v₁, w, u₁}
          (Functor.obj (Functor.const J) (Cocone.pt (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c))) j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j)
        ((fun (s : Cocone (K ⋙ 𝟭 C)) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              c.pt ⟶
                Cocone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s) =
      s.ι.app j

Tactic:
cases K
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
𝒥 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
c : Cocone K
h : IsColimit c
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C }}
    (h : IsColimit c)
    (s :
      Cocone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
    (m :
      Cocone.pt (F :=
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
          (Functor.mapCocone (𝟭 C) c) ⟶
        s.pt),
    (∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j ≫ m = s.ι.app j) →
      m =
        (fun
              (s :
                Cocone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C)) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              c.pt ⟶
                Cocone.pt.{w', v₁, w, u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp })
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (m : Cocone.pt (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c) ⟶ s.pt),
    (∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j ≫ m = s.ι.app j) →
      m =
        (fun (s : Cocone (K ⋙ 𝟭 C)) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              c.pt ⟶
                Cocone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s

Tactic:
cases K