awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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
⊢ IsClosedUnderColimitsOfShape.{v_1, u_1, v, u} (colimitClosure.{v, u, v_1, u_1} P J) J

Tactic:
P.instIsClosedUnderColimitsOfShapeColimitsClosure _ ()

Premises used: Unit.unit, CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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)
⊢ colimitsClosure.{t, v', u', v, u} P J =
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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_1 :
  colimitsClosure.{t, v', u', v, u} P J ≤
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
refine_2 :
  ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤
    colimitsClosure.{t, v', u', v, u} P J
⊢ colimitsClosure.{t, v', u', v, u} P J =
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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_1 : P ≤ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
⊢ colimitsClosure.{t, v', u', v, u} P J ≤
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)

Tactic:
apply colimitsClosure_le

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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_1 : P.op ≤ limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ
⊢ P ≤ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)

Tactic:
rw [← op_monotone_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.op_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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.op ≤ limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ

Tactic:
apply le_limitsClosure

Premises used: CategoryTheory.ObjectProperty.le_limitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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_2 : (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤ (colimitsClosure.{t, v', u', v, u} P J).op
⊢ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤
    colimitsClosure.{t, v', u', v, u} P J

Tactic:
rw [← op_monotone_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.op_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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_2 : P.op ≤ (colimitsClosure.{t, v', u', v, u} P J).op
⊢ (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤ (colimitsClosure.{t, v', u', v, u} P J).op

Tactic:
apply limitsClosure_le

Premises used: CategoryTheory.ObjectProperty.limitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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_2 : P ≤ colimitsClosure.{t, v', u', v, u} P J
⊢ P.op ≤ (colimitsClosure.{t, v', u', v, u} P J).op

Tactic:
rw [op_monotone_iff]

Premises used: CategoryTheory.ObjectProperty.op_monotone_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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 ≤ colimitsClosure.{t, v', u', v, u} P J

Tactic:
apply le_colimitsClosure

Premises used: CategoryTheory.ObjectProperty.le_colimitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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)
rw :
  ObjectProperty.EssentiallySmall.{w, v, u}
    (ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ))
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (colimitsClosure.{t, v', u', v, u} P J)

Tactic:
rw [colimitsClosure_eq_unop_limitsClosure]

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_eq_unop_limitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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)
⊢ ∀ (a : α), Small.{w, u'} (J a)ᵒᵖ

Tactic:
have (a : α) : Small.{w} (J a)ᵒᵖ := Opposite.small
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
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)
this : ∀ (a : α), Small.{w, u'} (J a)ᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u}
    (ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ strictColimitsOfShape.{v', u', v_1, u_1} Q J (colimit F)

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

Premises used: CategoryTheory.ObjectProperty.strictColimitsOfShape.colimit, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ strictColimitsOfShape.{v', u', v_1, u_1} Q J (colimit F)

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

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : HasColimit F
h : ∀ (j : J), ⊥ (F.obj j)
⊢ ⊥ (colimit F)

Tactic:
h (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : HasColimit F
h : ∀ (j : J), ⊥ (F.obj j)
⊢ ⊥ (colimit F)

Tactic:
exact h (Classical.arbitrary J)

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

Tactic:
exact p.ι.app j

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{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)
      (CostructuredArrow.left.{v_1, v_1, u_1, u_1} (D := C) (S := P.ι) (T := X)
        (CostructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toColimitPresentation (P := P).diag.obj X_1) ⋯)
          (p.toColimitPresentation (P := P).ι.app X_1))))
    (FullSubcategory.obj (P := P)
      (CostructuredArrow.left.{v_1, v_1, u_1, u_1} (D := C) (S := P.ι) (T := X)
        (CostructuredArrow.mk (Y := FullSubcategory.mk (P := P) (p.toColimitPresentation (P := P).diag.obj Y) ⋯)
          (p.toColimitPresentation (P := P).ι.app Y))))

Tactic:
exact p.diag.map f

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ ObjectProperty.colimitsOfShape.{v', u', v_1, u_1} P J X

Tactic:
⟨h⟩

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape, Nonempty.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ colimitsOfShape.{v', u', v_1, u_1} P J (colimit F)

Tactic:
⟨.colimit F hF⟩

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape, CategoryTheory.ObjectProperty.ColimitOfShape.colimit, Nonempty.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ colimitsOfShape.{v', u', v_1, u_1} P J (colimit F)

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

Tactic:
rw [eq_bot_iff]

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

Tactic:
h (Classical.arbitrary J)

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

Tactic:
exact h (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J Y

Tactic:
⟨h.ofIso e⟩

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.ofIso, CategoryTheory.ObjectProperty.colimitsOfShape, Nonempty.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J Y

Tactic:
exact ⟨h.ofIso e⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure = colimitsOfShape.{v', u', v_1, u_1} P J

Tactic:
le_antisymm ?_ ?_

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

Tactic:
refine le_antisymm ?_ ?_

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

Tactic:
rw [isoClosure_le_iff]

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

Tactic:
apply strictColimitsOfShape_le_colimitsOfShape

Premises used: CategoryTheory.ObjectProperty.strictColimitsOfShape_le_colimitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X), (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ≤ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X

Tactic:
⟨h⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ HasColimit h.toColimitPresentation (P := P).diag

Tactic:
have := h.hasColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X
this : HasColimit h.toColimitPresentation (P := P).diag
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X

Tactic:
⟨colimit h.diag, strictColimitsOfShape.colimit h.diag h.prop_diag_obj,
      ⟨h.isColimit.coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.Limits.colimit, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.ObjectProperty.strictColimitsOfShape.colimit, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X
this : HasColimit h.toColimitPresentation (P := P).diag
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X

Tactic:
exact ⟨colimit h.diag, strictColimitsOfShape.colimit h.diag h.prop_diag_obj,
      ⟨h.isColimit.coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{v', u', v_1, u_1} P J X), colimitsOfShape.{v', u', v_1, u_1} Q J X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ≤ colimitsOfShape.{v', u', v_1, u_1} Q J X

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

Tactic:
⟨h.ofLE hPQ⟩

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

Tactic:
exact ⟨h.ofLE hPQ⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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
⊢ colimitsOfShape.{v', u', v_1, u_1} P.isoClosure J = colimitsOfShape.{v', u', v_1, u_1} P J

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

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_antisymm, CategoryTheory.ObjectProperty.colimitsOfShape_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : colimitsOfShape.{v', u', v_1, u_1} P.isoClosure J ≤ colimitsOfShape.{v', u', v_1, u_1} P J
⊢ colimitsOfShape.{v', u', v_1, u_1} P.isoClosure J = colimitsOfShape.{v', u', v_1, u_1} P J

Tactic:
refine le_antisymm ?_ (colimitsOfShape_monotone _ (P.le_isoClosure))

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

Tactic:
⟨h⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{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.toColimitPresentation (P := P.isoClosure).diag.obj j ≅ obj j)),
    colimitsOfShape.{v', u', v_1, u_1} P J X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X

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

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{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.toColimitPresentation (P := P.isoClosure).diag.obj j ≅ obj j)
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X

Tactic:
⟨{ toColimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape, Nonempty.some, CategoryTheory.Limits.ColimitPresentation.changeDiag, Nonempty.intro, CategoryTheory.Functor.isoCopyObj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.ColimitOfShape.mk, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : ColimitOfShape.{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.toColimitPresentation (P := P.isoClosure).diag.obj j ≅ obj j)
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X

Tactic:
exact
   ⟨{ toColimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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} (strictColimitsOfShape.{v', u', v_1, u_1} P J)

Tactic:
small_of_surjective
    (f := fun (F : { F : J ⥤ P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
      (⟨_, letI := F.2; ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩)) ?_

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 (strictColimitsOfShape.{v', u', v_1, u_1} P J))
    fun (F : { F : Functor.{v', v_1, u', u_1} J P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
    Subtype.mk (p := strictColimitsOfShape.{v', u', v_1, u_1} P J) (colimit ((↑F : J ⥤ P.FullSubcategory) ⋙ P.ι)) ⋯
⊢ ObjectProperty.Small.{w, v_1, u_1} (strictColimitsOfShape.{v', u', v_1, u_1} P J)

Tactic:
refine small_of_surjective
    (f := fun (F : { F : J ⥤ P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
      (⟨_, letI := F.2; ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩)) ?_

Premises used: small_of_surjective