awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h : IsFiltered x
a :
  (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) →
    ∀ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X))
      (h : ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)),
      ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
⊢ (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) ↔
    ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
have a₁ : (∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)) →
  ∀ (pres : ColimitPresentation.{w, w, u_2, u_1} x X) (h : ∀ (i : x), P (pres.diag.obj i)),
    ∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)
Tactic: refine ⟨fun ⟨pres, h⟩ ↦ ?_, fun ⟨pres, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type w
inst_1 : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete ι)
inst_2 : HasProductsOfShape.{w, u, v} ι C
inst_3 : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
hc : ∀ (i : ι), P.ind (X i)
⊢ P.ind (piObj.{w, v, u} X)
have choose : ∀ (J : (i : ι) → Type w) (x : (i : ι) → SmallCategory (J i)),
  (∀ (i : ι), IsFiltered.{w, w} (J i)) →
    ∀ (pres : (i : ι) → ColimitPresentation.{w, w, v, u} (J i) (X i))
      (hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)), P.ind (piObj.{w, v, u} X)
Tactic: choose J _ _ pres hpres using hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type w
inst_1 : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete ι)
inst_2 : HasProductsOfShape.{w, u, v} ι C
inst_3 : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
J : (i : ι) → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
pres : (i : ι) → ColimitPresentation.{w, w, v, u} (J i) (X i)
hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)
⊢ P.ind (piObj.{w, v, u} X)
have obtain : ∀
  (hc :
    IsColimit.{w, v, w, u} (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) fun (i : ι) ↦ (pres i).diag)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ { pt := X i, ι := (pres i).ι })),
  P.ind (piObj.{w, v, u} X)
Tactic: obtain ⟨hc⟩ := IsIPCOfShape.nonempty_isColimit fun i ↦ (pres i).isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
⊢ IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι)
have refine : ∀ (X : C),
  strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X →
    ∀ (Y : Functor.{u_1, v, u_1, u} (Discrete ι) C) (h : ∀ (j : Discrete ι), P.ind (Y.obj j)), P.ind (limit Y)
Tactic: refine .mk' fun X ⟨Y, h⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
⊢ P.ind (limit Y)
have this : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
Tactic: have : HasProductsOfShape (Shrink.{w} ι) C :=
    hasLimitsOfShape_of_equivalence (Discrete.equivalence e)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
⊢ P.ind (limit Y)
have this₁ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
Tactic: have : IsIPCOfShape.{w} (Shrink.{w} ι) C := .of_equiv e
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this_1 : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
this : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
⊢ P.ind (limit Y)
have this₁ : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete (Shrink.{w, u_1} ι))
Tactic: have : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w} ι)) :=
    .of_equivalence (Discrete.equivalence e)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this_1 : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
this_2 : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅
  piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i } :=
  Iso.trans (Y := piObj.{u_1, v, u} fun (j : ι) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (Iso.symm (Pi.reindex e.symm fun (j : ι) ↦ Y.obj { as := j }))
⊢ P.ind (limit Y)
have rw : P.ind (piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i })
Tactic: rw [(ind.{w} P).prop_iff_of_iso iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderSubobjects
i : C
⊢ (MorphismProperty.ofObjectProperty P P).kernels i ≤ P i
have this : ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (k : KernelFork f) (hk : IsLimit k) (hf : MorphismProperty.ofObjectProperty P P f), P k.pt
Tactic: ⟨_, k, hk, hf⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
⊢ CreatesLimit (parallelPair f 0) P.ι
have c : Cone (parallelPair f 0 ⋙ P.ι)
Tactic: fapply createsLimitFullSubcategoryInclusion'
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
c : Cone (parallelPair f 0 ⋙ P.ι)
⊢ CreatesLimit (parallelPair f 0) P.ι
have hc : IsLimit
  ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
    (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) sorry))
Tactic: fapply createsLimitFullSubcategoryInclusion'
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
c : Cone (parallelPair f 0 ⋙ P.ι)
hc :
  IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
      (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) ⋯))
⊢ CreatesLimit (parallelPair f 0) P.ι
have h : P
  ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
      (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) sorry)).pt
Tactic: fapply createsLimitFullSubcategoryInclusion'
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) P.ι
have have : ∀ (this : CreatesLimit (parallelPair f 0) P.ι), PreservesLimit (parallelPair f 0) P.ι
Tactic: have := P.createsKernels f
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this : CreatesLimit (parallelPair f 0) P.ι
⊢ PreservesLimit (parallelPair f 0) P.ι
have this₁ : HasLimit (parallelPair f 0 ⋙ P.ι)
Tactic: have := P.hasLimit_parallelPair_comp_ι f
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderQuotients
i : C
⊢ (MorphismProperty.ofObjectProperty P P).cokernels i ≤ P i
have this : ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (k : CokernelCofork f) (hk : IsColimit k) (hf : MorphismProperty.ofObjectProperty P P f),
  P k.pt
Tactic: ⟨_, k, hk, hf⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
⊢ CreatesColimit (parallelPair f 0) P.ι
have c : Cocone (parallelPair f 0 ⋙ P.ι)
Tactic: fapply createsColimitFullSubcategoryInclusion'
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
c : Cocone (parallelPair f 0 ⋙ P.ι)
⊢ CreatesColimit (parallelPair f 0) P.ι
have hc : IsColimit
  ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
    (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) sorry))
Tactic: fapply createsColimitFullSubcategoryInclusion'
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
c : Cocone (parallelPair f 0 ⋙ P.ι)
hc :
  IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
      (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) ⋯))
⊢ CreatesColimit (parallelPair f 0) P.ι
have h : P
  ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
      (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) sorry)).pt
Tactic: fapply createsColimitFullSubcategoryInclusion'
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasCokernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) P.ι
have have : ∀ (this : CreatesColimit (parallelPair f 0) P.ι), PreservesColimit (parallelPair f 0) P.ι
Tactic: have := P.createsCokernels f
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Kernels (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasCokernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
this : CreatesColimit (parallelPair f 0) P.ι
⊢ PreservesColimit (parallelPair f 0) P.ι
have this₁ : HasColimit (parallelPair f 0 ⋙ P.ι)
Tactic: have := P.hasColimit_parallelPair_comp_ι f
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X : C
hX : limitsClosure.{t, v', u', v, u} P J X
⊢ Q X
have of_mem : ∀ (X : C) (hX : P X), Q X
Tactic: induction hX with
  | of_mem X hX => exact h _ hX
  | of_isoClosure e hX hX' => exact Q.prop_of_iso e hX'
  | of_limitPresentation pres h h' => exact Q.prop_of_isLimit pres.isLimit h'
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X : C
hX : limitsClosure.{t, v', u', v, u} P J X
of_mem : ∀ (X : C) (hX : P X), Q X
⊢ Q X
have of_isoClosure : ∀ {X Y : C} (e : X ≅ Y) (hX : limitsClosure.{t, v', u', v, u} P J X) (hX' : Q X), Q Y
Tactic: induction hX with
  | of_mem X hX => exact h _ hX
  | of_isoClosure e hX hX' => exact Q.prop_of_iso e hX'
  | of_limitPresentation pres h h' => exact Q.prop_of_isLimit pres.isLimit h'
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X : C
hX : limitsClosure.{t, v', u', v, u} P J X
of_mem : ∀ (X : C) (hX : P X), Q X
of_isoClosure : ∀ {X Y : C} (e : X ≅ Y) (hX : limitsClosure.{t, v', u', v, u} P J X) (hX' : Q X), Q Y
⊢ Q X
have of_limitPresentation : ∀ {X : C} {a : α} (pres : LimitPresentation.{v', u', v, u} (J a) X)
  (h : ∀ (j : J a), limitsClosure.{t, v', u', v, u} P J (pres.diag.obj j)) (h' : ∀ (j : J a), Q (pres.diag.obj j)), Q X
Tactic: induction hX with
  | of_mem X hX => exact h _ hX
  | of_isoClosure e hX hX' => exact Q.prop_of_iso e hX'
  | of_limitPresentation pres h h' => exact Q.prop_of_isLimit pres.isLimit h'
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ limitsClosure.{t, v', u', v, u} P.isoClosure J = limitsClosure.{t, v', u', v, u} P J
have refine : P.isoClosure ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: refine le_antisymm (limitsClosure_le ?_)
    (limitsClosure_monotone _ P.le_isoClosure)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure ≤ limitsClosure.{t, v', u', v, u} P J
have rw : P ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ P ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} P (J a) ≤ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)
have simp : P ≤ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a) ∧
  ∀ (i : α), strictLimitsOfShape.{v', u', v, u} P (J i) ≤ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
hb : IsMin b
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
have isMin : ∀ (hb : IsMin.{w'} (α := β) ⊥),
  strictLimitsClosureIter.{w', t, v', u', v, u} P J (β := β) ⊥ ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: obtain rfl := hb.eq_bot
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
hb : ¬IsMax b
hb' : strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b) ≤ limitsClosure.{t, v', u', v, u} P J
have succ : transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) b P ≤
    limitsClosure.{t, v', u', v, u} P J ∧
  ∀ (i : α),
    strictLimitsOfShape.{v', u', v, u}
        (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) b P)
        (J i) ≤
      limitsClosure.{t, v', u', v, u} P J
Tactic: rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep, sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
hb : Order.IsSuccLimit b
hb' : ∀ b_1 < b, strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1 ≤ limitsClosure.{t, v', u', v, u} P J
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
have isSuccLimit : ∀ (a : β) (b : a < b),
  transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) a P ≤
    limitsClosure.{t, v', u', v, u} P J
Tactic: simp only [transfiniteIterate_limit _ _ _ hb,
      iSup_le_iff, Subtype.forall, Set.mem_Iio]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
have isMin : ∀ (b : β) (hb : IsMin b), strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: induction b using SuccOrder.limitRecOn with
  | isMin b hb =>
    obtain rfl := hb.eq_bot
    simp
  | succ b hb hb' =>
    rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep, sup_le_iff, iSup_le_iff]
    exact ⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
      (limitsOfShape_monotone _ hb')).trans (limitsOfShape_le _ _)⟩
  | isSuccLimit b hb hb' =>
    simp only [transfiniteIterate_limit _ _ _ hb,
      iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro c hc
    exact hb' _ hc
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
isMin :
  ∀ (b : β) (hb : IsMin b), strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
have succ : ∀ (b : β) (hb : ¬IsMax b)
  (hb' : strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J),
  strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b) ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: induction b using SuccOrder.limitRecOn with
  | isMin b hb =>
    obtain rfl := hb.eq_bot
    simp
  | succ b hb hb' =>
    rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep, sup_le_iff, iSup_le_iff]
    exact ⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
      (limitsOfShape_monotone _ hb')).trans (limitsOfShape_le _ _)⟩
  | isSuccLimit b hb hb' =>
    simp only [transfiniteIterate_limit _ _ _ hb,
      iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro c hc
    exact hb' _ hc
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
isMin :
  ∀ (b : β) (hb : IsMin b), strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
succ :
  ∀ (b : β) (hb : ¬IsMax b)
    (hb' : strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J),
    strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b) ≤ limitsClosure.{t, v', u', v, u} P J
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
have isSuccLimit : ∀ (b : β) (hb : Order.IsSuccLimit b)
  (hb' : ∀ b_1 < b, strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1 ≤ limitsClosure.{t, v', u', v, u} P J),
  strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: induction b using SuccOrder.limitRecOn with
  | isMin b hb =>
    obtain rfl := hb.eq_bot
    simp
  | succ b hb hb' =>
    rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep, sup_le_iff, iSup_le_iff]
    exact ⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
      (limitsOfShape_monotone _ hb')).trans (limitsOfShape_le _ _)⟩
  | isSuccLimit b hb hb' =>
    simp only [transfiniteIterate_limit _ _ _ hb,
      iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro c hc
    exact hb' _ hc
Cleared hypotheses: b