awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderSubobjects
i : C
this :
  ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (k : KernelFork f) (hk : IsLimit k) (hf : MorphismProperty.ofObjectProperty P P f), P k.pt
⊢ (MorphismProperty.ofObjectProperty P P).kernels i ≤ P i

Tactic:
⟨_, k, hk, hf⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderSubobjects
i X₁ X₂ : C
f : X₁ ⟶ X₂
k : KernelFork f
hk : IsLimit k
hf : MorphismProperty.ofObjectProperty P P f
this : Mono (Fork.ι k) := ⋯
⊢ P k.pt

Tactic:
P.prop_of_mono k.ι hf.1

Premises used: And.left, CategoryTheory.Limits.Fork.ι, CategoryTheory.ObjectProperty.prop_of_mono
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderSubobjects
i X₁ X₂ : C
f : X₁ ⟶ X₂
k : KernelFork f
hk : IsLimit k
hf : MorphismProperty.ofObjectProperty P P f
this : Mono (Fork.ι k) := ⋯
⊢ P k.pt

Tactic:
exact P.prop_of_mono k.ι hf.1

Premises used: And.left, CategoryTheory.Limits.Fork.ι, CategoryTheory.ObjectProperty.prop_of_mono
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_2 : HasKernel f.hom
⊢ HasLimit (parallelPair f 0 ⋙ P.ι)

Tactic:
hasLimit_of_iso (F := parallelPair f.hom 0) (Iso.symm (diagramIsoParallelPair _))

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
c : Cone (parallelPair f 0 ⋙ P.ι)
hc :
  IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
      (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) ⋯))
h :
  P
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
        (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) ⋯)).pt
⊢ CreatesLimit (parallelPair f 0) P.ι

Tactic:
fapply createsLimitFullSubcategoryInclusion'

Premises used: CategoryTheory.Limits.createsLimitFullSubcategoryInclusion'
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
⊢ Eq (α := kernel f.hom ⟶ (parallelPair f 0 ⋙ P.ι).obj WalkingParallelPair.one)
    (kernel.ι f.hom ≫ (parallelPair f 0 ⋙ P.ι).map WalkingParallelPairHom.left)
    (kernel.ι f.hom ≫ (parallelPair f 0 ⋙ P.ι).map WalkingParallelPairHom.right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
⊢ Cone (parallelPair f 0 ⋙ P.ι)

Tactic:
exact (Cone.postcompose (Iso.symm (diagramIsoParallelPair _)).hom).obj
      (Fork.ofι (kernel.ι f.hom) (by simp))

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Iso.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cone.postcompose
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
⊢ IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
      (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) ⋯))

Tactic:
exact (IsLimit.postcomposeInvEquiv _ _).symm (kernelIsKernel f.hom)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.Limits.kernelIsKernel, CategoryTheory.InducedCategory.Hom.hom, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
⊢ P
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
        (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) ⋯)).pt

Tactic:
P.prop_kernel f.hom X.property Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.Limits.limit, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Limits.parallelPair, CategoryTheory.ObjectProperty.prop_kernel
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasKernel f.hom
⊢ P
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj
        (Fork.ofι (P := kernel f.hom) (kernel.ι f.hom) ⋯)).pt

Tactic:
exact P.prop_kernel f.hom X.property Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.ObjectProperty.prop_kernel
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
have : ∀ (this : CreatesLimit (parallelPair f 0) P.ι), PreservesLimit (parallelPair f 0) P.ι
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
have := P.createsKernels f
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this : CreatesLimit (parallelPair f 0) P.ι
⊢ HasLimit (parallelPair f 0 ⋙ P.ι)

Tactic:
have := P.hasLimit_parallelPair_comp_ι f
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this_1 : CreatesLimit (parallelPair f 0) P.ι
this : HasLimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
preservesLimit_of_createsLimit_and_hasLimit _ _

Premises used: CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this_1 : CreatesLimit (parallelPair f 0) P.ι
this : HasLimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
exact preservesLimit_of_createsLimit_and_hasLimit _ _

Premises used: CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : C
f : X ⟶ Y
k : CokernelCofork f
hk : IsColimit k
hX : P X
hY : P Y
⊢ P k.pt

Tactic:
IsClosedUnderCokernels.cokernels_le _ (.of_isColimit _ k hk ⟨hX, hY⟩)

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderCokernels.cokernels_le, And.intro, CategoryTheory.MorphismProperty.cokernels.of_isColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : C
f : X ⟶ Y
inst_3 : HasCokernel f
hX : P X
hY : P Y
⊢ P (cokernel f)

Tactic:
(P.prop_of_isColimit_cokernelCofork (cokernelIsCokernel f) hX hY :)

Premises used: CategoryTheory.ObjectProperty.prop_of_isColimit_cokernelCofork, CategoryTheory.Limits.colimit, CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderQuotients
i : C
this :
  ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (k : CokernelCofork f) (hk : IsColimit k) (hf : MorphismProperty.ofObjectProperty P P f),
    P k.pt
⊢ (MorphismProperty.ofObjectProperty P P).cokernels i ≤ P i

Tactic:
⟨_, k, hk, hf⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderQuotients
i X₁ X₂ : C
f : X₁ ⟶ X₂
k : CokernelCofork f
hk : IsColimit k
hf : MorphismProperty.ofObjectProperty P P f
this : Epi (Cofork.π k) := ⋯
⊢ P k.pt

Tactic:
P.prop_of_epi k.π hf.2

Premises used: And.right, CategoryTheory.ObjectProperty.prop_of_epi, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderQuotients
i X₁ X₂ : C
f : X₁ ⟶ X₂
k : CokernelCofork f
hk : IsColimit k
hf : MorphismProperty.ofObjectProperty P P f
this : Epi (Cofork.π k) := ⋯
⊢ P k.pt

Tactic:
exact P.prop_of_epi k.π hf.2

Premises used: And.right, CategoryTheory.ObjectProperty.prop_of_epi, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_2 : HasCokernel f.hom
⊢ HasColimit (parallelPair f 0 ⋙ P.ι)

Tactic:
hasColimit_of_iso (F := parallelPair f.hom 0) (diagramIsoParallelPair _)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoParallelPair
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
c : Cocone (parallelPair f 0 ⋙ P.ι)
hc :
  IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
      (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) ⋯))
h :
  P
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
        (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) ⋯)).pt
⊢ CreatesColimit (parallelPair f 0) P.ι

Tactic:
fapply createsColimitFullSubcategoryInclusion'

Premises used: CategoryTheory.Limits.createsColimitFullSubcategoryInclusion'
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
⊢ Eq (α := (parallelPair f 0 ⋙ P.ι).obj WalkingParallelPair.zero ⟶ cokernel f.hom)
    ((parallelPair f 0 ⋙ P.ι).map WalkingParallelPairHom.left ≫ cokernel.π f.hom)
    ((parallelPair f 0 ⋙ P.ι).map WalkingParallelPairHom.right ≫ cokernel.π f.hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
⊢ Cocone (parallelPair f 0 ⋙ P.ι)

Tactic:
exact (Cocone.precompose (diagramIsoParallelPair _).hom).obj
      (Cofork.ofπ (cokernel.π f.hom) (by simp))

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
⊢ IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
      (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) ⋯))

Tactic:
exact (IsColimit.precomposeHomEquiv _ _).symm (cokernelIsCokernel f.hom)

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.InducedCategory.Hom.hom, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
⊢ P
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
        (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) ⋯)).pt

Tactic:
P.prop_cokernel f.hom X.property Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.prop_cokernel, CategoryTheory.Limits.colimit, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst_3 : HasCokernel f.hom
⊢ P
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj
        (Cofork.ofπ (P := cokernel f.hom) (cokernel.π f.hom) ⋯)).pt

Tactic:
exact P.prop_cokernel f.hom X.property Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.prop_cokernel, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasCokernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
have : ∀ (this : CreatesColimit (parallelPair f 0) P.ι), PreservesColimit (parallelPair f 0) P.ι
⊢ PreservesColimit (parallelPair f 0) P.ι

Tactic:
have := P.createsCokernels f
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasCokernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
this : CreatesColimit (parallelPair f 0) P.ι
⊢ HasColimit (parallelPair f 0 ⋙ P.ι)

Tactic:
have := P.hasColimit_parallelPair_comp_ι f
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasCokernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
this_1 : CreatesColimit (parallelPair f 0) P.ι
this : HasColimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesColimit (parallelPair f 0) P.ι

Tactic:
preservesColimit_of_createsColimit_and_hasColimit _ _

Premises used: CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_2 : HasCokernels.{v_1, u_1} C
inst_3 : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
this_1 : CreatesColimit (parallelPair f 0) P.ι
this : HasColimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesColimit (parallelPair f 0) P.ι

Tactic:
exact preservesColimit_of_createsColimit_and_hasColimit _ _

Premises used: CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit
-- 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)
⊢ P ≤ limitsClosure.{t, v', u', v, u} P J

Tactic:
fun X hX ↦ .of_mem X hX

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

Tactic:
.mono (P.le_limitsClosure J)

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

Tactic:
.of_limitPresentation hX.toLimitPresentation hX.prop_diag_obj

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

Tactic:
exact .of_limitPresentation hX.toLimitPresentation hX.prop_diag_obj
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X_1 X : C
hX : P X
⊢ Q X

Tactic:
h _ hX
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X_1 X : C
hX : P X
⊢ Q X

Tactic:
exact h _ hX
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X X_1 Y : C
e : X_1 ≅ Y
hX : limitsClosure.{t, v', u', v, u} P J X_1
hX' : Q X_1
⊢ Q Y

Tactic:
Q.prop_of_iso e hX'

Premises used: CategoryTheory.ObjectProperty.prop_of_iso
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X X_1 Y : C
e : X_1 ≅ Y
hX : limitsClosure.{t, v', u', v, u} P J X_1
hX' : Q X_1
⊢ Q Y

Tactic:
exact Q.prop_of_iso e hX'

Premises used: CategoryTheory.ObjectProperty.prop_of_iso
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h_1 : P ≤ Q
X X_1 : C
a : α
pres : LimitPresentation.{v', u', v, u} (J a) X_1
h : ∀ (j : J a), limitsClosure.{t, v', u', v, u} P J (pres.diag.obj j)
h' : ∀ (j : J a), Q (pres.diag.obj j)
⊢ Q X_1

Tactic:
Q.prop_of_isLimit pres.isLimit h'

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit, CategoryTheory.Limits.LimitPresentation.isLimit
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h_1 : P ≤ Q
X X_1 : C
a : α
pres : LimitPresentation.{v', u', v, u} (J a) X_1
h : ∀ (j : J a), limitsClosure.{t, v', u', v, u} P J (pres.diag.obj j)
h' : ∀ (j : J a), Q (pres.diag.obj j)
⊢ Q X_1

Tactic:
exact Q.prop_of_isLimit pres.isLimit h'

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit, CategoryTheory.Limits.LimitPresentation.isLimit
-- 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)
Q : ObjectProperty.{v, u} C
inst_2 : Q.IsClosedUnderIsomorphisms
inst_3 : ∀ (a : α), IsClosedUnderLimitsOfShape.{v', u', v, u} Q (J a)
h : P ≤ Q
X : C
hX : limitsClosure.{t, v', u', v, u} P J X
of_mem : ∀ (X : C) (hX : P X), Q X
of_isoClosure : ∀ {X Y : C} (e : X ≅ Y) (hX : limitsClosure.{t, v', u', v, u} P J X) (hX' : Q X), Q Y
of_limitPresentation :
  ∀ {X : C} {a : α} (pres : LimitPresentation.{v', u', v, u} (J a) X)
    (h : ∀ (j : J a), limitsClosure.{t, v', u', v, u} P J (pres.diag.obj j)) (h' : ∀ (j : J a), Q (pres.diag.obj j)),
    Q X
⊢ Q X

Tactic:
induction hX with
  | of_mem X hX => exact h _ hX
  | of_isoClosure e hX hX' => exact Q.prop_of_iso e hX'
  | of_limitPresentation pres h h' => exact Q.prop_of_isLimit pres.isLimit 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)
Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ limitsClosure.{t, v', u', v, u} P J ≤ limitsClosure.{t, v', u', v, u} Q J

Tactic:
limitsClosure_le (h.trans (Q.le_limitsClosure J))

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

Tactic:
le_antisymm (limitsClosure_le (le_refl P)) (P.le_limitsClosure J)

Premises used: CategoryTheory.ObjectProperty.le_limitsClosure, le_refl, CategoryTheory.ObjectProperty.limitsClosure_le, le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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) (limitsClosure.{t, v', u', v, u} ⊥ J) ⊥

Tactic:
limitsClosure_eq_self _ _

Premises used: CategoryTheory.ObjectProperty.limitsClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
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) (limitsClosure.{t, v', u', v, u} ⊤ J) ⊤

Tactic:
limitsClosure_eq_self _ _

Premises used: CategoryTheory.ObjectProperty.limitsClosure_eq_self