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)
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)
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)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)

Tactic:
obtain ⟨κ, h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall J

Premises used: HasCardinalLT.exists_regular_cardinal_forall
-- 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 : 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) κ
⊢ Fact κ.IsRegular

Tactic:
have : Fact κ.IsRegular := ⟨h₁⟩
-- 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 : 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) κ
this : Fact κ.IsRegular
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)

Tactic:
isEssentiallySmall_limitsClosure P J κ h₂

Premises used: CategoryTheory.ObjectProperty.isEssentiallySmall_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)
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) κ
this : Fact κ.IsRegular
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (limitsClosure.{t, v', u', v, u} P J)

Tactic:
exact isEssentiallySmall_limitsClosure P J κ h₂

Premises used: CategoryTheory.ObjectProperty.isEssentiallySmall_limitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
h : P ≤ Q
F : Functor.{v', v_1, u', u_1} J C
inst_2 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ strictLimitsOfShape.{v', u', v_1, u_1} Q J (limit F)

Tactic:
⟨F, fun j ↦ h _ (hF j)⟩

Premises used: CategoryTheory.ObjectProperty.strictLimitsOfShape.limit, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
h : P ≤ Q
F : Functor.{v', v_1, u', u_1} J C
inst_2 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ strictLimitsOfShape.{v', u', v_1, u_1} Q J (limit F)

Tactic:
exact ⟨F, fun j ↦ h _ (hF j)⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (strictLimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (strictLimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
F : Functor.{v', v_1, u', u_1} J C
inst_3 : HasLimit F
h : ∀ (j : J), ⊥ (F.obj j)
⊢ ⊥ (limit F)

Tactic:
h (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
F : Functor.{v', v_1, u', u_1} J C
inst_3 : HasLimit F
h : ∀ (j : J), ⊥ (F.obj j)
⊢ ⊥ (limit F)

Tactic:
exact h (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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'
X : C
p : LimitOfShape.{v', u', v_1, u_1} P J X
j : J
⊢ X ⟶ P.ι.obj (FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj j) ⋯)

Tactic:
exact p.π.app j

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.LimitPresentation.π, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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'
X : C
p : LimitOfShape.{v', u', v_1, u_1} P J X
X_1 Y : J
f : X_1 ⟶ Y
⊢ Quiver.Hom.{v_1, u_1} (V := C)
    (FullSubcategory.obj (P := P)
      (StructuredArrow.right.{v_1, v_1, u_1, u_1} (D := C) (S := X) (T := P.ι)
        (StructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj X_1) ⋯)
          (p.toLimitPresentation (P := P).π.app X_1))))
    (FullSubcategory.obj (P := P)
      (StructuredArrow.right.{v_1, v_1, u_1, u_1} (D := C) (S := X) (T := P.ι)
        (StructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj Y) ⋯)
          (p.toLimitPresentation (P := P).π.app Y))))

Tactic:
exact p.diag.map f

Premises used: CategoryTheory.Functor.map, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.LimitPresentation.diag
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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'
X : C
p : LimitOfShape.{v', u', v_1, u_1} P J X
X_1 Y : J
f : X_1 ⟶ Y
⊢ Eq (α :=
    X ⟶
      P.ι.obj
        (StructuredArrow.right.{v_1, v_1, u_1, u_1} (D := C) (S := X) (T := P.ι)
          (StructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj Y) ⋯)
            (p.toLimitPresentation (P := P).π.app Y))))
    (CategoryStruct.comp (Y :=
      P.ι.obj
        (StructuredArrow.right.{v_1, v_1, u_1, u_1} (D := C) (S := X) (T := P.ι)
          (StructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj X_1) ⋯)
            (p.toLimitPresentation (P := P).π.app X_1))))
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj X_1) ⋯)
          (p.toLimitPresentation (P := P).π.app X_1)))
      (P.ι.map (homMk (P := P) (p.toLimitPresentation (P := P).diag.map f))))
    (StructuredArrow.hom
      (StructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toLimitPresentation (P := P).diag.obj Y) ⋯)
        (p.toLimitPresentation (P := P).π.app Y)))

Tactic:
simpa using (p.π.naturality f).symm

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.LimitPresentation.π
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
⊢ ObjectProperty.limitsOfShape.{v', u', v_1, u_1} P J X

Tactic:
⟨h⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.limitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
F : Functor.{v', v_1, u', u_1} J C
inst_2 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ limitsOfShape.{v', u', v_1, u_1} P J (limit F)

Tactic:
⟨.limit F hF⟩

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.limit, Nonempty.intro, CategoryTheory.ObjectProperty.limitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
F : Functor.{v', v_1, u', u_1} J C
inst_2 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ limitsOfShape.{v', u', v_1, u_1} P J (limit F)

Tactic:
exact ⟨.limit F hF⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (limitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (limitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
X : C
toLimitPresentation : LimitPresentation.{v', u', v_1, u_1} J X
h : ∀ (j : J), ⊥ (toLimitPresentation.diag.obj j)
⊢ ⊥ X

Tactic:
h (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
X : C
toLimitPresentation : LimitPresentation.{v', u', v_1, u_1} J X
h : ∀ (j : J), ⊥ (toLimitPresentation.diag.obj j)
⊢ ⊥ X

Tactic:
exact h (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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'
X Y : C
e : X ≅ Y
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ limitsOfShape.{v', u', v_1, u_1} P J Y

Tactic:
⟨h.ofIso e⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.LimitOfShape.ofIso, CategoryTheory.ObjectProperty.limitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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'
X Y : C
e : X ≅ Y
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ limitsOfShape.{v', u', v_1, u_1} P J Y

Tactic:
exact ⟨h.ofIso e⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
refine_2 : limitsOfShape.{v', u', v_1, u_1} P J ≤ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure = limitsOfShape.{v', u', v_1, u_1} P J

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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 ≤ 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

Tactic:
rw [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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 ≤ limitsOfShape.{v', u', v_1, u_1} P J

Tactic:
apply strictLimitsOfShape_le_limitsOfShape

Premises used: CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
refine_2 : ∀ (h : LimitOfShape.{v', u', v_1, u_1} P J X), (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ≤ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X

Tactic:
⟨h⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
⊢ HasLimit h.toLimitPresentation (P := P).diag

Tactic:
have := h.hasLimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
this : HasLimit h.toLimitPresentation (P := P).diag
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X

Tactic:
⟨limit h.diag, strictLimitsOfShape.limit h.diag h.prop_diag_obj,
      ⟨h.isLimit.conePointUniqueUpToIso (limit.isLimit _)⟩⟩

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.ObjectProperty.strictLimitsOfShape.limit, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.limit, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Limits.LimitPresentation.diag
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
this : HasLimit h.toLimitPresentation (P := P).diag
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X

Tactic:
exact ⟨limit h.diag, strictLimitsOfShape.limit h.diag h.prop_diag_obj,
      ⟨h.isLimit.conePointUniqueUpToIso (limit.isLimit _)⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
this : ∀ (h : LimitOfShape.{v', u', v_1, u_1} P J X), limitsOfShape.{v', u', v_1, u_1} Q J X
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ≤ limitsOfShape.{v', u', v_1, u_1} Q J X

Tactic:
⟨h⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ limitsOfShape.{v', u', v_1, u_1} Q J X

Tactic:
⟨h.ofLE hPQ⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.LimitOfShape.ofLE, CategoryTheory.ObjectProperty.limitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ limitsOfShape.{v', u', v_1, u_1} Q J X

Tactic:
exact ⟨h.ofLE hPQ⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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

Tactic:
le_antisymm ?_ (limitsOfShape_monotone _ P.le_isoClosure)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_antisymm, CategoryTheory.ObjectProperty.limitsOfShape_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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 : limitsOfShape.{v', u', v_1, u_1} P.isoClosure J ≤ limitsOfShape.{v', u', v_1, u_1} P J
⊢ 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)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_antisymm, CategoryTheory.ObjectProperty.limitsOfShape_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
this : ∀ (h : LimitOfShape.{v', u', v_1, u_1} P.isoClosure J X), limitsOfShape.{v', u', v_1, u_1} P J X
⊢ limitsOfShape.{v', u', v_1, u_1} P.isoClosure J X ≤ limitsOfShape.{v', u', v_1, u_1} P J X

Tactic:
⟨h⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
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
⊢ limitsOfShape.{v', u', v_1, u_1} P J X

Tactic:
choose obj h₁ h₂ using h.prop_diag_obj

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
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:
⟨{ toLimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩

Premises used: CategoryTheory.Limits.LimitPresentation.changeDiag, Nonempty.some, Nonempty.intro, CategoryTheory.Functor.isoCopyObj, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.ObjectProperty.LimitOfShape.mk, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.limitsOfShape, CategoryTheory.Limits.LimitPresentation.diag
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
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:
exact
   ⟨{ toLimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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)

Tactic:
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⟩⟩)) ?_

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
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.ι)) ⋯
⊢ ObjectProperty.Small.{w, v_1, u_1} (strictLimitsOfShape.{v', u', v_1, u_1} P J)

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⟩⟩)) ?_

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
F : Functor.{v', v_1, u', u_1} J C
inst_8 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ HasLimit (P.lift F hF ⋙ P.ι)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
F : Functor.{v', v_1, u', u_1} J C
inst_8 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ ∃ (a : { F : Functor.{v', v_1, u', u_1} J P.FullSubcategory // HasLimit (F ⋙ P.ι) }),
    (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.ι)) ⋯ :
            Subtype (strictLimitsOfShape.{v', u', v_1, u_1} P J)))
        a =
      Subtype.mk (p := strictLimitsOfShape.{v', u', v_1, u_1} P J) (limit F) ⋯

Tactic:
exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
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
rw : ObjectProperty.EssentiallySmall.{w, v_1, u_1} (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P J)

Tactic:
rw [← isoClosure_strictLimitsOfShape]

Premises used: CategoryTheory.ObjectProperty.isoClosure_strictLimitsOfShape