awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
inr :
  ∀ (m : Ordinal.{w}) (hm : m < κ.ord) (hm' : ∀ (j : J a), o j ≤ m),
    strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)

Tactic:
obtain ⟨m, hm, hm'⟩ : ∃ (m : Ordinal.{w}) (hm : m < κ.ord), ∀ (j : J a), o j ≤ m := by
      refine ⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
        Ordinal.iSup_lt_of_lt_cof ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩
      · rw [hκ.cof_ord, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
          ← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]
        exact h a
      · obtain ⟨j, rfl⟩ := (equivShrink.{w} (J a)).symm.surjective j
        exact le_ciSup Ordinal.bddAbove_of_small _

Premises used: Cardinal.ord
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)

Tactic:
monotone_transfiniteIterate _ _
      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J) (Order.succ_le_iff.2 hm) _ ?_

Premises used: Iff.mpr, monotone_transfiniteIterate, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, Order.succ_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
inr :
  transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (Order.succ m)
    P (limit F)
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)

Tactic:
refine monotone_transfiniteIterate _ _
      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J) (Order.succ_le_iff.2 hm) _ ?_

Premises used: Iff.mpr, monotone_transfiniteIterate, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, Order.succ_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ ¬IsMax m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
inr :
  strictLimitsClosureStep.{t, v', u', v, u}
    (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) m P) J
    (limit F)
⊢ transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (Order.succ m)
    P (limit F)

Tactic:
rw [transfiniteIterate_succ _ _ _ (by simp)]

Premises used: transfiniteIterate_succ
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
inr :
  transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)) m P
      (limit F) ∨
    ∃ (a_1 : α),
      strictLimitsOfShape.{v', u', v, u}
        (transfiniteIterate
          (fun (Q : ObjectProperty.{v, u} C) ↦ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)) m P)
        (J a_1) (limit F)
⊢ strictLimitsClosureStep.{t, v', u', v, u}
    (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) m P) J
    (limit F)

Tactic:
simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff]

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.prop_sup_iff, CategoryTheory.ObjectProperty.prop_iSup_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)) m P
      (limit F) ∨
    ∃ (a_1 : α),
      strictLimitsOfShape.{v', u', v, u}
        (transfiniteIterate
          (fun (Q : ObjectProperty.{v, u} C) ↦ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)) m P)
        (J a_1) (limit F)

Tactic:
Or.inr ⟨a, ⟨_, fun j ↦ monotone_transfiniteIterate _ _
      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J)  (hm' j) _ (ho' j)⟩⟩

Premises used: monotone_transfiniteIterate, CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, CategoryTheory.ObjectProperty.strictLimitsOfShape.limit, Exists.intro, CategoryTheory.Functor.obj, Or.inr
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : Functor.{v', v, u', u} (J a) C
inst_3 : HasLimit F
o : (j : J a) → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' :
  ∀ (j : J a),
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (o j) P
      (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)) m P
      (limit F) ∨
    ∃ (a_1 : α),
      strictLimitsOfShape.{v', u', v, u}
        (transfiniteIterate
          (fun (Q : ObjectProperty.{v, u} C) ↦ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)) m P)
        (J a_1) (limit F)

Tactic:
exact Or.inr ⟨a, ⟨_, fun j ↦ monotone_transfiniteIterate _ _
      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J)  (hm' j) _ (ho' j)⟩⟩

Premises used: Or.inr
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
⊢ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure = limitsClosure.{t, v', u', v, u} P J

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
refine_1 : (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure ≤ limitsClosure.{t, v', u', v, u} P J
refine_2 : limitsClosure.{t, v', u', v, u} P J ≤ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
⊢ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure = limitsClosure.{t, v', u', v, u} P J

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
refine_1 : strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord ≤ limitsClosure.{t, v', u', v, u} P J
⊢ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
rw [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
P.strictLimitsClosureIter_le_limitsClosure J κ.ord

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure, Cardinal.ord
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
exact P.strictLimitsClosureIter_le_limitsClosure J κ.ord

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure, Cardinal.ord
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
a : α
rw :
  (strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) J).isoClosure
| (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure

Tactic:
rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep_strictLimitsClosureIter_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
a : α
conv_rhs :
  limitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure (J a) ≤
    (strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord)
        J).isoClosure
⊢ limitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure (J a) ≤
    (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure

Tactic:
conv_rhs => rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep_strictLimitsClosureIter_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
a : α
rw :
  (strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) (J a)).isoClosure ≤
    (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord ⊔
        ⨆ (a : α),
          strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord)
            (J a)).isoClosure
⊢ limitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure (J a) ≤
    (strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord)
        J).isoClosure

Tactic:
rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
        strictLimitsClosureStep]

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.limitsOfShape_isoClosure, CategoryTheory.ObjectProperty.isoClosure_strictLimitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
a : α
⊢ strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) (J a) ≤
    strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) (J a)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
a : α
⊢ (strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) (J a)).isoClosure ≤
    (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord ⊔
        ⨆ (a : α),
          strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord)
            (J a)).isoClosure

Tactic:
exact monotone_isoClosure ((le_trans (by rfl) (le_iSup _ a)).trans le_sup_right)

Premises used: le_iSup, le_sup_right, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans, le_trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
⊢ ∀ (a : α),
    IsClosedUnderLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
      (J a)

Tactic:
have (a : α) :
        (P.strictLimitsClosureIter J κ.ord).isoClosure.IsClosedUnderLimitsOfShape (J a) := ⟨by
      conv_rhs => rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]
      rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
        strictLimitsClosureStep]
      exact monotone_isoClosure ((le_trans (by rfl) (le_iSup _ a)).trans le_sup_right)⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
this :
  ∀ (a : α),
    IsClosedUnderLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
      (J a)
⊢ limitsClosure.{t, v', u', v, u} P J ≤ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure

Tactic:
limitsClosure_le
      ((P.le_strictLimitsClosureIter J κ.ord).trans (le_isoClosure _))

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.limitsClosure_le, Cardinal.ord, LE.le.trans, CategoryTheory.ObjectProperty.le_strictLimitsClosureIter
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
this :
  ∀ (a : α),
    IsClosedUnderLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
      (J a)
⊢ limitsClosure.{t, v', u', v, u} P J ≤ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure

Tactic:
refine limitsClosure_le
      ((P.le_strictLimitsClosureIter J κ.ord).trans (le_isoClosure _))

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.limitsClosure_le, Cardinal.ord, LE.le.trans, CategoryTheory.ObjectProperty.le_strictLimitsClosureIter
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_4 : LocallySmall.{w, v, u} C
inst_5 : Small.{w, t} α
inst_6 : ∀ (a : α), Small.{w, u'} (J a)
inst_7 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
obtain :
  ∀ (Q : ObjectProperty.{v, u} C) (hQ : ObjectProperty.Small.{w, v, u} Q) (hQ₁ : Q ≤ P) (hQ₂ : P ≤ Q.isoClosure),
    ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)

Tactic:
obtain ⟨Q, hQ, hQ₁, hQ₂⟩ := EssentiallySmall.exists_small_le.{w} P
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_4 : LocallySmall.{w, v, u} C
inst_5 : Small.{w, t} α
inst_6 : ∀ (a : α), Small.{w, u'} (J a)
inst_7 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty.{v, u} C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
rw : ObjectProperty.EssentiallySmall.{w, v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} Q J κ.ord).isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} Q.isoClosure J)

Tactic:
rw [limitsClosure_isoClosure,
      ← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]

Premises used: CategoryTheory.ObjectProperty.isoClosure_strictLimitsClosureIter_eq_limitsClosure, CategoryTheory.ObjectProperty.limitsClosure_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_4 : LocallySmall.{w, v, u} C
inst_5 : Small.{w, t} α
inst_6 : ∀ (a : α), Small.{w, u'} (J a)
inst_7 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty.{v, u} C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} Q J κ.ord).isoClosure

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_4 : LocallySmall.{w, v, u} C
inst_5 : Small.{w, t} α
inst_6 : ∀ (a : α), Small.{w, u'} (J a)
inst_7 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty.{v, u} C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} Q.isoClosure J)

Tactic:
have : ObjectProperty.EssentiallySmall.{w} (Q.isoClosure.limitsClosure J) := by
    rw [limitsClosure_isoClosure,
      ← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]
    infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_4 : LocallySmall.{w, v, u} C
inst_5 : Small.{w, t} α
inst_6 : ∀ (a : α), Small.{w, u'} (J a)
inst_7 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty.{v, u} C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
this : ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} Q.isoClosure J)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)

Tactic:
.of_le (limitsClosure_monotone J hQ₂)

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.of_le, CategoryTheory.ObjectProperty.limitsClosure_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_4 : LocallySmall.{w, v, u} C
inst_5 : Small.{w, t} α
inst_6 : ∀ (a : α), Small.{w, u'} (J a)
inst_7 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty.{v, u} C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
this : ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} Q.isoClosure J)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)

Tactic:
exact .of_le (limitsClosure_monotone J hQ₂)