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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b,
    ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
      ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1)
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
isSuccLimit :
  ObjectProperty.Small.{w, v, u} (C := C)
    (⨆ (x : (↑(Set.Iio b) : Type w')),
      transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (↑x : β) P)
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)

Tactic:
simp only [transfiniteIterate_limit _ _ _ hb]

Premises used: transfiniteIterate_limit
-- 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b,
    ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
      ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1)
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
c : (↑(Set.Iio b) : Type w')
⊢ Small.{w, w'} (↑(Set.Iio (↑c : β)) : Type w')

Tactic:
have := H c.2.le
-- 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b,
    ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
      ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1)
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
c : (↑(Set.Iio b) : Type w')
this : Small.{w, w'} (↑(Set.Iio (↑c : β)) : Type w')
⊢ ObjectProperty.Small.{w, v, u}
    (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (↑c : β) P)

Tactic:
hb' c.1 c.2

Premises used: Subtype.val, Subtype.property
-- 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b,
    ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
      ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1)
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
c : (↑(Set.Iio b) : Type w')
this : Small.{w, w'} (↑(Set.Iio (↑c : β)) : Type w')
⊢ ObjectProperty.Small.{w, v, u}
    (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (↑c : β) P)

Tactic:
exact hb' c.1 c.2

Premises used: Subtype.val, Subtype.property
-- 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b,
    ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
      ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1)
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
⊢ ∀ (c : (↑(Set.Iio b) : Type w')),
    ObjectProperty.Small.{w, v, u}
      (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (↑c : β)
        P)

Tactic:
have (c : Set.Iio b) : ObjectProperty.Small.{w}
      (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c.1 P) := by
      have := H c.2.le
      exact hb' c.1 c.2
-- 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b,
    ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
      ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1)
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
this :
  ∀ (c : (↑(Set.Iio b) : Type w')),
    ObjectProperty.Small.{w, v, u}
      (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (↑c : β)
        P)
⊢ ObjectProperty.Small.{w, v, u} (C := C)
    (⨆ (x : (↑(Set.Iio b) : Type w')),
      transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (↑x : β) P)

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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
inst_6 : ObjectProperty.Small.{w, v, u} P
inst_7 : LocallySmall.{w, v, u} C
inst_8 : Small.{w, t} α
inst_9 : ∀ (a : α), Small.{w, u'} (J a)
inst_10 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
b : β
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
isMin :
  ∀ (b : β) (hb : IsMin b) [hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')],
    ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
succ :
  ∀ (b : β) (hb : ¬IsMax b)
    (hb' :
      ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')],
        ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b))
    [hb₀ : Small.{w, w'} (↑(Set.Iio (Order.succ b)) : Type w')],
    ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b))
isSuccLimit :
  ∀ (b : β) (hb : Order.IsSuccLimit b)
    (hb' :
      ∀ b_1 < b,
        ∀ [hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')],
          ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b_1))
    [hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')],
    ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)

Tactic:
induction b using SuccOrder.limitRecOn generalizing hb₀ with
  | isMin b hb =>
    obtain rfl := hb.eq_bot
    simp only [transfiniteIterate_bot]
    infer_instance
  | succ b hb hb' =>
    have := H (Order.le_succ b)
    rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep]
    infer_instance
  | isSuccLimit b hb hb' =>
    simp only [transfiniteIterate_limit _ _ _ hb]
    have (c : Set.Iio b) : ObjectProperty.Small.{w}
      (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c.1 P) := by
      have := H c.2.le
      exact hb' c.1 c.2
    infer_instance

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.strictLimitsClosureIter, transfiniteIterate_bot, 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) κ
⊢ κ.IsRegular

Tactic:
have hκ : κ.IsRegular := Fact.out
-- 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
⊢ ∀ (a : α), Small.{w, u'} (J a)

Tactic:
have (a : α) := (h a).small
-- 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)
⊢ strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) J =
    strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord

Tactic:
le_antisymm (fun X hX ↦ ?_) (le_strictLimitsClosureStep _ _)

Premises used: CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, 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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
refine :
  ∀ (X : C)
    (hX : strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) J X),
    strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X
⊢ strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) J =
    strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord

Tactic:
refine le_antisymm (fun X hX ↦ ?_) (le_strictLimitsClosureStep _ _)

Premises used: CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, 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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
X : C
hX : strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) J X
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X ∨
    ∃ (a : α), strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) (J a) X

Tactic:
simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff] at hX

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)
X : C
hX :
  strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X ∨
    ∃ (a : α), strictLimitsOfShape.{v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) (J a) X
inl :
  ∀ (hX : strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X),
    strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X
inr :
  ∀ (a : α) (F : Functor.{v', v, u', u} (J a) C) [inst_3 : HasLimit F]
    (hF : ∀ (j : J a), strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (F.obj j)),
    strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X

Tactic:
obtain (hX | ⟨a, F, hF⟩) := hX
-- 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)
X : C
hX : strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X

Tactic:
hX
-- 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)
X : C
hX : strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X

Tactic:
exact hX
-- 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
hF : ∀ (j : J a), strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (F.obj j)
⊢ ∀ (j : J a),
    ∃ a_1 < κ.ord,
      transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) a_1 P
        (F.obj j)

Tactic:
simp only [strictLimitsClosureIter, transfiniteIterate_limit _ _ _
      (Cardinal.isSuccLimit_ord hκ.aleph0_le), prop_iSup_iff,
      Subtype.exists, Set.mem_Iio, exists_prop] at hF

Premises used: Set.mem_Iio, Cardinal.isSuccLimit_ord, Cardinal.IsRegular.aleph0_le, Subtype.exists, CategoryTheory.ObjectProperty.strictLimitsClosureIter, exists_prop, transfiniteIterate_limit, 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
hF :
  ∀ (j : J a),
    ∃ a_1 < κ.ord,
      transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) a_1 P
        (F.obj j)
inr :
  ∀ (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)),
    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:
choose o ho ho' using hF
-- 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}) (_ : m < κ.ord), ∀ (j : J a), o j ≤ m

Tactic:
⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
        Ordinal.iSup_lt_of_lt_cof ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩

Premises used: Ordinal.iSup_lt_of_lt_cof, iSup, Exists.intro, Equiv.symm, equivShrink, DFunLike.coe
-- 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)
refine_1 : Cardinal.mk (Shrink.{w, u'} (J a)) < κ.ord.cof
refine_2 :
  ∀ (j : J a),
    o j ≤ ⨆ (j : Shrink.{w, u'} (J a)), o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j)
⊢ ∃ (m : Ordinal.{w}) (_ : m < κ.ord), ∀ (j : J a), o j ≤ m

Tactic:
refine ⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
        Ordinal.iSup_lt_of_lt_cof ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩
-- 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)
refine_1 : HasCardinalLT.{w, u'} (J a) κ
⊢ Cardinal.mk (Shrink.{w, u'} (J a)) < κ.ord.cof

Tactic:
rw [hκ.cof_ord, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
          ← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]

Premises used: Cardinal.IsRegular.cof_ord, hasCardinalLT_iff_cardinal_mk_lt
-- 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)
⊢ HasCardinalLT.{w, u'} (J a) κ

Tactic:
h a
-- 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)
⊢ HasCardinalLT.{w, u'} (J a) κ

Tactic:
exact h a
-- 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)
j : J a
refine_2 :
  ∀ (j : Shrink.{w, u'} (J a)),
    o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j) ≤
      ⨆ (j : Shrink.{w, u'} (J a)), o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j)
⊢ o j ≤ ⨆ (j : Shrink.{w, u'} (J a)), o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j)

Tactic:
obtain ⟨j, rfl⟩ := (equivShrink.{w} (J a)).symm.surjective j

Premises used: 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) κ
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)
j : Shrink.{w, u'} (J a)
⊢ o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j) ≤
    ⨆ (j : Shrink.{w, u'} (J a)), o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j)

Tactic:
le_ciSup Ordinal.bddAbove_of_small _

Premises used: Ordinal.bddAbove_of_small, le_ciSup
-- 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)
j : Shrink.{w, u'} (J a)
⊢ o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j) ≤
    ⨆ (j : Shrink.{w, u'} (J a)), o ((Equiv.symm (equivShrink (J a)) : (a_1 : Shrink.{w, u'} (J a)) → J a) j)

Tactic:
exact le_ciSup Ordinal.bddAbove_of_small _

Premises used: Ordinal.bddAbove_of_small, le_ciSup