awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact fun c d f => colimit_sound f rfl

Premises used: CategoryTheory.Limits.Types.colimit_sound, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x y : (j : C) × F.obj j
h : F.ColimitTypeRel x y
⊢ Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
Zigzag.of_hom <| Exists.choose h

Premises used: Exists.choose, CategoryTheory.Zigzag.of_hom
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x y : (j : C) × F.obj j
h : F.ColimitTypeRel x y
⊢ Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
exact Zigzag.of_hom <| Exists.choose h

Premises used: Exists.choose, CategoryTheory.Zigzag.of_hom
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x : (j : C) × F.obj j
⊢ Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (x.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
Zigzag.refl _

Premises used: CategoryTheory.Zigzag.refl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x : (j : C) × F.obj j
⊢ Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (x.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
exact Zigzag.refl _

Premises used: CategoryTheory.Zigzag.refl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x y : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel x y
ih : Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))
⊢ Zigzag.{v, u} (y.fst (β := fun (j : C) ↦ F.obj j)) (x.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
zigzag_symmetric ih

Premises used: CategoryTheory.zigzag_symmetric
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x y : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel x y
ih : Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))
⊢ Zigzag.{v, u} (y.fst (β := fun (j : C) ↦ F.obj j)) (x.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
exact zigzag_symmetric ih

Premises used: CategoryTheory.zigzag_symmetric
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x y z : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel x y
h_1 : Relation.EqvGen F.ColimitTypeRel y z
ih₁ : Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))
ih₂ : Zigzag.{v, u} (y.fst (β := fun (j : C) ↦ F.obj j)) (z.fst (β := fun (j : C) ↦ F.obj j))
⊢ Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (z.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
ih₁.trans ih₂

Premises used: CategoryTheory.Zigzag.trans
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d x y z : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel x y
h_1 : Relation.EqvGen F.ColimitTypeRel y z
ih₁ : Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))
ih₂ : Zigzag.{v, u} (y.fst (β := fun (j : C) ↦ F.obj j)) (z.fst (β := fun (j : C) ↦ F.obj j))
⊢ Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (z.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
exact ih₁.trans ih₂

Premises used: CategoryTheory.Zigzag.trans
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
c d : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel c d
rel :
  ∀ (x y : (j : C) × F.obj j) (h : F.ColimitTypeRel x y),
    Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))
refl :
  ∀ (x : (j : C) × F.obj j), Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (x.fst (β := fun (j : C) ↦ F.obj j))
symm :
  ∀ (x y : (j : C) × F.obj j),
    Relation.EqvGen F.ColimitTypeRel x y →
      ∀ (ih : Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j))),
        Zigzag.{v, u} (y.fst (β := fun (j : C) ↦ F.obj j)) (x.fst (β := fun (j : C) ↦ F.obj j))
trans :
  ∀ (x y z : (j : C) × F.obj j),
    Relation.EqvGen F.ColimitTypeRel x y →
      Relation.EqvGen F.ColimitTypeRel y z →
        ∀ (ih₁ : Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (y.fst (β := fun (j : C) ↦ F.obj j)))
          (ih₂ : Zigzag.{v, u} (y.fst (β := fun (j : C) ↦ F.obj j)) (z.fst (β := fun (j : C) ↦ F.obj j))),
          Zigzag.{v, u} (x.fst (β := fun (j : C) ↦ F.obj j)) (z.fst (β := fun (j : C) ↦ F.obj j))
⊢ Zigzag.{v, u} (c.fst (β := fun (j : C) ↦ F.obj j)) (d.fst (β := fun (j : C) ↦ F.obj j))

Tactic:
induction h with
  | rel _ _ h => exact Zigzag.of_hom <| Exists.choose h
  | refl _ => exact Zigzag.refl _
  | symm _ _ _ ih => exact zigzag_symmetric ih
  | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂

Premises used: CategoryTheory.Zigzag.refl, symm, CategoryTheory.Zigzag.of_hom, refl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
⊢ IsConnected.{v, u} C ↔ Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩

Premises used: _private.0.CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.match_1, Nonempty.intro, Iff.intro, CategoryTheory.IsConnected, CategoryTheory.Limits.Types.colimitConstPUnitIsoPUnit
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
refine :
  Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}) →
    ∀ (h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}), IsConnected.{v, u} C
⊢ IsConnected.{v, u} C ↔ Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
refine ⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
⊢ Nonempty C

Tactic:
have : Nonempty C := nonempty_of_nonempty_colimit <| Nonempty.map h.inv inferInstance
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
⊢ IsConnected.{v, u} C

Tactic:
zigzag_isConnected <| fun c d => ?_

Premises used: CategoryTheory.zigzag_isConnected
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
refine : ∀ (c d : C), Zigzag.{v, u} c d
⊢ IsConnected.{v, u} C

Tactic:
refine zigzag_isConnected <| fun c d => ?_

Premises used: CategoryTheory.zigzag_isConnected
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Zigzag.{v, u} c d

Tactic:
zigzag_of_eqvGen_colimitTypeRel _ (constPUnitFunctor C) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩ ?_

Premises used: CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel, PUnit.unit, Sigma.mk, CategoryTheory.Limits.Types.constPUnitFunctor
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
refine :
  Relation.EqvGen (α := (j : C) × Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j)
    (Functor.ColimitTypeRel (constPUnitFunctor C))
    (Sigma.mk (β := fun (j : C) ↦ Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j) c PUnit.unit)
    (Sigma.mk (β := fun (j : C) ↦ Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j) d PUnit.unit)
⊢ Zigzag.{v, u} c d

Tactic:
refine zigzag_of_eqvGen_colimitTypeRel _ (constPUnitFunctor C) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩ ?_

Premises used: CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel, PUnit.unit, Sigma.mk, CategoryTheory.Limits.Types.constPUnitFunctor
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Relation.EqvGen (α := (j : C) × Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j)
    (Functor.ColimitTypeRel (constPUnitFunctor C))
    (Sigma.mk (β := fun (j : C) ↦ Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j) c PUnit.unit)
    (Sigma.mk (β := fun (j : C) ↦ Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j) d PUnit.unit)

Tactic:
colimit_eq <| h.toEquiv.injective rfl

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Limits.Types.colimit_eq, Equiv.injective, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
h_1 : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Relation.EqvGen (α := (j : C) × Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j)
    (Functor.ColimitTypeRel (constPUnitFunctor C))
    (Sigma.mk (β := fun (j : C) ↦ Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j) c PUnit.unit)
    (Sigma.mk (β := fun (j : C) ↦ Functor.obj.{v, w, u, w + 1} (constPUnitFunctor C) j) d PUnit.unit)

Tactic:
exact colimit_eq <| h.toEquiv.injective rfl

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Limits.Types.colimit_eq, Equiv.injective, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsConnected.{v, u} C ↔ Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C))

Tactic:
⟨fun inst => ⟨isColimitPUnitCocone C⟩, fun ⟨h⟩ => ?_⟩

Premises used: CategoryTheory.Limits.Types.isColimitPUnitCocone, _private.0.CategoryTheory.Limits.Types.isConnected_iff_isColimit_pUnitCocone.match_1, Nonempty.intro, Iff.intro, CategoryTheory.IsConnected
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
refine :
  Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C)) →
    ∀ (h : IsColimit.{v, w, u, w + 1} (pUnitCocone C)), IsConnected.{v, u} C
⊢ IsConnected.{v, u} C ↔ Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C))

Tactic:
refine ⟨fun inst => ⟨isColimitPUnitCocone C⟩, fun ⟨h⟩ => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
h_1 : Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C))
h : IsColimit.{v, w, u, w + 1} (pUnitCocone C)
colimitCocone : ColimitCocone.{v, u, w, w + 1} (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
⊢ HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)

Tactic:
have : HasColimit (constPUnitFunctor.{w} C) := ⟨⟨colimitCocone⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
h_1 : Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C))
h : IsColimit.{v, w, u, w + 1} (pUnitCocone C)
colimitCocone : ColimitCocone.{v, u, w, w + 1} (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
simp : Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})
⊢ IsConnected.{v, u} C

Tactic:
simp only [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{w} C]
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
h_1 : Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C))
h : IsColimit.{v, w, u, w + 1} (pUnitCocone C)
colimitCocone : ColimitCocone.{v, u, w, w + 1} (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
⊢ Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
⟨colimit.isoColimitCocone colimitCocone⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
h_1 : Nonempty (IsColimit.{v, w, u, w + 1} (pUnitCocone C))
h : IsColimit.{v, w, u, w + 1} (pUnitCocone C)
colimitCocone : ColimitCocone.{v, u, w, w + 1} (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
this : HasColimit.{v, u, w, w + 1} (constPUnitFunctor C)
⊢ Nonempty.{w + 1} (colimit.{v, u, w, w + 1} (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
exact ⟨colimit.isoColimitCocone colimitCocone⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
inst_2 : F.Final
rw :
  Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})
⊢ IsConnected.{v, u} C ↔ IsConnected.{v₂, u₂} D

Tactic:
rw [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} C,
    isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} D]
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
inst_2 : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})

Tactic:
Equiv.nonempty_congr <| Iso.isoCongrLeft <|
    CategoryTheory.Functor.Final.colimitIso F <| constPUnitFunctor.{max u v u₂ v₂} D

Premises used: CategoryTheory.Iso.isoCongrLeft, Equiv.nonempty_congr, CategoryTheory.Functor.Final.colimitIso, CategoryTheory.Limits.Types.constPUnitFunctor
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
inst_2 : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})

Tactic:
exact Equiv.nonempty_congr <| Iso.isoCongrLeft <|
    CategoryTheory.Functor.Final.colimitIso F <| constPUnitFunctor.{max u v u₂ v₂} D

Premises used: CategoryTheory.Iso.isoCongrLeft, Equiv.nonempty_congr, CategoryTheory.Functor.Final.colimitIso
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
inst_2 : F.Initial
rw : IsConnected.{v, u} Cᵒᵖ ↔ IsConnected.{v₂, u₂} Dᵒᵖ
⊢ IsConnected.{v, u} C ↔ IsConnected.{v₂, u₂} D

Tactic:
rw [← isConnected_op_iff_isConnected C, ← isConnected_op_iff_isConnected D]

Premises used: CategoryTheory.isConnected_op_iff_isConnected
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
inst_2 : F.Initial
⊢ IsConnected.{v, u} Cᵒᵖ ↔ IsConnected.{v₂, u₂} Dᵒᵖ

Tactic:
isConnected_iff_of_final F.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.isConnected_iff_of_final
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
inst_2 : F.Initial
⊢ IsConnected.{v, u} Cᵒᵖ ↔ IsConnected.{v₂, u₂} Dᵒᵖ

Tactic:
exact isConnected_iff_of_final F.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.isConnected_iff_of_final
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial.{v_1, u_1} x
this : Nonempty C := ⋯
h₁ : ∀ (j₁ j₂ : C), ∃ (l : List C), List.IsChain Zag.{v_1, u_1} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsConnected.{v_1, u_1} C

Tactic:
apply isConnected_of_zigzag

Premises used: CategoryTheory.isConnected_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
h₁ : List.IsChain Zag.{v_1, u_1} [j₁, x, j₂] ∧ [j₁, x, j₂].getLast ⋯ = j₂
⊢ ∃ (l : List C), List.IsChain Zag.{v_1, u_1} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
use [x, j₂]
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
h₁ : Zag.{v_1, u_1} j₁ x ∧ Zag.{v_1, u_1} x j₂
⊢ List.IsChain Zag.{v_1, u_1} [j₁, x, j₂] ∧ [j₁, x, j₂].getLast ⋯ = j₂

Tactic:
simp only [List.isChain_cons_cons, List.isChain_singleton, and_true, ne_eq,
    reduceCtorEq, not_false_eq_true, List.getLast_cons, List.cons_ne_self, List.getLast_singleton]

Premises used: reduceCtorEq, List.isChain_singleton, and_true, List.cons_ne_self, ne_eq, List.isChain_cons_cons, List.getLast_cons, List.getLast_singleton, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
⊢ Zag.{v_1, u_1} j₁ x ∧ Zag.{v_1, u_1} x j₂

Tactic:
⟨Zag.symm <| Zag.of_hom <| h.to _, Zag.of_hom <| h.to _⟩

Premises used: CategoryTheory.Zag.symm, CategoryTheory.Limits.IsInitial.to, And.intro, CategoryTheory.Zag.of_hom
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
⊢ Zag.{v_1, u_1} j₁ x ∧ Zag.{v_1, u_1} x j₂

Tactic:
exact ⟨Zag.symm <| Zag.of_hom <| h.to _, Zag.of_hom <| h.to _⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal.{v_1, u_1} x
this : Nonempty C := ⋯
h₁ : ∀ (j₁ j₂ : C), ∃ (l : List C), List.IsChain Zag.{v_1, u_1} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsConnected.{v_1, u_1} C

Tactic:
apply isConnected_of_zigzag

Premises used: CategoryTheory.isConnected_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
h₁ : List.IsChain Zag.{v_1, u_1} [j₁, x, j₂] ∧ [j₁, x, j₂].getLast ⋯ = j₂
⊢ ∃ (l : List C), List.IsChain Zag.{v_1, u_1} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
use [x, j₂]
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
h₁ : Zag.{v_1, u_1} j₁ x ∧ Zag.{v_1, u_1} x j₂
⊢ List.IsChain Zag.{v_1, u_1} [j₁, x, j₂] ∧ [j₁, x, j₂].getLast ⋯ = j₂

Tactic:
simp only [List.isChain_cons_cons, List.isChain_singleton, and_true, ne_eq,
    reduceCtorEq, not_false_eq_true, List.getLast_cons, List.cons_ne_self, List.getLast_singleton]

Premises used: reduceCtorEq, List.isChain_singleton, and_true, List.cons_ne_self, ne_eq, List.isChain_cons_cons, List.getLast_cons, List.getLast_singleton, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
⊢ Zag.{v_1, u_1} j₁ x ∧ Zag.{v_1, u_1} x j₂

Tactic:
⟨Zag.of_hom <| h.from _, Zag.symm <| Zag.of_hom <| h.from _⟩

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Zag.symm, And.intro, CategoryTheory.Zag.of_hom
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal.{v_1, u_1} x
this : Nonempty C := ⋯
j₁ j₂ : C
⊢ Zag.{v_1, u_1} j₁ x ∧ Zag.{v_1, u_1} x j₂

Tactic:
exact ⟨Zag.of_hom <| h.from _, Zag.symm <| Zag.of_hom <| h.from _⟩
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasInitial.{v_1, u_1} C
⊢ IsConnected.{v_1, u_1} C

Tactic:
isConnected_of_isInitial C Limits.initialIsInitial

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.isConnected_of_isInitial
-- Module: Mathlib.CategoryTheory.Limits.IsConnected
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasTerminal.{v_1, u_1} C
⊢ IsConnected.{v_1, u_1} C

Tactic:
isConnected_of_isTerminal C Limits.terminalIsTerminal

Premises used: CategoryTheory.Limits.terminalIsTerminal, CategoryTheory.isConnected_of_isTerminal
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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 : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
P Q : IsLimit t
mk :
  ∀ (lift : (s : Cone F) → s.pt ⟶ t.pt) (fac : ∀ (s : Cone F) (j : J), lift s ≫ t.π.app j = s.π.app j)
    (uniq : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift s),
    { lift := lift, fac := fac, uniq := uniq : IsLimit t } = Q
⊢ P = Q

Tactic:
cases P
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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 : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
Q : IsLimit t
lift : (s : Cone F) → s.pt ⟶ t.pt
fac : ∀ (s : Cone F) (j : J), lift s ≫ t.π.app j = s.π.app j
uniq : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift s
mk :
  ∀ (lift_1 : (s : Cone F) → s.pt ⟶ t.pt) (fac_1 : ∀ (s : Cone F) (j : J), lift_1 s ≫ t.π.app j = s.π.app j)
    (uniq_1 : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift_1 s),
    { lift := lift, fac := fac, uniq := uniq : IsLimit t } = { lift := lift_1, fac := fac_1, uniq := uniq_1 }
⊢ { lift := lift, fac := fac, uniq := uniq : IsLimit t } = Q

Tactic:
cases Q