awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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')
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
have H : ∀ {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)
-- 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 β
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')
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
have 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 (β := β) ⊥)
Tactic: obtain rfl := hb.eq_bot
Cleared hypotheses: b, hb, hb₀
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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')
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b))
have this : Small.{w, w'} (↑(Set.Iio b) : Type w')
Tactic: have := H (Order.le_succ 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 β
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} (strictLimitsClosureIter.{w', t, v', u', v, u} P J (Order.succ b))
have 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))
Tactic: rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep]
-- 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 β
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')
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
have 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)
Tactic: simp only [transfiniteIterate_limit _ _ _ hb]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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)
have this : Small.{w, w'} (↑(Set.Iio (↑c : β)) : Type w')
Tactic: have := H c.2.le
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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')
⊢ 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)
have 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)
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
-- 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 β
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')
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
have 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)
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
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 β
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)
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
have 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))
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
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 β
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))
⊢ ObjectProperty.Small.{w, v, u} (strictLimitsClosureIter.{w', t, v', u', v, u} P J b)
have 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)
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
Cleared hypotheses: b, hb₀
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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) κ
⊢ 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
have hκ : κ.IsRegular
Tactic: have hκ : κ.IsRegular := Fact.out
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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
⊢ 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
have this : ∀ (a : α), Small.{w, u'} (J a)
Tactic: have (a : α) := (h a).small
-- 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)
κ : 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
have 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
Tactic: refine le_antisymm (fun X hX ↦ ?_) (le_strictLimitsClosureStep _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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
have 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
Tactic: simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff] at hX
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)
κ : 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
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X
have 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
Tactic: obtain (hX | ⟨a, F, hF⟩) := hX
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)
κ : 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
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord X
have 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)
Tactic: obtain (hX | ⟨a, F, hF⟩) := hX
Cleared hypotheses: X, hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (hypothesis)
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)
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)
have 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)
Tactic: simp only [strictLimitsClosureIter, transfiniteIterate_limit _ _ _
      (Cardinal.isSuccLimit_ord hκ.aleph0_le), prop_iSup_iff,
      Subtype.exists, Set.mem_Iio, exists_prop] at hF
Cleared hypotheses: hF
-- 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)
κ : 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)
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)
have 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)
Tactic: choose o ho ho' using hF
Cleared hypotheses: hF
-- 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)
κ : 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
have refine_1 : Cardinal.mk (Shrink.{w, u'} (J a)) < κ.ord.cof
Tactic: refine ⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
        Ordinal.iSup_lt_of_lt_cof ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩
-- 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)
κ : 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
⊢ ∃ (m : Ordinal.{w}) (_ : m < κ.ord), ∀ (j : J a), o j ≤ m
have 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)
Tactic: refine ⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
        Ordinal.iSup_lt_of_lt_cof ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩
-- 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)
κ : 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)
⊢ Cardinal.mk (Shrink.{w, u'} (J a)) < κ.ord.cof
have refine_1 : HasCardinalLT.{w, u'} (J a) κ
Tactic: rw [hκ.cof_ord, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
          ← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]