awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
have 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)
Tactic: obtain ⟨j, rfl⟩ := (equivShrink.{w} (J a)).symm.surjective j
Cleared hypotheses: 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)
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)
have 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)
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 _
-- 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}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord (limit F)
have inr : (fun (j : Ordinal.{w}) ↦
    transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) j P)
  (Order.succ m) (limit F)
Tactic: refine monotone_transfiniteIterate _ _
      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J) (Order.succ_le_iff.2 hm) _ ?_
-- 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}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ transfiniteIterate (fun (Q : ObjectProperty.{v, u} C) ↦ strictLimitsClosureStep.{t, v', u', v, u} Q J) (Order.succ m)
    P (limit F)
have 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)
Tactic: rw [transfiniteIterate_succ _ _ _ (by simp)]
-- 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}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ 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)
have 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)
Tactic: simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
κ : 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
have refine_1 : (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: refine le_antisymm ?_ ?_
-- 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) κ
refine_1 : (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure ≤ 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
have refine_2 : limitsClosure.{t, v', u', v, u} P J ≤ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
Tactic: refine le_antisymm ?_ ?_
-- 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) κ
⊢ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure ≤ limitsClosure.{t, v', u', v, u} P J
have refine_1 : strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord ≤ limitsClosure.{t, v', u', v, u} P J
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT.{w, u'} (J a) κ
a : α
| (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
have rw : (strictLimitsClosureStep.{t, v', u', v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord) J).isoClosure
Tactic: rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]
-- 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) κ
a : α
⊢ 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
have 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
Tactic: conv_rhs => rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]
-- 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) κ
a : α
⊢ 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
have 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
Tactic: rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
        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) κ
⊢ limitsClosure.{t, v', u', v, u} P J ≤ (strictLimitsClosureIter.{w + 1, t, v', u', v, u} P J κ.ord).isoClosure
have this : ∀ (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)⟩
-- 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) κ
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)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)
have 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)
Tactic: obtain ⟨Q, hQ, hQ₁, hQ₂⟩ := EssentiallySmall.exists_small_le.{w} P
-- 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) κ
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)
have rw : ObjectProperty.EssentiallySmall.{w, v, u} (strictLimitsClosureIter.{w + 1, t, v', u', v, u} Q J κ.ord).isoClosure
Tactic: rw [limitsClosure_isoClosure,
      ← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]
-- 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) κ
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} P J)
have this : 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
-- 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)
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
inst_4 : Small.{w, t} α
inst_5 : ∀ (a : α), Small.{w, u'} (J a)
inst_6 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)
have obtain : ∀ (κ : Cardinal.{w}) (h₁ : κ.IsRegular) (h₂ : ∀ (i : α), HasCardinalLT.{w, u'} (J i) κ),
  ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)
Tactic: obtain ⟨κ, h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall J
-- 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)
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
inst_4 : Small.{w, t} α
inst_5 : ∀ (a : α), Small.{w, u'} (J a)
inst_6 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
κ : Cardinal.{w}
h₁ : κ.IsRegular
h₂ : ∀ (i : α), HasCardinalLT.{w, u'} (J i) κ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)
have this : Fact κ.IsRegular
Tactic: have : Fact κ.IsRegular := ⟨h₁⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : Nonempty J
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (strictLimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (strictLimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : Nonempty J
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (limitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (limitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure = limitsOfShape.{v', u', v_1, u_1} P J
have refine_1 : (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ limitsOfShape.{v', u', v_1, u_1} P J
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
refine_1 : (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ limitsOfShape.{v', u', v_1, u_1} P J
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure = limitsOfShape.{v', u', v_1, u_1} P J
have refine_2 : limitsOfShape.{v', u', v_1, u_1} P J ≤ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ limitsOfShape.{v', u', v_1, u_1} P J
have refine_1 : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ limitsOfShape.{v', u', v_1, u_1} P J
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ≤ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
have refine_2 : ∀ (h : LimitOfShape.{v', u', v_1, u_1} P J X), (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
have this : HasLimit h.toLimitPresentation (P := P).diag
Tactic: have := h.hasLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
X : C
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ≤ limitsOfShape.{v', u', v_1, u_1} Q J X
have this : ∀ (h : LimitOfShape.{v', u', v_1, u_1} P J X), limitsOfShape.{v', u', v_1, u_1} Q J X
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
⊢ limitsOfShape.{v', u', v_1, u_1} P.isoClosure J = limitsOfShape.{v', u', v_1, u_1} P J
have refine : limitsOfShape.{v', u', v_1, u_1} P.isoClosure J ≤ limitsOfShape.{v', u', v_1, u_1} P J
Tactic: refine le_antisymm ?_ (limitsOfShape_monotone _ P.le_isoClosure)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
⊢ limitsOfShape.{v', u', v_1, u_1} P.isoClosure J X ≤ limitsOfShape.{v', u', v_1, u_1} P J X
have this : ∀ (h : LimitOfShape.{v', u', v_1, u_1} P.isoClosure J X), limitsOfShape.{v', u', v_1, u_1} P J X
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h : LimitOfShape.{v', u', v_1, u_1} P.isoClosure J X
⊢ limitsOfShape.{v', u', v_1, u_1} P J X
have choose : ∀ (obj : (j : J) → C) (h₁ : ∀ (j : J), P (obj j))
  (h₂ : ∀ (j : J), Nonempty.{v_1 + 1} (h.toLimitPresentation (P := P.isoClosure).diag.obj j ≅ obj j)),
  limitsOfShape.{v', u', v_1, u_1} P J X
Tactic: choose obj h₁ h₂ using h.prop_diag_obj
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : ObjectProperty.Small.{w, v_1, u_1} P
inst_5 : LocallySmall.{w, v_1, u_1} C
inst_6 : Small.{w, u'} J
inst_7 : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.Small.{w, v_1, u_1} (strictLimitsOfShape.{v', u', v_1, u_1} P J)
have refine : Function.Surjective (β := Subtype (strictLimitsOfShape.{v', u', v_1, u_1} P J))
  fun (F : { F : Functor.{v', v_1, u', u_1} J P.FullSubcategory // HasLimit (F ⋙ P.ι) }) ↦
  Subtype.mk (p := strictLimitsOfShape.{v', u', v_1, u_1} P J) (limit ((↑F : J ⥤ P.FullSubcategory) ⋙ P.ι)) sorry
Tactic: refine small_of_surjective
    (f := fun (F : { F : J ⥤ P.FullSubcategory // HasLimit (F ⋙ P.ι) }) ↦
      (⟨_, letI := F.2; ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : ObjectProperty.Small.{w, v_1, u_1} P
inst_5 : LocallySmall.{w, v_1, u_1} C
inst_6 : Small.{w, u'} J
inst_7 : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P J)
have rw : ObjectProperty.EssentiallySmall.{w, v_1, u_1} (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure
Tactic: rw [← isoClosure_strictLimitsOfShape]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
| P
have rw : P.isoClosure
Tactic: rw [← P.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ limitsOfShape.{v', u', v_1, u_1} P J ≤ P
have conv_rhs : limitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure
Tactic: conv_rhs => rw [← P.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ limitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure
have rw : (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure
Tactic: rw [← isoClosure_strictLimitsOfShape]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : Nonempty J
⊢ LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (limitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
Tactic: rw [limitsOfShape_bot]