awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ (P.strictMap F).isoClosure = P.map F

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
refine_1 : (P.strictMap F).isoClosure ≤ P.map F
refine_2 : P.map F ≤ (P.strictMap F).isoClosure
⊢ (P.strictMap F).isoClosure = P.map F

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
refine_1 : P.strictMap F ≤ P.map F
⊢ (P.strictMap F).isoClosure ≤ P.map F

Tactic:
rw [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ P.strictMap F ≤ P.map F

Tactic:
P.strictMap_le_map F

Premises used: CategoryTheory.ObjectProperty.strictMap_le_map
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ P.strictMap F ≤ P.map F

Tactic:
exact P.strictMap_le_map F

Premises used: CategoryTheory.ObjectProperty.strictMap_le_map
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : D
Y : C
hY : P Y
e : F.obj Y ≅ X
⊢ (P.strictMap F).isoClosure X

Tactic:
⟨F.obj Y, ⟨Y, hY⟩, ⟨e.symm⟩⟩

Premises used: CategoryTheory.ObjectProperty.strictMap.mk, Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : D
Y : C
hY : P Y
e : F.obj Y ≅ X
⊢ (P.strictMap F).isoClosure X

Tactic:
exact ⟨F.obj Y, ⟨Y, hY⟩, ⟨e.symm⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ P.isoClosure.map F = P.map F

Tactic:
le_antisymm ?_ (map_monotone P.le_isoClosure F)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_antisymm, CategoryTheory.ObjectProperty.map_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
refine : P.isoClosure.map F ≤ P.map F
⊢ P.isoClosure.map F = P.map F

Tactic:
refine le_antisymm ?_ (map_monotone P.le_isoClosure F)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_antisymm, CategoryTheory.ObjectProperty.map_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : D
Y Z : C
hZ : P Z
e : Y ≅ Z
e' : F.obj Y ≅ X
⊢ P.map F X

Tactic:
⟨Z, hZ, ⟨F.mapIso e.symm ≪≫ e'⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Iso.trans, And.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.map, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : D
Y Z : C
hZ : P Z
e : Y ≅ Z
e' : F.obj Y ≅ X
⊢ P.map F X

Tactic:
exact ⟨Z, hZ, ⟨F.mapIso e.symm ≪≫ e'⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsStableUnderShift A
a : A
X : C
this : ∀ (Y : C) (hY : P Y) (i : X ⟶ Y) (r : Y ⟶ X) (w : i ≫ r = 𝟙 X), P.retractClosure.shift a X
⊢ P.retractClosure X ≤ P.retractClosure.shift a X

Tactic:
⟨Y, hY, i, r, w⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsStableUnderShift A
a : A
X Y : C
hY : P Y
i : X ⟶ Y
r : Y ⟶ X
w : i ≫ r = 𝟙 X
⊢ Functor.map (shiftFunctor C a) i ≫ Functor.map (shiftFunctor C a) r =
    𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsStableUnderShift A
a : A
X Y : C
hY : P Y
i : X ⟶ Y
r : Y ⟶ X
w : i ≫ r = 𝟙 X
⊢ P.retractClosure.shift a X

Tactic:
exact ⟨Y⟦a⟧, IsStableUnderShiftBy.le_shift Y hY, i⟦a⟧', r⟦a⟧', by grind⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X_1 X : C
hX : P X
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X

Tactic:
limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, CategoryTheory.ObjectProperty.limitsClosure.of_mem
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X_1 X : C
hX : P X
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X

Tactic:
exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)

Premises used: CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, CategoryTheory.ObjectProperty.limitsClosure.of_mem
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X X_1 Y : C
e : X_1 ≅ Y
hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X_1
hX' : (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X_1
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a Y

Tactic:
limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctor, CategoryTheory.ObjectProperty.limitsClosure.of_isoClosure, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X X_1 Y : C
e : X_1 ≅ Y
hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X_1
hX' : (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X_1
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a Y

Tactic:
exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.ObjectProperty.limitsClosure.of_isoClosure, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X X_1 : C
a_1 : α
pres : Limits.LimitPresentation.{u_5, u_4, v_1, u_1} (J a_1) X_1
h : ∀ (j : J a_1), limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J (pres.diag.obj j)
h' : ∀ (j : J a_1), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a (pres.diag.obj j)
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X_1

Tactic:
limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'

Premises used: CategoryTheory.Limits.LimitPresentation.map, CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctor, CategoryTheory.ObjectProperty.limitsClosure.of_limitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X X_1 : C
a_1 : α
pres : Limits.LimitPresentation.{u_5, u_4, v_1, u_1} (J a_1) X_1
h : ∀ (j : J a_1), limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J (pres.diag.obj j)
h' : ∀ (j : J a_1), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a (pres.diag.obj j)
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X_1

Tactic:
exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'

Premises used: CategoryTheory.Limits.LimitPresentation.map, CategoryTheory.shiftFunctor, CategoryTheory.ObjectProperty.limitsClosure.of_limitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X : C
hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X
of_mem : ∀ (X : C) (hX : P X), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
of_isoClosure :
  ∀ {X Y : C} (e : X ≅ Y) (hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X)
    (hX' : (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X),
    (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a Y
of_limitPresentation :
  ∀ {X : C} {a_1 : α} (pres : Limits.LimitPresentation.{u_5, u_4, v_1, u_1} (J a_1) X)
    (h : ∀ (j : J a_1), limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J (pres.diag.obj j))
    (h' : ∀ (j : J a_1), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a (pres.diag.obj j)),
    (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X

Tactic:
induction hX with
    | of_mem X hX => exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)
    | of_isoClosure e hX hX' => exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'
    | of_limitPresentation pres h h' =>
      exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'

Premises used: CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, CategoryTheory.ObjectProperty.limitsClosure.of_mem
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
⊢ P ≤ P.colimitsCardinalClosure κ

Tactic:
P.le_colimitsClosure _

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure, CategoryTheory.ObjectProperty.le_colimitsClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
⊢ (P.colimitsClosure (SmallCategoryCardinalLT.categoryFamily κ)).IsClosedUnderIsomorphisms

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsClosure (SmallCategoryCardinalLT.categoryFamily κ))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
S : SmallCategoryCardinalLT κ
⊢ IsClosedUnderColimitsOfShape.{w, w, v, u} (P.colimitsClosure (SmallCategoryCardinalLT.categoryFamily κ))
    (SmallCategoryCardinalLT.categoryFamily κ S)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
J : Type u'
inst_1 : Category.{v', u'} J
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
obtain :
  ∀ (S : SmallCategoryCardinalLT κ) (e : Equivalence.{w, v', w, u'} (SmallCategoryCardinalLT.categoryFamily κ S) J),
    IsClosedUnderColimitsOfShape.{v', u', v, u} (P.colimitsCardinalClosure κ) J
⊢ IsClosedUnderColimitsOfShape.{v', u', v, u} (P.colimitsCardinalClosure κ) J

Tactic:
obtain ⟨S, ⟨e⟩⟩ := SmallCategoryCardinalLT.exists_equivalence κ J hJ

Premises used: CategoryTheory.SmallCategoryCardinalLT.exists_equivalence
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
J : Type u'
inst_1 : Category.{v', u'} J
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
S : SmallCategoryCardinalLT κ
e : Equivalence.{w, v', w, u'} (SmallCategoryCardinalLT.categoryFamily κ S) J
rw :
  IsClosedUnderColimitsOfShape.{w, w, v, u} (P.colimitsCardinalClosure κ) (SmallCategoryCardinalLT.categoryFamily κ S)
⊢ IsClosedUnderColimitsOfShape.{v', u', v, u} (P.colimitsCardinalClosure κ) J

Tactic:
rw [isClosedUnderColimitsOfShape_iff_of_equivalence _ e.symm]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
J : Type u'
inst_1 : Category.{v', u'} J
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
S : SmallCategoryCardinalLT κ
e : Equivalence.{w, v', w, u'} (SmallCategoryCardinalLT.categoryFamily κ S) J
⊢ IsClosedUnderColimitsOfShape.{w, w, v, u} (P.colimitsCardinalClosure κ) (SmallCategoryCardinalLT.categoryFamily κ S)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
Q : ObjectProperty.{v, u} C
inst_1 : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst_2 : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
⊢ ∀ (i : SmallCategoryCardinalLT κ),
    IsClosedUnderColimitsOfShape.{w, w, v, u} Q (SmallCategoryCardinalLT.categoryFamily κ i)

Tactic:
have (i : SmallCategoryCardinalLT κ) := hQ _ i.hasCardinalLT
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
Q : ObjectProperty.{v, u} C
inst_1 : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst_2 : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
this :
  ∀ (i : SmallCategoryCardinalLT κ),
    IsClosedUnderColimitsOfShape.{w, w, v, u} Q (SmallCategoryCardinalLT.categoryFamily κ i)
⊢ P.colimitsCardinalClosure κ ≤ Q

Tactic:
colimitsClosure_le h

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure, CategoryTheory.ObjectProperty.colimitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
Q : ObjectProperty.{v, u} C
inst_1 : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst_2 : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
this :
  ∀ (i : SmallCategoryCardinalLT κ),
    IsClosedUnderColimitsOfShape.{w, w, v, u} Q (SmallCategoryCardinalLT.categoryFamily κ i)
⊢ P.colimitsCardinalClosure κ ≤ Q

Tactic:
exact colimitsClosure_le h

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
simp : Finite (Arrow WalkingParallelPair)
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

Tactic:
simp only [hasCardinalLT_aleph0_iff]

Premises used: hasCardinalLT_aleph0_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ Finite (Arrow WalkingParallelPair)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair

Tactic:
have := P.isClosedUnderColimitsOfShape_colimitsCardinalClosure κ
    WalkingParallelPair (HasCardinalLT.of_le (by
      simp only [hasCardinalLT_aleph0_iff]
      infer_instance)
    (Cardinal.IsRegular.aleph0_le Fact.out))
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ (P.colimitsCardinalClosure κ).IsStableUnderRetracts

Tactic:
infer_instance
-- 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:
fun X hX ↦ .of_mem X hX

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

Tactic:
.mono (P.le_colimitsClosure J)

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, 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)
a : α
X : C
hX : ColimitOfShape.{v', u', v, u} (colimitsClosure.{t, v', u', v, u} P J) (J a) X
⊢ colimitsClosure.{t, v', u', v, u} P J X

Tactic:
.of_colimitPresentation hX.toColimitPresentation hX.prop_diag_obj

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.ObjectProperty.colimitsClosure.of_colimitPresentation, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- 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)
a : α
X : C
hX : ColimitOfShape.{v', u', v, u} (colimitsClosure.{t, v', u', v, u} P J) (J a) X
⊢ colimitsClosure.{t, v', u', v, u} P J X

Tactic:
exact .of_colimitPresentation hX.toColimitPresentation hX.prop_diag_obj
-- 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)
Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ colimitsClosure.{t, v', u', v, u} P J ≤ colimitsClosure.{t, v', u', v, u} Q J

Tactic:
colimitsClosure_le (h.trans (Q.le_colimitsClosure J))

Premises used: CategoryTheory.ObjectProperty.le_colimitsClosure, CategoryTheory.ObjectProperty.colimitsClosure_le, LE.le.trans
-- 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 : P.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderColimitsOfShape.{v', u', v, u} P (J a)
⊢ colimitsClosure.{t, v', u', v, u} P J = P

Tactic:
le_antisymm (colimitsClosure_le (le_refl P)) (P.le_colimitsClosure J)

Premises used: le_refl, le_antisymm, CategoryTheory.ObjectProperty.le_colimitsClosure, CategoryTheory.ObjectProperty.colimitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
inst_2 : ∀ (a : α), Nonempty.{u' + 1} (J a)
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (colimitsClosure.{t, v', u', v, u} ⊥ J) ⊥

Tactic:
colimitsClosure_eq_self _ _

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (colimitsClosure.{t, v', u', v, u} ⊤ J) ⊤

Tactic:
colimitsClosure_eq_self _ _

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_eq_self
-- 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.isoClosure J = colimitsClosure.{t, v', u', v, u} P J

Tactic:
le_antisymm (colimitsClosure_le ?_)
    (colimitsClosure_monotone _ P.le_isoClosure)

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

Tactic:
refine le_antisymm (colimitsClosure_le ?_)
    (colimitsClosure_monotone _ P.le_isoClosure)

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

Tactic:
rw [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_le_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:
le_colimitsClosure P J

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

Tactic:
exact le_colimitsClosure P J

Premises used: CategoryTheory.ObjectProperty.le_colimitsClosure