awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : P Y ∨ Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X
have h : ∀ (hY : P Y), P.isoClosure X ∨ Q.isoClosure X
Tactic: obtain hY | hY := hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : P Y ∨ Q Y
h : ∀ (hY : P Y), P.isoClosure X ∨ Q.isoClosure X
⊢ P.isoClosure X ∨ Q.isoClosure X
have h₁ : ∀ (hY : Q Y), P.isoClosure X ∨ Q.isoClosure X
Tactic: obtain hY | hY := hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)
have refine_1 : LE.le.{u} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
refine_1 : LE.le.{u} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)
have refine_2 : LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), (P a).isoClosure) (isoClosure (⨆ (a : α), P a))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X Y : C
hY : (⨆ (a : α), P a) Y
e : X ≅ Y
⊢ (⨆ (a : α), (P a).isoClosure) X
have refine_1 : ∀ (hY : ∃ (a : α), P a Y), ∃ (a : α), (P a).isoClosure X
Tactic: simp only [prop_iSup_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : ∃ (a : α), P a Y
⊢ ∃ (a : α), (P a).isoClosure X
have refine_1 : ∀ (a : α) (hY : P a Y), ∃ (a : α), (P a).isoClosure X
Tactic: obtain ⟨a, hY⟩ := hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
⊢ LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), (P a).isoClosure) (isoClosure (⨆ (a : α), P a))
have refine_2 : ∀ (i : α), (P i).isoClosure ≤ isoClosure (⨆ (a : α), P a)
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
a : α
⊢ (P a).isoClosure ≤ isoClosure (⨆ (a : α), P a)
have refine_2 : P a ≤ isoClosure (⨆ (a : α), P a)
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.Nonempty ↔ ¬P = ⊥
have rw : P.Nonempty ↔ ∃ (X : C), P X
Tactic: rw [ne_bot_iff_exists, nonempty_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
rw : P.Nonempty ↔ ∃ (X : C), P X
⊢ P.Nonempty ↔ ¬P = ⊥
have rw₁ : (∃ (X : C), P X) ↔ ∃ (X : C), P X
Tactic: rw [ne_bot_iff_exists, nonempty_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ ¬P.Nonempty ↔ P = ⊥
have rw : ¬¬P = ⊥ ↔ P = ⊥
Tactic: rw [P.nonempty_iff_ne_bot, not_not]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
rw : ¬¬P = ⊥ ↔ P = ⊥
⊢ ¬P.Nonempty ↔ P = ⊥
have rw₁ : P = ⊥ ↔ P = ⊥
Tactic: rw [P.nonempty_iff_ne_bot, not_not]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ map ⊤ P.ι = P.isoClosure
have h : ∀ (X : C), map ⊤ P.ι X ↔ P.isoClosure X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ map ⊤ P.ι X ↔ P.isoClosure X
have h : map ⊤ P.ι X → P.isoClosure X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
h : map ⊤ P.ι X → P.isoClosure X
⊢ map ⊤ P.ι X ↔ P.isoClosure X
have h₁ : P.isoClosure X → map ⊤ P.ι X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero.{v, u} Z
⊢ P Z
have obtain : ∀ (Z₀ : C) (hZ₀ : IsZero.{v, u} Z₀) (h₀ : P Z₀), P Z
Tactic: obtain ⟨Z₀, hZ₀, h₀⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasZeroMorphisms.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
⊢ ∃ (Z : D), IsZero.{v', u'} Z ∧ P.map F Z
have obtain : ∀ (Z : C) (h₁ : IsZero.{v, u} Z) (h₂ : P Z), ∃ (Z : D), IsZero.{v', u'} Z ∧ P.map F Z
Tactic: obtain ⟨Z, h₁, h₂⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.isoClosure Z
have obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (hP : P Z), ∃ (Z : C), IsZero.{v, u} Z ∧ P.isoClosure Z
Tactic: obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : Q.ContainsZero
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z
have obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (hQ : Q Z), ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z
Tactic: obtain ⟨Z, hZ, hQ⟩ := Q.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
⊢ ∃ (Z : Cᵒᵖ), IsZero.{v, u} Z ∧ P.op Z
have obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (mem : P Z), ∃ (Z : Cᵒᵖ), IsZero.{v, u} Z ∧ P.op Z
Tactic: obtain ⟨Z, hZ, mem⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P_1 Q : ObjectProperty.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
inst_2 : ContainsZero.{v, u} P
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.unop Z
have obtain : ∀ (Z : Cᵒᵖ) (hZ : IsZero.{v, u} Z) (mem : P Z), ∃ (Z : C), IsZero.{v, u} Z ∧ P.unop Z
Tactic: obtain ⟨Z, hZ, mem⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
⊢ ∃ (X : P.FullSubcategory), IsZero.{v, u} X
have obtain : ∀ (X : C) (h₁ : IsZero.{v, u} X) (h₂ : P X), ∃ (X : P.FullSubcategory), IsZero.{v, u} X
Tactic: obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ContainsZero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : Q.ContainsZero
inst_4 : Q.IsClosedUnderIsomorphisms
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z
have obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (hP : P Z), ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z
Tactic: obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.EpiMono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderSubobjects
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₁
have have : ∀ (this : Mono S.f), P S.X₁
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.EpiMono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderQuotients
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₃
have have : ∀ (this : Epi S.g), P S.X₃
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Equivalence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ (ιOfLE (P := P) (P' := Q) h).EssSurj ↔ Q ≤ P.isoClosure
have refine_1 : (ιOfLE (P := P) (P' := Q) h).EssSurj → ∀ (X : C) (hX : Q X), P.isoClosure X
Tactic: refine ⟨fun _ X hX ↦ ?_, fun hPQ ↦ ⟨fun ⟨Y, hY⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Equivalence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
refine_1 : (ιOfLE (P := P) (P' := Q) h).EssSurj → ∀ (X : C) (hX : Q X), P.isoClosure X
⊢ (ιOfLE (P := P) (P' := Q) h).EssSurj ↔ Q ≤ P.isoClosure
have refine_2 : ∀ (hPQ : Q ≤ P.isoClosure) (x : Q.FullSubcategory) (Y : C) (hY : Q Y),
  (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)
Tactic: refine ⟨fun _ X hX ↦ ?_, fun hPQ ↦ ⟨fun ⟨Y, hY⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Equivalence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x : Q.FullSubcategory
Y : C
hY : Q Y
⊢ (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)
have refine_2 : ∀ (X : C) (hX : P X) (e : Y ≅ X), (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)
Tactic: obtain ⟨X, hX, ⟨e⟩⟩ := hPQ _ hY
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Equivalence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ (ιOfLE (P := P) (P' := Q) h).IsEquivalence ↔ Q ≤ P.isoClosure
have rw : (ιOfLE (P := P) (P' := Q) h).IsEquivalence ↔ (ιOfLE (P := P) (P' := Q) h).EssSurj
Tactic: rw [← essSurj_ιOfLE_iff h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Equivalence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ (ιOfLE (P := P) (P' := P.isoClosure) ⋯).IsEquivalence
have rw : P.isoClosure ≤ P.isoClosure
Tactic: rw [isEquivalence_ιOfLE_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Extensions (hypothesis)
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₃
⊢ P.inverseImage F S.X₂
have this : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Extensions (hypothesis)
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
⊢ P.inverseImage F S.X₂
have this₁ : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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
have refine : ∀ (h : P ≤ Q), P.binaryProductsClosure ≤ Q
Tactic: refine ⟨fun h ↦ (P.le_limitsClosure _).trans h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)
have rw : IsClosedUnderLimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))
Tactic: rw [P.isClosedUnderLimitsOfShape_iff_of_equivalence (Discrete.equivalence (equivShrink.{w} _))]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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
⊢ IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
have obtain : ∀ (n : ℕ) (e : J ≃ Fin n), IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
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
⊢ IsClosedUnderLimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
have this : P.IsClosedUnderLimitsOfShape (Discrete (Fin n))
Tactic: have : P.IsClosedUnderLimitsOfShape (Discrete (Fin n)) :=
    IsClosedUnderFiniteProducts.isClosedUnderLimitsOfShape _
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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
⊢ P X
have obtain : ∀ (Z : C) (hZ : IsZero.{v_1, u_1} Z) (hZ₂ : P Z), P X
Tactic: obtain ⟨Z, hZ, hZ₂⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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
⊢ P X
have have : ∀ (hX : IsTerminal.{v_1, u_1} X), P X
Tactic: have hX : IsTerminal X :=
      (IsLimit.equivOfNatIsoOfIso p.diag.uniqueFromEmpty _ _
        (by exact Cone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩))).1 p.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
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.IsClosedUnderFiniteProducts
have this : P.IsClosedUnderIsomorphisms
Tactic: have := IsClosedUnderBinaryProducts.closedUnderIsomorphisms P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
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
⊢ P.IsClosedUnderFiniteProducts
have this₁ : HasFiniteProducts.{v_1, u_1} P.FullSubcategory
Tactic: have := hasFiniteProducts_of_has_binary_and_terminal (C := P.FullSubcategory)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
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
⊢ P.IsClosedUnderFiniteProducts
have this₁ : PreservesFiniteProducts P.ι
Tactic: have := PreservesFiniteProducts.of_preserves_binary_and_terminal P.ι
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryCoproducts
inst_3 : Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q
have refine : ∀ (h : P ≤ Q), P.binaryCoproductsClosure ≤ Q
Tactic: refine ⟨fun h ↦ (P.le_colimitsClosure _).trans h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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], IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)
have rw : IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))
Tactic: rw [P.isClosedUnderColimitsOfShape_iff_of_equivalence
      (Discrete.equivalence (equivShrink.{w} _))]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
⊢ IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
have obtain : ∀ (n : ℕ) (e : J ≃ Fin n), IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
⊢ IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
have this : P.IsClosedUnderColimitsOfShape (Discrete (Fin n))
Tactic: have : P.IsClosedUnderColimitsOfShape (Discrete (Fin n)) :=
    IsClosedUnderFiniteCoproducts.isClosedUnderColimitsOfShape _
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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.ColimitOfShape (Discrete PEmpty.{1}) X
⊢ P X
have obtain : ∀ (Z : C) (hZ : IsZero.{v_1, u_1} Z) (hZ₂ : P Z), P X
Tactic: obtain ⟨Z, hZ, hZ₂⟩ := P.exists_prop_of_containsZero
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (goal)
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.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
⊢ P X
have have : ∀ (hX : IsInitial.{v_1, u_1} X), P X
Tactic: have hX : IsInitial X :=
      (IsColimit.equivOfNatIsoOfIso p.diag.uniqueFromEmpty _ _
        (by exact Cocone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩))).1 p.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
⊢ P.IsClosedUnderFiniteCoproducts
have this : P.IsClosedUnderIsomorphisms
Tactic: have := IsClosedUnderBinaryCoproducts.closedUnderIsomorphisms P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
this : P.IsClosedUnderIsomorphisms
⊢ P.IsClosedUnderFiniteCoproducts
have this₁ : HasFiniteCoproducts.{v_1, u_1} P.FullSubcategory
Tactic: have := hasFiniteCoproducts_of_has_binary_and_initial (C := P.FullSubcategory)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FiniteProducts (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
this_1 : P.IsClosedUnderIsomorphisms
this : HasFiniteCoproducts.{v_1, u_1} P.FullSubcategory
⊢ P.IsClosedUnderFiniteCoproducts
have this₁ : ∀ (J : Type) [Finite J], PreservesColimitsOfShape (Discrete J) P.ι
Tactic: have := PreservesFiniteCoproducts.of_preserves_binary_and_initial P.ι
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesLimit F) (preservesLimit F')
have h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C), preservesLimit F G ↔ preservesLimit F' G
Tactic: ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesColimit F) (preservesColimit F')
have h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C), preservesColimit F G ↔ preservesColimit F' G
Tactic: ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesLimit F)
have h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
  preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesLimit F) G
Tactic: ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesLimit F) G
have h : PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔ ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesLimit i G
Tactic: simp only [preservesLimitsOfShape_iff, iInf_apply, preservesLimit_iff, iInf_Prop_eq]