awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
rw :
  { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
    (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i
⊢ { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)

Tactic:
rw [IsColimit.ι_map]

Premises used: CategoryTheory.Limits.IsColimit.ι_map
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
    (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Tactic:
simpa using i.hom.1.w.symm

Premises used: CategoryTheory.Comma.hom, CategoryTheory.CommaMorphism.w, Prod.fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  P₁.F.map h.left ≫ x_1.hom.1.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
    P₁.F.map h.left ≫ x_1.hom.2.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.2.left = x.hom.2.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  P₁.F.map h.left ≫ x_1.hom.1.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
    P₁.F.map h.left ≫ x_1.hom.2.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.2.left = x.hom.2.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ g = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Tactic:
(isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
refine :
  ∀ (i : K f g P₁ P₂),
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
      { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
        (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)
⊢ g = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Tactic:
refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
rw :
  { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
    (whiskerRight (ψ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i
⊢ { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Tactic:
rw [IsColimit.ι_map]

Premises used: CategoryTheory.Limits.IsColimit.ι_map
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
    (whiskerRight (ψ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Tactic:
simpa using i.hom.2.w.symm

Premises used: CategoryTheory.Comma.hom, CategoryTheory.CommaMorphism.w, Eq.symm, Prod.snd
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hA : IsIndObject A
hB : IsIndObject B
f g : A ⟶ B
⊢ Nonempty (IndParallelPairPresentation f g)

Tactic:
⟨NonemptyParallelPairPresentationAux.presentation f g hA.presentation hB.presentation⟩

Premises used: CategoryTheory.NonemptyParallelPairPresentationAux.presentation, Nonempty.intro, CategoryTheory.Limits.IsIndObject.presentation
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P : IndParallelPairPresentation f g
j : P.I
⊢ { pt := A, ι := P.ι₁ : Cocone (P.F₁ ⋙ yoneda) }.ι.app j ≫
      (parallelPair f g).map WalkingParallelPairHom.left ≫
        Iso.hom (P.isColimit₂.coconePointUniqueUpToIso (colimit.isColimit (P.F₂ ⋙ yoneda))) =
    { pt := A, ι := P.ι₁ : Cocone (P.F₁ ⋙ yoneda) }.ι.app j ≫
      Iso.hom (P.isColimit₁.coconePointUniqueUpToIso (colimit.isColimit (P.F₁ ⋙ yoneda))) ≫
        (parallelPair P.φ P.ψ ⋙
              obj (whiskeringRight P.I C (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))) yoneda ⋙ colim).map
          WalkingParallelPairHom.left

Tactic:
simp [P.hf, P.isColimit₁.ι_map_assoc, P.isColimit₁.comp_coconePointUniqueUpToIso_hom_assoc,
        P.isColimit₂.comp_coconePointUniqueUpToIso_hom]

Premises used: CategoryTheory.IndParallelPairPresentation.hf, CategoryTheory.Limits.IsColimit.ι_map_assoc, CategoryTheory.IndParallelPairPresentation.isColimit₁, CategoryTheory.IndParallelPairPresentation.isColimit₂, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P : IndParallelPairPresentation f g
j : P.I
⊢ { pt := A, ι := P.ι₁ : Cocone (P.F₁ ⋙ yoneda) }.ι.app j ≫
      (parallelPair f g).map WalkingParallelPairHom.right ≫
        Iso.hom (P.isColimit₂.coconePointUniqueUpToIso (colimit.isColimit (P.F₂ ⋙ yoneda))) =
    { pt := A, ι := P.ι₁ : Cocone (P.F₁ ⋙ yoneda) }.ι.app j ≫
      Iso.hom (P.isColimit₁.coconePointUniqueUpToIso (colimit.isColimit (P.F₁ ⋙ yoneda))) ≫
        (parallelPair P.φ P.ψ ⋙
              obj (whiskeringRight P.I C (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))) yoneda ⋙ colim).map
          WalkingParallelPairHom.right

Tactic:
simp [P.hg, P.isColimit₁.ι_map_assoc, P.isColimit₁.comp_coconePointUniqueUpToIso_hom_assoc,
        P.isColimit₂.comp_coconePointUniqueUpToIso_hom]

Premises used: CategoryTheory.Limits.IsColimit.ι_map_assoc, CategoryTheory.IndParallelPairPresentation.isColimit₁, CategoryTheory.IndParallelPairPresentation.isColimit₂, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.IndParallelPairPresentation.hg, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc
-- Module: Mathlib.CategoryTheory.Limits.Indization.Products
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject.{v, u} (∏ᶜ Functor.obj yoneda ∘ g)
f : α → Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) := fun (a : α) ↦ ⋯.presentation.F ⋙ yoneda
suffices : ∏ᶜ f ≅ colimit (pointwiseProduct (I := fun (i : α) ↦ ⋯.presentation.I) F)
⊢ IsIndObject (∏ᶜ f)

Tactic:
suffices (∏ᶜ f ≅ colimit (pointwiseProduct F)) from
    (isIndObject_colimit _ _ (fun i => h _)).map this.inv
-- Module: Mathlib.CategoryTheory.Limits.Indization.Products
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject.{v, u} (∏ᶜ Functor.obj yoneda ∘ g)
f : α → Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) := fun (a : α) ↦ ⋯.presentation.F ⋙ yoneda
refine : (s : α) → f s ≅ colimit (F s)
⊢ ∏ᶜ f ≅ colimit (pointwiseProduct (I := fun (i : α) ↦ ⋯.presentation.I) F)

Tactic:
refine Pi.mapIso (fun s => ?_) ≪≫ (asIso (colimitPointwiseProductToProductColimit F)).symm

Premises used: CategoryTheory.Limits.Pi.mapIso, CategoryTheory.Limits.colimitPointwiseProductToProductColimit, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Indization.Products
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject.{v, u} (∏ᶜ Functor.obj yoneda ∘ g)
f : α → Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) := fun (a : α) ↦ ⋯.presentation.F ⋙ yoneda
s : α
⊢ f s ≅ colimit (F s)

Tactic:
exact IsColimit.coconePointUniqueUpToIso (hf s).presentation.isColimit (colimit.isColimit _)

Premises used: CategoryTheory.Limits.IndObjectPresentation.isColimit, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsIndObject.presentation, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Indization.Products
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject.{v, u} (∏ᶜ Functor.obj yoneda ∘ g)
F : Discrete α ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (a : Discrete α), IsIndObject (F.obj a)
⊢ IsIndObject (limit F)

Tactic:
IsIndObject.map (Pi.isoLimit _).hom (isIndObject_pi h _ (fun a => hF ⟨a⟩))

Premises used: CategoryTheory.Limits.IsIndObject.map, CategoryTheory.Limits.isIndObject_pi, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Pi.isoLimit, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Indization.Products
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : HasLimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (a : Discrete α), IsIndObject (F.obj a)
⊢ IsIndObject (limit F)

Tactic:
isIndObject_limit_of_discrete (fun g => (isIndObject_limit_comp_yoneda (Discrete.functor g)).map
      (HasLimit.isoOfNatIso (Discrete.compNatIsoDiscrete g yoneda)).hom) F hF

Premises used: CategoryTheory.Limits.isIndObject_limit_of_discrete, CategoryTheory.Limits.HasLimit.isoOfNatIso, CategoryTheory.Limits.IsIndObject.map, CategoryTheory.Discrete.functor, CategoryTheory.yoneda, CategoryTheory.Limits.isIndObject_limit_comp_yoneda, CategoryTheory.Discrete.compNatIsoDiscrete, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
j : C
h :
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) (Cocone.pt.{v, w, u, w + 1} (pUnitCocone C))) j)
          (NatTrans.app (Cocone.ι (pUnitCocone C)) j) (s.ι.app Classical.ofNonempty)))
      PUnit.unit =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app j)).toFun PUnit.unit
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) (Cocone.pt.{v, w, u, w + 1} (pUnitCocone C))) j)
      (NatTrans.app (Cocone.ι (pUnitCocone C)) j) (s.ι.app Classical.ofNonempty) =
    s.ι.app j

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
j : C
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) (Cocone.pt.{v, w, u, w + 1} (pUnitCocone C))) j)
          (NatTrans.app (Cocone.ι (pUnitCocone C)) j) (s.ι.app Classical.ofNonempty)))
      PUnit.unit =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app j)).toFun PUnit.unit

Tactic:
constant_of_preserves_morphisms (α := s.pt)
      (fun (k : C) ↦ s.ι.app k PUnit.unit) ?_ Classical.ofNonempty j

Premises used: Classical.ofNonempty, CategoryTheory.ConcreteCategory.hom, CategoryTheory.constant_of_preserves_morphisms, CategoryTheory.Limits.Cocone.ι, PUnit.unit, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
j : C
h :
  ∀ (j₁ j₂ : C) (x : j₁ ⟶ j₂),
    Eq.{w + 1} (α := s.pt)
      ((fun (k : C) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app k) :
                (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj k)) →
                  (fun (X : Type w) ↦ X) (((Functor.const C).obj s.pt).obj k))
              PUnit.unit :
            (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) s.pt) k)))
        j₁)
      ((fun (k : C) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app k) :
                (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj k)) →
                  (fun (X : Type w) ↦ X) (((Functor.const C).obj s.pt).obj k))
              PUnit.unit :
            (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) s.pt) k)))
        j₂)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) (Cocone.pt.{v, w, u, w + 1} (pUnitCocone C))) j)
          (NatTrans.app (Cocone.ι (pUnitCocone C)) j) (s.ι.app Classical.ofNonempty)))
      PUnit.unit =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app j)).toFun PUnit.unit

Tactic:
refine constant_of_preserves_morphisms (α := s.pt)
      (fun (k : C) ↦ s.ι.app k PUnit.unit) ?_ Classical.ofNonempty j

Premises used: Classical.ofNonempty, CategoryTheory.ConcreteCategory.hom, CategoryTheory.constant_of_preserves_morphisms, CategoryTheory.Limits.Cocone.ι, PUnit.unit, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
j X Y : C
f : X ⟶ Y
⊢ Eq.{w + 1} (α := s.pt)
    ((fun (k : C) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app k) :
              (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj k)) →
                (fun (X : Type w) ↦ X) (((Functor.const C).obj s.pt).obj k))
            PUnit.unit :
          (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) s.pt) k)))
      X)
    ((fun (k : C) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app k) :
              (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj k)) →
                (fun (X : Type w) ↦ X) (((Functor.const C).obj s.pt).obj k))
            PUnit.unit :
          (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) s.pt) k)))
      Y)

Tactic:
ConcreteCategory.congr_hom (s.ι.naturality f).symm PUnit.unit

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
j X Y : C
f : X ⟶ Y
⊢ Eq.{w + 1} (α := s.pt)
    ((fun (k : C) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app k) :
              (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj k)) →
                (fun (X : Type w) ↦ X) (((Functor.const C).obj s.pt).obj k))
            PUnit.unit :
          (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) s.pt) k)))
      X)
    ((fun (k : C) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app k) :
              (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj k)) →
                (fun (X : Type w) ↦ X) (((Functor.const C).obj s.pt).obj k))
            PUnit.unit :
          (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) s.pt) k)))
      Y)

Tactic:
exact ConcreteCategory.congr_hom (s.ι.naturality f).symm PUnit.unit

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
m : Cocone.pt.{v, w, u, w + 1} (pUnitCocone C) ⟶ s.pt
h : ∀ (j : C), NatTrans.app (Cocone.ι (pUnitCocone C)) j ≫ m = s.ι.app j
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun PUnit.unit =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app Classical.ofNonempty)) PUnit.unit
⊢ m = s.ι.app Classical.ofNonempty

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
m : Cocone.pt.{v, w, u, w + 1} (pUnitCocone C) ⟶ s.pt
h : ∀ (j : C), NatTrans.app (Cocone.ι (pUnitCocone C)) j ≫ m = s.ι.app j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun PUnit.unit =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app Classical.ofNonempty)) PUnit.unit

Tactic:
simp [← h Classical.ofNonempty]

Premises used: Classical.ofNonempty
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
⊢ HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)

Tactic:
⟨_, isColimitPUnitCocone _⟩

Premises used: CategoryTheory.Limits.Types.isColimitPUnitCocone, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsPreconnected.{v, u} C
inst_2 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
a b : colimit.{v, u, w, w + 1} (constPUnitFunctor C)
obtain :
  ∀ (c : C),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) c) :
          (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj c)) →
            (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
        PUnit.unit =
      b
⊢ a = b

Tactic:
obtain ⟨c, ⟨⟩, rfl⟩ := jointly_surjective' a

Premises used: CategoryTheory.Limits.Types.jointly_surjective', rfl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsPreconnected.{v, u} C
inst_2 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
b : colimit.{v, u, w, w + 1} (constPUnitFunctor C)
c : C
obtain :
  ∀ (d : C),
    Eq (α := colimit.{v, u, w, w + 1} (constPUnitFunctor C))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) c) :
            (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj c)) →
              (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
          PUnit.unit :
        (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) d) :
            (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj d)) →
              (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
          PUnit.unit :
        (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) c) :
        (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj c)) →
          (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
      PUnit.unit =
    b

Tactic:
obtain ⟨d, ⟨⟩, rfl⟩ := jointly_surjective' b

Premises used: CategoryTheory.Limits.Types.jointly_surjective', rfl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsPreconnected.{v, u} C
inst_2 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
c d : C
h :
  ∀ (j₁ j₂ : C) (x : j₁ ⟶ j₂),
    Eq (α := (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) j₁) :
            (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj j₁)) →
              (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
          PUnit.unit :
        (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) j₂) :
            (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj j₂)) →
              (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
          PUnit.unit :
        (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
⊢ Eq (α := colimit.{v, u, w, w + 1} (constPUnitFunctor C))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) c) :
          (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj c)) →
            (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
        PUnit.unit :
      (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) d) :
          (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj d)) →
            (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
        PUnit.unit :
      (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))

Tactic:
apply constant_of_preserves_morphisms (colimit.ι (constPUnitFunctor C) · PUnit.unit)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.constant_of_preserves_morphisms, PUnit.unit, DFunLike.coe, CategoryTheory.Limits.Types.constPUnitFunctor, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsPreconnected.{v, u} C
inst_2 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
c d : C
⊢ ∀ (j₁ j₂ : C) (x : j₁ ⟶ j₂),
    Eq (α := (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) j₁) :
            (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj j₁)) →
              (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
          PUnit.unit :
        (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (constPUnitFunctor C) j₂) :
            (a : (fun (X : Type w) ↦ X) ((constPUnitFunctor C).obj j₂)) →
              (fun (X : Type w) ↦ X) (colimit (constPUnitFunctor C)))
          PUnit.unit :
        (fun (X : Type w) ↦ X) (colimit.{v, u, w, w + 1} (constPUnitFunctor C)))

Tactic:
fun c d f => colimit_sound f rfl

Premises used: CategoryTheory.Limits.Types.colimit_sound, rfl