awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v₁, u₁} P J X
⊢ f = g

Tactic:
p.isColimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.mk, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
J : Type w
w : Category.{w', w} J
p : ColimitOfShape.{w', w, v₁, u₁} P J X
⊢ f = g

Tactic:
exact p.isColimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.mk, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), limitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
obtain : ∀ (J : Type w) (w : Category.{w', w} J) (p : LimitOfShape.{w', w, v₁, u₁} P J Y), f = g
⊢ f = g

Tactic:
obtain ⟨J, _, ⟨p⟩⟩ := hP Y
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), limitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
J : Type w
w : Category.{w', w} J
p : LimitOfShape.{w', w, v₁, u₁} P J Y
⊢ f = g

Tactic:
p.isLimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Limits.LimitPresentation.π, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), limitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
J : Type w
w : Category.{w', w} J
p : LimitOfShape.{w', w, v₁, u₁} P J Y
⊢ f = g

Tactic:
exact p.isLimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Limits.LimitPresentation.π, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : ObjectProperty.{v₁, u₁} C
X : C
inst_2 : HasCoproduct (P.coproductFromFamily X)
Y : C
f : Y ⟶ X
hY : P Y
⊢ P.ι.obj (FullSubcategory.mk (P := P) Y hY) ⟶ X

Tactic:
exact f
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : ObjectProperty.{v₁, u₁} C
X : C
inst_2 : HasCoproduct (P.coproductFromFamily X)
Y : C
f : Y ⟶ X
hY : P Y
⊢ Y ⟶ ∐ P.coproductFromFamily X

Tactic:
exact Sigma.ι (P.coproductFromFamily X) (CostructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))

Premises used: CategoryTheory.Limits.Sigma.ι, CategoryTheory.ObjectProperty.coproductFromFamily, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X : C
inst_1 : HasCoproduct (P.coproductFromFamily X)
Z : C
u v : X ⟶ Z
huv : Eq (α := ∐ P.coproductFromFamily X ⟶ Z) (P.coproductFrom X ≫ u) (P.coproductFrom X ≫ v)
G : C
hG : P G
h : G ⟶ X
⊢ h ≫ u = h ≫ v

Tactic:
simpa using P.ιCoproductFrom h hG ≫= huv

Premises used: CategoryTheory.ObjectProperty.ιCoproductFrom
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : ∀ (X : C), HasCoproduct (P.coproductFromFamily X)
⊢ P.IsSeparating ↔ ∀ (X : C), Epi (X := ∐ P.coproductFromFamily X) (P.coproductFrom X)

Tactic:
⟨fun hP X ↦ hP.epi_coproductFrom X,
    fun hP ↦ IsSeparating.mk_of_exists_epi (fun X ↦ ⟨_, P.coproductFromFamily X,
      fun i ↦ i.left.2, _, colimit.isColimit _, _, hP X⟩)⟩

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.CostructuredArrow, CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_epi, CategoryTheory.ObjectProperty.coproductFromFamily, Iff.intro, Exists.intro, CategoryTheory.Limits.colimit.cocone, CategoryTheory.ObjectProperty.coproductFrom, CategoryTheory.CostructuredArrow.left, CategoryTheory.ObjectProperty.IsSeparating.epi_coproductFrom
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : ObjectProperty.{v₁, u₁} C
X : C
inst_2 : HasProduct (P.productToFamily X)
Y : C
f : X ⟶ Y
hY : P Y
⊢ X ⟶ P.ι.obj (FullSubcategory.mk (P := P) Y hY)

Tactic:
exact f
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : ObjectProperty.{v₁, u₁} C
X : C
inst_2 : HasProduct (P.productToFamily X)
Y : C
f : X ⟶ Y
hY : P Y
⊢ ∏ᶜ P.productToFamily X ⟶ Y

Tactic:
exact Pi.π (P.productToFamily X) (StructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))

Premises used: CategoryTheory.ObjectProperty.productToFamily, CategoryTheory.Limits.Pi.π, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X : C
inst_1 : HasProduct (P.productToFamily X)
Z : C
u v : Z ⟶ X
huv : Eq (α := Z ⟶ ∏ᶜ P.productToFamily X) (u ≫ P.productTo X) (v ≫ P.productTo X)
G : C
hG : P G
h : X ⟶ G
⊢ u ≫ h = v ≫ h

Tactic:
simpa using huv =≫ P.πProductTo h hG

Premises used: CategoryTheory.ObjectProperty.πProductTo
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : ∀ (X : C), HasProduct (P.productToFamily X)
⊢ P.IsCoseparating ↔ ∀ (X : C), Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)

Tactic:
⟨fun hP X ↦ hP.mono_productTo X,
    fun hP ↦ IsCoseparating.mk_of_exists_mono (fun X ↦ ⟨_, P.productToFamily X,
      fun i ↦ i.right.2, _, limit.isLimit _, _, hP X⟩)⟩

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.productToFamily, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Discrete.functor, CategoryTheory.Limits.limit.cone, CategoryTheory.ObjectProperty.productTo, CategoryTheory.Limits.limit.isLimit, CategoryTheory.ObjectProperty.IsCoseparating.mono_productTo, Iff.intro, Exists.intro, CategoryTheory.StructuredArrow.right, CategoryTheory.StructuredArrow, CategoryTheory.ObjectProperty.IsCoseparating.mk_of_exists_mono
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
⊢ HasFiniteLimits.{v₁, u₁} C

Tactic:
have := hasFiniteLimits_of_hasLimitsOfSize C
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this : HasFiniteLimits.{v₁, u₁} C
⊢ HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C

Tactic:
haveI := hasProductsOfShape_of_small C (Subtype P)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
⊢ ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C

Tactic:
haveI := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this :
  (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)
⊢ HasInitial.{v₁, u₁} C

Tactic:
hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)

Premises used: CategoryTheory.Subobject.underlying, CategoryTheory.Limits.hasInitial_of_unique, Bot.bot, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this :
  (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)
⊢ HasInitial.{v₁, u₁} C

Tactic:
exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)

Premises used: CategoryTheory.Subobject.underlying, CategoryTheory.Limits.hasInitial_of_unique, Bot.bot, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
suffices :
  (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)
⊢ HasInitial.{v₁, u₁} C

Tactic:
suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
    exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
⊢ ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)

Tactic:
have := hP.mono_productTo
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
refine_1 :
  (A : C) →
    Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      A
refine_2 :
  ∀ (A : C)
    (f :
      Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A),
    f = default
⊢ (A : C) →
    Unique
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A)

Tactic:
refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
s : piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)) ⟶ ∏ᶜ P.productToFamily A :=
  Pi.lift fun (f : StructuredArrow A P.ι) ↦ Pi.π (Subtype.val (p := P)) (Subtype.mk (p := P) (f.right.obj (P := P)) ⋯)
⊢ Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A

Tactic:
exact Subobject.ofLEMk _
      (pullback.fst _ _ : pullback s (P.productTo A) ⟶ _) bot_le ≫ pullback.snd _ _

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.fst, CategoryTheory.Subobject.ofLEMk, bot_le
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this_5 : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
this :
  ∀
    (g :
      Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A),
    f = g
⊢ f = default

Tactic:
apply this
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
refine_2 :
  ∀
    (g :
      Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        A),
    f = g
⊢ f = default

Tactic:
suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
      apply this
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this_5 : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
this : IsSplitEpi (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
eq_of_epi_equalizer

Premises used: CategoryTheory.Limits.eq_of_epi_equalizer
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this_5 : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
this : IsSplitEpi (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
exact eq_of_epi_equalizer

Premises used: CategoryTheory.Limits.eq_of_epi_equalizer
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
refine_2 : IsSplitEpi (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer