awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))
hy :
  Eq (α := (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y' :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
ky : (i : α) → I i
yk₀ : (pointwiseProduct (I := I) F).obj ky
hyk₀ :
  (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky) :
        (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
          (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
      yk₀ =
    y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct (I := I) F).obj ky'
hyk₀' :
  (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky') :
        (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky')) →
          (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
      yk₀' =
    y'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : (pointwiseProduct (I := I) F).obj k :=
  (hom (FC := TypeCat.Fun) ((pointwiseProduct (I := I) F).map (IsFiltered.leftToMax ky ky')) :
      (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
        (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj (IsFiltered.max ky ky')))
    yk₀
yk' : (pointwiseProduct (I := I) F).obj k :=
  (hom (FC := TypeCat.Fun) ((pointwiseProduct (I := I) F).map (IsFiltered.rightToMax ky ky')) :
      (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky')) →
        (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj (IsFiltered.max ky ky')))
    yk₀'
⊢ y =
    (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
        (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
          (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
      yk

Tactic:
simp only [k, yk, colimit.w_apply, hyk₀]

Premises used: CategoryTheory.Limits.colimit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
⊢ ∀ (s : α),
    ∃ (i : I s) (xi : (F s).obj i),
      Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (colimit.ι (F s) i) :
              (a : (fun (X : Type u) ↦ X) ((F s).obj i)) → (fun (X : Type u) ↦ X) (colimit (F s)))
            xi :
          (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
            x :
          (fun (X : Type u) ↦ X) (colimit (F s)))

Tactic:
have hch : ∀ (s : α), ∃ (i : I s) (xi : (F s).obj i), colimit.ι (F s) i xi =
        Pi.π (fun s => colimit (F s)) s x := fun s => Types.jointly_surjective' _
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
hch :
  ∀ (s : α),
    ∃ (i : I s) (xi : (F s).obj i),
      Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (colimit.ι (F s) i) :
              (a : (fun (X : Type u) ↦ X) ((F s).obj i)) → (fun (X : Type u) ↦ X) (colimit (F s)))
            xi :
          (fun (X : Type u) ↦ X) (colimit (F s)))
        ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
            x :
          (fun (X : Type u) ↦ X) (colimit (F s)))
refine_2 :
  ∀ (k : (s : α) → I s) (p : (s : α) → (F s).obj (k s))
    (hk :
      ∀ (s : α),
        Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
          ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
                (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
              (p s) :
            (fun (X : Type u) ↦ X) (colimit (F s)))
          ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
                (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
              x :
            (fun (X : Type u) ↦ X) (colimit (F s)))),
    ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
      (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
            (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
              (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
          a =
        x
⊢ ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x

Tactic:
choose k p hk using hch
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk :
  ∀ (s : α),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          (p s) :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
⊢ ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x

Tactic:
⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Types.productIso, Exists.intro, CategoryTheory.Limits.pointwiseProduct, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk :
  ∀ (s : α),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          (p s) :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
refine_2 :
  (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
        (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
          (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
            (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
              (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
          ((hom (FC := TypeCat.Fun) (productIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)).inv :
                (a : (fun (X : Type u) ↦ X) ((j : α) → (Functor.pi F).obj k j)) →
                  (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi F).obj k))
              p :
            (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)) :
        (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))) =
    x
⊢ ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
    (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        a =
      x

Tactic:
refine ⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk :
  ∀ (s : α),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          (p s) :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
⊢ (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
        (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
          (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
            (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
              (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
          ((hom (FC := TypeCat.Fun) (productIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)).inv :
                (a : (fun (X : Type u) ↦ X) ((j : α) → (Functor.pi F).obj k j)) →
                  (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi F).obj k))
              p :
            (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)) :
        (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))) =
    x

Tactic:
Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Types.productIso, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimitPointwiseProductToProductColimit, _private.0.CategoryTheory.Limits.Types.isIso_colimitPointwiseProductToProductColimit.match_1, CategoryTheory.Limits.pointwiseProduct, CategoryTheory.Functor.pi, Eq, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.Limits.Types.limit_ext', CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk :
  ∀ (s : α),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          (p s) :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
x_1 : Discrete α
s : α
⊢ Eq (α := colimit (F s))
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := colimit (pointwiseProduct (I := I) F))
              (colimit.ι (pointwiseProduct (I := I) F) k)
              (colimitPointwiseProductToProductColimit (I := I) F ≫ Pi.π (fun (s : α) ↦ colimit (F s)) s)) :
          (a : (pointwiseProduct F).obj k) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (Iso.inv (productIso fun (j : α) ↦ (F j).obj (k j))) :
              (a : (fun (X : Type u) ↦ X) ((j : α) → (F j).obj (k j))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j)))
            p :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j))) :
      colimit (F s))
    ((hom (FC := TypeCat.Fun)
            (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k) s ≫ colimit.ι (F s) (k s)) :
          (a : (pointwiseProduct F).obj k) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (Iso.inv (productIso fun (j : α) ↦ (F j).obj (k j))) :
              (a : (fun (X : Type u) ↦ X) ((j : α) → (F j).obj (k j))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j)))
            p :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j))) :
      colimit (F s))

Tactic:
have := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s)
      ((Types.productIso _).inv p)
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
inst_1 : HasProductsOfShape.{u_1, u, v} ι C
inst_2 : IsIPCOfShape.{w, u_1, v, u} ι C
inst_3 : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst_4 : Category.{v₁, u₁} D
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → J i ⥤ Functor.{v₁, v, u₁, u} D C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
⟨evaluationJointlyReflectsColimits _ fun X ↦ ?_⟩

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
inst_1 : HasProductsOfShape.{u_1, u, v} ι C
inst_2 : IsIPCOfShape.{w, u_1, v, u} ι C
inst_3 : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst_4 : Category.{v₁, u₁} D
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → J i ⥤ Functor.{v₁, v, u₁, u} D C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
refine :
  (X : D) →
    IsColimit (F := pointwiseProduct (I := J) F ⋙ Functor.obj (evaluation D C) X)
      (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := J) c))
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
refine ⟨evaluationJointlyReflectsColimits _ fun X ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
inst_1 : HasProductsOfShape.{u_1, u, v} ι C
inst_2 : IsIPCOfShape.{w, u_1, v, u} ι C
inst_3 : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst_4 : Category.{v₁, u₁} D
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → J i ⥤ Functor.{v₁, v, u₁, u} D C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
X : D
⊢ IsColimit (F := pointwiseProduct (I := J) F ⋙ Functor.obj (evaluation D C) X)
    (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := J) c))

Tactic:
exact IsColimit.equivOfNatIsoOfIso (pointwiseProductCompEvaluation F X).symm _ _
      (evaluationCoconePointwiseProductIso F X c).symm
      (IsIPCOfShape.nonempty_isColimit fun i ↦ isColimitOfPreserves _ (hc i)).some

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.pointwiseProductCompEvaluation, Nonempty.some, CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit, CategoryTheory.Limits.evaluationCoconePointwiseProductIso, CategoryTheory.Iso.symm, DFunLike.coe, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
rw : IsConnected (StructuredArrow { as := default } F) ↔ F.Final
⊢ IsConnected.{v, u} C ↔ F.Final

Tactic:
rw [← isConnected_iff_of_equivalence
    (Discrete.structuredArrowEquivalenceOfUnique F default)]

Premises used: Inhabited.default, CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.Discrete.structuredArrowEquivalenceOfUnique
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
⊢ IsConnected (StructuredArrow { as := default } F) ↔ F.Final

Tactic:
⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Functor.Final.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
refine : IsConnected (StructuredArrow { as := default } F) → ∀ (d : Discrete T), IsConnected (StructuredArrow d F)
⊢ IsConnected (StructuredArrow { as := default } F) ↔ F.Final

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
h : IsConnected (StructuredArrow { as := default } F)
d : T
obtain : IsConnected (StructuredArrow { as := default } F)
⊢ IsConnected (StructuredArrow { as := d : Discrete T } F)

Tactic:
obtain rfl := Subsingleton.elim d default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
h : IsConnected (StructuredArrow { as := default } F)
⊢ IsConnected (StructuredArrow { as := default } F)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
rw : IsConnected (CostructuredArrow F { as := default }) ↔ F.Initial
⊢ IsConnected.{v, u} C ↔ F.Initial

Tactic:
rw [← isConnected_iff_of_equivalence
    (Discrete.costructuredArrowEquivalenceOfUnique F default)]

Premises used: Inhabited.default, CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.Discrete.costructuredArrowEquivalenceOfUnique
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
⊢ IsConnected (CostructuredArrow F { as := default }) ↔ F.Initial

Tactic:
⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Functor.Initial.mk, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
refine : IsConnected (CostructuredArrow F { as := default }) → ∀ (d : Discrete T), IsConnected (CostructuredArrow F d)
⊢ IsConnected (CostructuredArrow F { as := default }) ↔ F.Initial

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
h : IsConnected (CostructuredArrow F { as := default })
d : T
obtain : IsConnected (CostructuredArrow F { as := default })
⊢ IsConnected (CostructuredArrow F { as := d })

Tactic:
obtain rfl := Subsingleton.elim d default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
inst_1 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
h : IsConnected (CostructuredArrow F { as := default })
⊢ IsConnected (CostructuredArrow F { as := default })

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
T : Type w
inst_2 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
inst_3 rwa rwa₁ rwa₂ rwa₃ : IsConnected.{v, u} C
⊢ F.Final

Tactic:
rwa [← isConnected_iff_final_of_unique F]

Premises used: CategoryTheory.isConnected_iff_final_of_unique
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
T : Type w
inst_2 : Unique T
F : Functor.{v, w, u, w} C (Discrete T)
inst_3 rwa rwa₁ rwa₂ rwa₃ : IsConnected.{v, u} C
⊢ F.Initial

Tactic:
rwa [← isConnected_iff_initial_of_unique F]

Premises used: CategoryTheory.isConnected_iff_initial_of_unique
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
T : Type w
inst_2 : Unique T
inst_3 : IsConnected.{v', u'} D
⊢ Functor.Final (Prod.fst C D)

Tactic:
inferInstanceAs (Functor.prod (𝟭 C) ((Functor.const _).obj (Discrete.mk .unit)) ⋙
    (prod.rightUnitorEquivalence.{0} C).functor).Final

Premises used: _private.0.CategoryTheory.final_fst._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
T : Type w
inst_2 : Unique T
inst_3 : IsConnected.{v, u} C
⊢ Functor.Final (Prod.snd C D)

Tactic:
inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Final

Premises used: _private.0.CategoryTheory.final_snd._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
T : Type w
inst_2 : Unique T
inst_3 : IsConnected.{v', u'} D
⊢ Functor.Initial (Prod.fst C D)

Tactic:
inferInstanceAs (Functor.prod (𝟭 C) ((Functor.const _).obj (Discrete.mk .unit)) ⋙
    (prod.rightUnitorEquivalence.{0} C).functor).Initial

Premises used: _private.0.CategoryTheory.initial_fst._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final.Connected
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
T : Type w
inst_2 : Unique T
inst_3 : IsConnected.{v, u} C
⊢ Functor.Initial (Prod.snd C D)

Tactic:
inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Initial

Premises used: _private.0.CategoryTheory.initial_snd._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty.{v_1 + 1} (X ⟶ Z)
h₂ :
  ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
    Zigzag.{0, v_1} (J := CostructuredArrow (parallelPair f g) Z) (mk (Y := zero) i) (mk (Y := zero) j)
Z : C
⊢ Nonempty.{max 1 (v_1 + 1)} (CostructuredArrow (parallelPair f g) Z)

Tactic:
have : Nonempty (CostructuredArrow (parallelPair f g) Z) :=
      ⟨mk (Y := zero) (h₁ Z).some⟩