awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
rw rw₁ : P.isoClosure ≤ P.isoClosure
⊢ (ιOfLE (P := P) (P' := P.isoClosure) ⋯).IsEquivalence

Tactic:
rw [isEquivalence_ιOfLE_iff]

Premises used: CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ ∀ (X : C), ⊤ (Functor.obj.{v, v, u, u} (𝟭 C) X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : P.IsClosedUnderExtensions
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₁ : P S.X₁
h₃ : P S.X₃
⊢ P S.X₂

Tactic:
IsClosedUnderExtensions.prop_X₂_of_shortExact hS h₁ h₃

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderExtensions.prop_X₂_of_shortExact
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
⊢ ∀ {S : ShortComplex.{v, u} C} (hS : S.ShortExact) (h₁ : ⊤ S.X₁) (h₃ : ⊤ S.X₃), ⊤ S.X₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : P.IsClosedUnderExtensions
F : Functor.{v', v, u', u} D C
inst_4 : HasZeroMorphisms.{v', u'} D
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits F
inst_7 : PreservesFiniteColimits F
S : ShortComplex.{v', u'} D
hS : S.ShortExact
h₁ : P.inverseImage F S.X₁
h₃ : P.inverseImage F S.X₃
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : P.IsClosedUnderExtensions
F : Functor.{v', v, u', u} D C
inst_4 : HasZeroMorphisms.{v', u'} D
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits F
inst_7 : PreservesFiniteColimits F
S : ShortComplex.{v', u'} D
hS : S.ShortExact
h₁ : P.inverseImage F S.X₁
h₃ : P.inverseImage F S.X₃
this : Mono S.f
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : P.IsClosedUnderExtensions
F : Functor.{v', v, u', u} D C
inst_4 : HasZeroMorphisms.{v', u'} D
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits F
inst_7 : PreservesFiniteColimits F
S : ShortComplex.{v', u'} D
hS : S.ShortExact
h₁ : P.inverseImage F S.X₁
h₃ : P.inverseImage F S.X₃
this_1 : Mono S.f
this : Epi S.g
⊢ P.inverseImage F S.X₂

Tactic:
P.prop_X₂_of_shortExact (hS.map F) h₁ h₃

Premises used: CategoryTheory.ShortComplex.ShortExact.map, CategoryTheory.ObjectProperty.prop_X₂_of_shortExact, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : P.IsClosedUnderExtensions
F : Functor.{v', v, u', u} D C
inst_4 : HasZeroMorphisms.{v', u'} D
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits F
inst_7 : PreservesFiniteColimits F
S : ShortComplex.{v', u'} D
hS : S.ShortExact
h₁ : P.inverseImage F S.X₁
h₃ : P.inverseImage F S.X₃
this_1 : Mono S.f
this : Epi S.g
⊢ P.inverseImage F S.X₂

Tactic:
exact P.prop_X₂_of_shortExact (hS.map F) h₁ h₃

Premises used: CategoryTheory.ShortComplex.ShortExact.map, CategoryTheory.ObjectProperty.prop_X₂_of_shortExact
-- Module: Mathlib.CategoryTheory.ObjectProperty.Extensions
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X₁ X₂ : C
h₁ : P X₁
h₂ : P X₂
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : P.IsClosedUnderExtensions
inst_4 : HasBinaryBiproduct.{v, u} X₁ X₂
⊢ P (biprod.{v, u} X₁ X₂)

Tactic:
P.prop_X₂_of_shortExact
    (ShortComplex.Splitting.ofHasBinaryBiproduct X₁ X₂).shortExact h₁ h₂

Premises used: CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct, CategoryTheory.ObjectProperty.prop_X₂_of_shortExact, CategoryTheory.ShortComplex.Splitting.shortExact
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan.{v_1, u_1} X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ P (Functor.obj.{0, v_1, 0, u_1} (Limits.pair X Y) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan.{v_1, u_1} X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ P (Functor.obj.{0, v_1, 0, u_1} (Limits.pair X Y) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderBinaryProducts
X Y : C
inst_2 : HasBinaryProduct.{v_1, u_1} X Y
hX : P X
hY : P Y
⊢ P (Limits.prod.{v_1, u_1} X Y)

Tactic:
P.prop_of_isLimit_binaryFan (limit.isLimit _) hX hY

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_2 : HasTerminal.{v_1, u_1} C
⊢ P (terminal.{v_1, u_1} C)

Tactic:
P.prop_of_isTerminal _ terminalIsTerminal

Premises used: CategoryTheory.ObjectProperty.prop_of_isTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_2 : HasTerminal.{v_1, u_1} C
⊢ P.Nonempty

Tactic:
nonempty_of_prop P.prop_terminal

Premises used: CategoryTheory.ObjectProperty.nonempty_of_prop, CategoryTheory.ObjectProperty.prop_terminal
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : T ⟶ terminal.{v_1, u_1} C) (g : T ⟶ X),
    CategoryStruct.comp (Y :=
        Cone.pt (F := Limits.pair (terminal.{v_1, u_1} C) X) (BinaryFan.mk (terminal.from Y) e.inv))
        ((fun {T : C} (x : T ⟶ terminal.{v_1, u_1} C) (f : T ⟶ X) ↦ f ≫ e.hom) f g :
          T ⟶ Cone.pt (F := Limits.pair (terminal.{v_1, u_1} C) X) (BinaryFan.mk (terminal.from Y) e.inv))
        (BinaryFan.snd (BinaryFan.mk (terminal.from Y) e.inv) :
          Functor.obj.{0, v_1, 0, u_1}
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cone.pt (F := Limits.pair (terminal.{v_1, u_1} C) X) (BinaryFan.mk (terminal.from Y) e.inv)))
              { as := WalkingPair.right : Discrete WalkingPair } ⟶
            Functor.obj.{0, v_1, 0, u_1} (Limits.pair (terminal.{v_1, u_1} C) X)
              { as := WalkingPair.right : Discrete WalkingPair }) =
      g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
let : P Y
⊢ P Y

Tactic:
let h : IsLimit (BinaryFan.mk (terminal.from Y) e.inv) :=
      BinaryFan.IsLimit.mk _ (fun _ f ↦ f ≫ e.hom) (by cat_disch) (by simp) (by cat_disch)
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
h : IsLimit (F := Limits.pair (terminal.{v_1, u_1} C) X) (BinaryFan.mk (terminal.from Y) e.inv) :=
  BinaryFan.IsLimit.mk (BinaryFan.mk (terminal.from Y) e.inv)
    (fun {T : C} (x : T ⟶ terminal.{v_1, u_1} C) (f : T ⟶ X) ↦ f ≫ e.hom) ⋯ ⋯ ⋯
⊢ P Y

Tactic:
P.prop_of_isLimit_binaryFan h P.prop_terminal hX

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan, CategoryTheory.ObjectProperty.prop_terminal
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
h : IsLimit (F := Limits.pair (terminal.{v_1, u_1} C) X) (BinaryFan.mk (terminal.from Y) e.inv) :=
  BinaryFan.IsLimit.mk (BinaryFan.mk (terminal.from Y) e.inv)
    (fun {T : C} (x : T ⟶ terminal.{v_1, u_1} C) (f : T ⟶ X) ↦ f ≫ e.hom) ⋯ ⋯ ⋯
⊢ P Y

Tactic:
exact P.prop_of_isLimit_binaryFan h P.prop_terminal hX

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan, CategoryTheory.ObjectProperty.prop_terminal
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryProducts
inst_3 : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryProductsClosure ≤ Q ↔ P ≤ Q

Tactic:
⟨fun h ↦ (P.le_limitsClosure _).trans h, fun h ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.le_limitsClosure, CategoryTheory.Limits.WalkingPair, Iff.intro, LE.le.trans, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryProducts
inst_3 : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
refine : ∀ (h : P ≤ Q), P.binaryProductsClosure ≤ Q
⊢ P.binaryProductsClosure ≤ Q ↔ P ≤ Q

Tactic:
refine ⟨fun h ↦ (P.le_limitsClosure _).trans h, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryProducts
inst_3 : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
h : P ≤ Q
this : Q.IsClosedUnderIsomorphisms := ⋯
⊢ P.binaryProductsClosure ≤ Q

Tactic:
limitsClosure_le h

Premises used: CategoryTheory.ObjectProperty.limitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasTerminal.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryProducts
inst_3 : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
h : P ≤ Q
this : Q.IsClosedUnderIsomorphisms := ⋯
⊢ P.binaryProductsClosure ≤ Q

Tactic:
exact limitsClosure_le h

Premises used: CategoryTheory.ObjectProperty.limitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
H : ∀ (J : Type w) [Finite J], IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
rw : IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)

Tactic:
rw [P.isClosedUnderLimitsOfShape_iff_of_equivalence (Discrete.equivalence (equivShrink.{w} _))]
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
H : ∀ (J : Type w) [Finite J], IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
⊢ IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))

Tactic:
H _
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
H : ∀ (J : Type w) [Finite J], IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
⊢ IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))

Tactic:
exact H _
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
obtain : ∀ (n : ℕ) (e : J ≃ Fin n), IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
⊢ IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
⊢ P.IsClosedUnderLimitsOfShape (Discrete (Fin n))

Tactic:
have : P.IsClosedUnderLimitsOfShape (Discrete (Fin n)) :=
    IsClosedUnderFiniteProducts.isClosedUnderLimitsOfShape _
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
this : P.IsClosedUnderLimitsOfShape (Discrete (Fin n))
⊢ IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)

Tactic:
IsClosedUnderLimitsOfShape.of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, Equiv.symm, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.of_equivalence
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
this : P.IsClosedUnderLimitsOfShape (Discrete (Fin n))
⊢ IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)

Tactic:
exact IsClosedUnderLimitsOfShape.of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, Equiv.symm, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.of_equivalence
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
f : J → C
F : Fan.{u_2, v_1, u_1} f
hF : IsLimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P (Functor.obj.{u_2, v_1, u_2, u_1} (Discrete.functor f) { as := j : Discrete J })

Tactic:
h j
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
f : J → C
F : Fan.{u_2, v_1, u_1} f
hF : IsLimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P (Functor.obj.{u_2, v_1, u_2, u_1} (Discrete.functor f) { as := j : Discrete J })

Tactic:
exact h j
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteProducts
J : Type u_2
inst_2 : Finite J
f : J → C
inst_3 : HasProduct.{u_2, v_1, u_1} f
h : ∀ (j : J), P (f j)
⊢ P (piObj.{u_2, v_1, u_1} f)

Tactic:
P.prop_of_isLimit_fan (limit.isLimit (Discrete.functor f)) h

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.ObjectProperty.prop_of_isLimit_fan, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
obtain : ∀ (Z : C) (hZ : IsZero.{v_1, u_1} Z) (hZ₂ : P Z), P X
⊢ P X

Tactic:
obtain ⟨Z, hZ, hZ₂⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
⊢ (Cone.postcompose p.toLimitPresentation (P := P).diag.uniqueFromEmpty.hom).obj
      { pt := X, π := p.toLimitPresentation (P := P).π : Cone p.toLimitPresentation (P := P).diag } ≅
    asEmptyCone X

Tactic:
exact Cone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
have : ∀ (hX : IsTerminal.{v_1, u_1} X), P X
⊢ P X

Tactic:
have hX : IsTerminal X :=
      (IsLimit.equivOfNatIsoOfIso p.diag.uniqueFromEmpty _ _
        (by exact Cone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩))).1 p.isLimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
hX : IsTerminal.{v_1, u_1} X
⊢ P X

Tactic:
P.prop_of_isZero (IsZero.of_iso hZ
      (IsLimit.conePointUniqueUpToIso hX (IsZero.isTerminal hZ)))

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Limits.IsZero.isTerminal, CategoryTheory.ObjectProperty.prop_of_isZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
hX : IsTerminal.{v_1, u_1} X
⊢ P X

Tactic:
exact P.prop_of_isZero (IsZero.of_iso hZ
      (IsLimit.conePointUniqueUpToIso hX (IsZero.isTerminal hZ)))

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Limits.IsZero.isTerminal, CategoryTheory.ObjectProperty.prop_of_isZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteProducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
⊢ P.IsClosedUnderIsomorphisms

Tactic:
have := IsClosedUnderBinaryProducts.closedUnderIsomorphisms P
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteProducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
this : P.IsClosedUnderIsomorphisms
⊢ HasFiniteProducts.{v_1, u_1} P.FullSubcategory

Tactic:
have := hasFiniteProducts_of_has_binary_and_terminal (C := P.FullSubcategory)
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteProducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
this_1 : P.IsClosedUnderIsomorphisms
this : HasFiniteProducts.{v_1, u_1} P.FullSubcategory
⊢ PreservesFiniteProducts P.ι

Tactic:
have := PreservesFiniteProducts.of_preserves_binary_and_terminal P.ι
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteProducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
this_1 : P.IsClosedUnderIsomorphisms
this_2 : HasFiniteProducts.{v_1, u_1} P.FullSubcategory
this : PreservesFiniteProducts P.ι
⊢ P.IsClosedUnderFiniteProducts

Tactic:
⟨fun J _ ↦ P.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι _⟩

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.mk, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteProducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryProducts
this_1 : P.IsClosedUnderIsomorphisms
this_2 : HasFiniteProducts.{v_1, u_1} P.FullSubcategory
this : PreservesFiniteProducts P.ι
⊢ P.IsClosedUnderFiniteProducts

Tactic:
exact ⟨fun J _ ↦ P.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι _⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan.{v_1, u_1} X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ P (Functor.obj.{0, v_1, 0, u_1} (Limits.pair X Y) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan.{v_1, u_1} X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ P (Functor.obj.{0, v_1, 0, u_1} (Limits.pair X Y) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderBinaryCoproducts
X Y : C
inst_2 : HasBinaryCoproduct.{v_1, u_1} X Y
hX : P X
hY : P Y
⊢ P (coprod.{v_1, u_1} X Y)

Tactic:
P.prop_of_isColimit_binaryCofan (colimit.isColimit (Limits.pair X Y)) hX hY

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_2 : HasInitial.{v_1, u_1} C
⊢ P (initial.{v_1, u_1} C)

Tactic:
P.prop_of_isInitial _ initialIsInitial

Premises used: CategoryTheory.ObjectProperty.prop_of_isInitial, CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_2 : HasInitial.{v_1, u_1} C
⊢ P.Nonempty

Tactic:
nonempty_of_prop P.prop_initial

Premises used: CategoryTheory.ObjectProperty.prop_initial, CategoryTheory.ObjectProperty.nonempty_of_prop