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)
⊢ limitsClosure.{t, v', u', v, u} P.isoClosure J = limitsClosure.{t, v', u', v, u} P J

Tactic:
le_antisymm (limitsClosure_le ?_)
    (limitsClosure_monotone _ P.le_isoClosure)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.limitsClosure_le, le_antisymm, 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)
refine : P.isoClosure ≤ limitsClosure.{t, v', u', v, u} P J
⊢ limitsClosure.{t, v', u', v, u} P.isoClosure J = limitsClosure.{t, v', u', v, u} P J

Tactic:
refine le_antisymm (limitsClosure_le ?_)
    (limitsClosure_monotone _ P.le_isoClosure)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.limitsClosure_le, le_antisymm, 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)
rw : P ≤ limitsClosure.{t, v', u', v, u} P J
⊢ P.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)
⊢ P ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
le_limitsClosure P J

Premises used: CategoryTheory.ObjectProperty.le_limitsClosure
-- 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)
⊢ P ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
exact le_limitsClosure P J

Premises used: CategoryTheory.ObjectProperty.le_limitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J_1 : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J_1 a)
J : Type u_1
inst_2 : Category.{v_1, u_1} J
⊢ IsClosedUnderLimitsOfShape.{v_1, u_1, v, u} (limitClosure.{v, u, v_1, u_1} P J) J

Tactic:
P.instIsClosedUnderLimitsOfShapeLimitsClosure _ ()

Premises used: Unit.unit, CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeLimitsClosure
-- 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)
⊢ P ≤ strictLimitsClosureStep.{t, v', u', v, u} P J

Tactic:
le_sup_left

Premises used: le_sup_left, CategoryTheory.ObjectProperty.strictLimitsClosureStep
-- 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)
inst_2 : P.Nonempty
⊢ (strictLimitsClosureStep.{t, v', u', v, u} P J).Nonempty

Tactic:
.mono (P.le_strictLimitsClosureStep J)

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep
-- 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)
Q : ObjectProperty.{v, u} C
h : P ≤ Q
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)
⊢ P ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} P (J a) ≤ Q ⊔ ⨆ (a : α), strictLimitsOfShape.{v', u', v, u} Q (J a)

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_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)
Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ 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:
⟨h.trans le_sup_left, fun a ↦
    (strictLimitsOfShape_monotone (J a) h).trans <|
      le_iSup (fun a ↦ Q.strictLimitsOfShape (J a)) a |>.trans le_sup_right⟩

Premises used: le_sup_left, le_iSup, le_sup_right, CategoryTheory.ObjectProperty.strictLimitsOfShape_monotone, And.intro, CategoryTheory.ObjectProperty.strictLimitsOfShape, LE.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)
Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ 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:
exact ⟨h.trans le_sup_left, fun a ↦
    (strictLimitsOfShape_monotone (J a) h).trans <|
      le_iSup (fun a ↦ Q.strictLimitsOfShape (J a)) 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
⊢ P ≤ strictLimitsClosureIter.{w', t, v', u', v, u} P J b

Tactic:
le_of_eq_of_le (transfiniteIterate_bot _ _).symm
    (monotone_transfiniteIterate _ _ (fun _ ↦ le_strictLimitsClosureStep _ _) bot_le)

Premises used: monotone_transfiniteIterate, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, transfiniteIterate_bot, le_of_eq_of_le, Eq.symm, bot_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 β
b : β
inst_6 : P.Nonempty
⊢ (strictLimitsClosureIter.{w', t, v', u', v, u} P J b).Nonempty

Tactic:
.mono (P.le_strictLimitsClosureIter J b)

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, 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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
b : β
hb : IsMin b
isMin :
  ∀ (hb : IsMin.{w'} (α := β) ⊥),
    strictLimitsClosureIter.{w', t, v', u', v, u} P J (β := β) ⊥ ≤ 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:
obtain rfl := hb.eq_bot

Premises used: IsMin.eq_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)
β : Type w'
inst_2 : LinearOrder β
inst_3 : OrderBot β
inst_4 : SuccOrder β
inst_5 : WellFoundedLT β
hb : IsMin.{w'} (α := β) ⊥
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J (β := β) ⊥ ≤ limitsClosure.{t, v', u', v, u} P J

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)
β : 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
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
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b) ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep, sup_le_iff, iSup_le_iff]

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.strictLimitsClosureIter, transfiniteIterate_succ, sup_le_iff, iSup_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)
β : 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
⊢ 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:
⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
      (limitsOfShape_monotone _ hb')).trans (limitsOfShape_le _ _)⟩

Premises used: CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape, CategoryTheory.ObjectProperty.strictLimitsClosureIter, CategoryTheory.ObjectProperty.limitsClosure, And.intro, CategoryTheory.ObjectProperty.limitsOfShape_monotone, LE.le.trans, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_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 β
b : β
hb : ¬IsMax b
hb' : strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J
⊢ 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:
exact ⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
      (limitsOfShape_monotone _ hb')).trans (limitsOfShape_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 β
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
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
⊢ strictLimitsClosureIter.{w', t, v', u', v, u} P J b ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
simp only [transfiniteIterate_limit _ _ _ hb,
      iSup_le_iff, Subtype.forall, Set.mem_Iio]

Premises used: Set.mem_Iio, Subtype.forall, iSup_le_iff, 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 β
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
c : β
hc : c < b
⊢ transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) c P ≤
    limitsClosure.{t, v', u', v, u} P J

Tactic:
hb' _ hc
-- 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 β
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
c : β
hc : c < b
⊢ transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) c P ≤
    limitsClosure.{t, v', u', v, u} P J

Tactic:
exact hb' _ hc
-- 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 β
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
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
⊢ 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

Premises used: Set.mem_Iio, CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.strictLimitsClosureIter, Subtype.forall, sup_le_iff, iSup_le_iff, 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)
β : 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_1 : β
hb₀ : Small.{w, w'} (↑(Set.Iio b_1) : Type w')
b c : β
hbc : b ≤ c
inst_11 : Small.{w, w'} (↑(Set.Iio c) : Type w')
x x_1 : (↑(Set.Iio b) : Type w')
h :
  Eq.{w' + 1} (α := { x : β // x ∈ Set.Iio c })
    ((fun (x : (↑(Set.Iio b) : Type w')) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.Iio c) (↑x : β) ⋯ : { x : β // x ∈ Set.Iio c }))
      x)
    ((fun (x : (↑(Set.Iio b) : Type w')) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.Iio c) (↑x : β) ⋯ : { x : β // x ∈ Set.Iio c }))
      x_1)
⊢ x = x_1

Tactic:
aesop
-- 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')
⊢ ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')

Tactic:
have H {b c : β} (hbc : b ≤ c) [Small.{w} (Set.Iio c)] : Small.{w} (Set.Iio b) :=
    small_of_injective (f := fun x ↦ (⟨x.1, lt_of_lt_of_le x.2 hbc⟩ : Set.Iio c))
      (fun _ _ _ ↦ by aesop)
-- 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 : IsMin b
hb₀ : Small.{w, w'} (↑(Set.Iio b) : Type w')
isMin :
  ∀ (hb : IsMin.{w'} (α := β) ⊥) [hb₀ : Small.{w, w'} (↑(Set.Iio ⊥) : Type w')],
    ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J (β := β) ⊥)
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)

Tactic:
obtain rfl := hb.eq_bot

Premises used: IsMin.eq_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)
β : 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')
hb : IsMin.{w'} (α := β) ⊥
hb₀ : Small.{w, w'} (↑(Set.Iio ⊥) : Type w')
isMin : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J (β := β) ⊥)

Tactic:
simp only [transfiniteIterate_bot]

Premises used: transfiniteIterate_bot
-- 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')
hb : IsMin.{w'} (α := β) ⊥
hb₀ : Small.{w, w'} (↑(Set.Iio ⊥) : Type w')
⊢ ObjectProperty.Small.{w, v, u} 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)
H : ∀ {b c : β} (hbc : b ≤ c) [Small.{w, w'} (↑(Set.Iio c) : Type w')], Small.{w, w'} (↑(Set.Iio b) : Type w')
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')
⊢ Small.{w, w'} (↑(Set.Iio b) : Type w')

Tactic:
have := H (Order.le_succ b)
-- 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 : ¬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')
this : Small.{w, w'} (↑(Set.Iio b) : Type w')
succ :
  ObjectProperty.Small.{w, v, u}
    (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) b P ⊔
      ⨆ (a : α),
        strictLimitsOfShape.{v', u', v, u}
          (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) b P)
          (J a))
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b))

Tactic:
rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep]

Premises used: CategoryTheory.ObjectProperty.strictLimitsClosureStep, CategoryTheory.ObjectProperty.strictLimitsClosureIter, 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)
β : 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 : ¬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')
this : Small.{w, w'} (↑(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) b P ⊔
      ⨆ (a : α),
        strictLimitsOfShape.{v', u', v, u}
          (transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) b P)
          (J a))

Tactic:
infer_instance