awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
X : C
h_1 : P.ind.inverseImage F X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
refine_1 : F.asEquivalence.inverse.obj (F.obj X) ≅ X
refine_2 :
  ∀ (j : J),
    P.inverseImage F (((pres.map F.asEquivalence.inverse).ofIso (F.asEquivalence.unitIso.app X).symm).diag.obj j)
⊢ (P.inverseImage F).ind X

Tactic:
refine ⟨J, ‹_›, ‹_›, .ofIso (pres.map F.asEquivalence.inverse) ?_, fun j ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
X : C
h_1 : P.ind.inverseImage F X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
⊢ F.asEquivalence.inverse.obj (F.obj X) ≅ X

Tactic:
exact (F.asEquivalence.unitIso.app X).symm

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
X : C
h_1 : P.ind.inverseImage F X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
j : J
⊢ P.inverseImage F (((pres.map F.asEquivalence.inverse).ofIso (F.asEquivalence.unitIso.app X).symm).diag.obj j)

Tactic:
P.prop_of_iso ((F.asEquivalence.counitIso.app _).symm) (h j)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.ObjectProperty.inverseImage, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
X : C
h_1 : P.ind.inverseImage F X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
j : J
⊢ P.inverseImage F (((pres.map F.asEquivalence.inverse).ofIso (F.asEquivalence.unitIso.app X).symm).diag.obj j)

Tactic:
exact P.prop_of_iso ((F.asEquivalence.counitIso.app _).symm) (h j)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
a :
  ∀ (x : Type w) (x_1 : SmallCategory x),
    IsFiltered x →
      ((∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
          ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) ↔
        ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i))
⊢ (∃ (J : Type w) (x : SmallCategory J) (_ : IsFiltered J) (pres :
      ColimitPresentation.{w, w, v, u} J (e.inverse.obj X)), ∀ (i : J), P.inverseImage e.functor (pres.diag.obj i)) ↔
    ∃ (J : Type w) (x : SmallCategory J) (_ : IsFiltered J) (pres : ColimitPresentation.{w, w, u_2, u_1} J X),
      ∀ (i : J), P (pres.diag.obj i)

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h : IsFiltered x
⊢ (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) ↔
    ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)

Tactic:
⟨fun ⟨pres, h⟩ ↦ ?_, fun ⟨pres, h⟩ ↦ ?_⟩

Premises used: Exists, _private.0.CategoryTheory.ObjectProperty.ind_iff_of_equivalence.match_1, Iff.intro, _private.0.CategoryTheory.ObjectProperty.ind_iff_of_equivalence.match_2
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h : IsFiltered x
a :
  (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) →
    ∀ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X))
      (h : ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)),
      ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
a₁ :
  (∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)) →
    ∀ (pres : ColimitPresentation.{w, w, u_2, u_1} x X) (h : ∀ (i : x), P (pres.diag.obj i)),
      ∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
        ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)
⊢ (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) ↔
    ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)

Tactic:
refine ⟨fun ⟨pres, h⟩ ↦ ?_, fun ⟨pres, h⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h_1 : IsFiltered x
h_2 :
  ∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)), ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)
pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)
h : ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)
⊢ ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)

Tactic:
⟨.ofIso (pres.map e.functor) (e.counitIso.app X), fun i ↦ h i⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Limits.ColimitPresentation.map, CategoryTheory.Limits.ColimitPresentation.ofIso, Exists.intro, CategoryTheory.Iso.app, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h_1 : IsFiltered x
h_2 :
  ∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)), ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)
pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)
h : ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)
⊢ ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)

Tactic:
exact ⟨.ofIso (pres.map e.functor) (e.counitIso.app X), fun i ↦ h i⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h_1 : IsFiltered x
h_2 : ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
pres : ColimitPresentation.{w, w, u_2, u_1} x X
h : ∀ (i : x), P (pres.diag.obj i)
⊢ ∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)), ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)

Tactic:
⟨pres.map e.inverse, fun i ↦ P.prop_of_iso ((e.counitIso.app _).symm) (h i)⟩

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.ColimitPresentation.map, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h_1 : IsFiltered x
h_2 : ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
pres : ColimitPresentation.{w, w, u_2, u_1} x X
h : ∀ (i : x), P (pres.diag.obj i)
⊢ ∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)), ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)

Tactic:
exact ⟨pres.map e.inverse, fun i ↦ P.prop_of_iso ((e.counitIso.app _).symm) (h i)⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type w
inst_1 : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete ι)
inst_2 : HasProductsOfShape.{w, u, v} ι C
inst_3 : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
hc : ∀ (i : ι), P.ind (X i)
choose :
  ∀ (J : (i : ι) → Type w) (x : (i : ι) → SmallCategory (J i)),
    (∀ (i : ι), IsFiltered.{w, w} (J i)) →
      ∀ (pres : (i : ι) → ColimitPresentation.{w, w, v, u} (J i) (X i))
        (hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)), P.ind (piObj.{w, v, u} X)
⊢ P.ind (piObj.{w, v, u} X)

Tactic:
choose J _ _ pres hpres using hc
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type w
inst_1 : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete ι)
inst_2 : HasProductsOfShape.{w, u, v} ι C
inst_3 : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
J : (i : ι) → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
pres : (i : ι) → ColimitPresentation.{w, w, v, u} (J i) (X i)
hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)
obtain :
  ∀
    (hc :
      IsColimit.{w, v, w, u} (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) fun (i : ι) ↦ (pres i).diag)
        (coconePointwiseProduct (I := J) fun (i : ι) ↦ { pt := X i, ι := (pres i).ι })),
    P.ind (piObj.{w, v, u} X)
⊢ P.ind (piObj.{w, v, u} X)

Tactic:
obtain ⟨hc⟩ := IsIPCOfShape.nonempty_isColimit fun i ↦ (pres i).isColimit

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type w
inst_1 : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete ι)
inst_2 : HasProductsOfShape.{w, u, v} ι C
inst_3 : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
J : (i : ι) → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
pres : (i : ι) → ColimitPresentation.{w, w, v, u} (J i) (X i)
hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)
hc :
  IsColimit.{w, v, w, u} (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) fun (i : ι) ↦ (pres i).diag)
    (coconePointwiseProduct (I := J) fun (i : ι) ↦ { pt := X i, ι := (pres i).ι })
⊢ P.ind (piObj.{w, v, u} X)

Tactic:
⟨∀ j, J j, inferInstance, inferInstance,
    { diag := _, ι := _, isColimit := hc }, fun i ↦ P.prop_limit _ fun a ↦ hpres a.1 _⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.Pi.constCompPiIsoConst, CategoryTheory.Discrete.functor, inferInstance, CategoryTheory.Limits.Cocone.mk, CategoryTheory.ObjectProperty.prop_limit, CategoryTheory.Limits.ColimitPresentation.mk, CategoryTheory.Limits.Pi.functor, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Functor.whiskerRight, CategoryTheory.Discrete.as, CategoryTheory.Limits.Cocone.ι, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.pi, CategoryTheory.Limits.pointwiseProduct, CategoryTheory.Functor.pi, CategoryTheory.ObjectProperty.ind, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type w
inst_1 : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete ι)
inst_2 : HasProductsOfShape.{w, u, v} ι C
inst_3 : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
J : (i : ι) → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
pres : (i : ι) → ColimitPresentation.{w, w, v, u} (J i) (X i)
hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)
hc :
  IsColimit.{w, v, w, u} (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) fun (i : ι) ↦ (pres i).diag)
    (coconePointwiseProduct (I := J) fun (i : ι) ↦ { pt := X i, ι := (pres i).ι })
⊢ P.ind (piObj.{w, v, u} X)

Tactic:
exact ⟨∀ j, J j, inferInstance, inferInstance,
    { diag := _, ι := _, isColimit := hc }, fun i ↦ P.prop_limit _ fun a ↦ hpres a.1 _⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
⊢ IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι)

Tactic:
.mk' fun X ⟨Y, h⟩ ↦ ?_

Premises used: _private.0.CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_ind_discrete.match_1, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk', CategoryTheory.ObjectProperty.ind
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
refine :
  ∀ (X : C),
    strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X →
      ∀ (Y : Functor.{u_1, v, u_1, u} (Discrete ι) C) (h : ∀ (j : Discrete ι), P.ind (Y.obj j)), P.ind (limit Y)
⊢ IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι)

Tactic:
refine .mk' fun X ⟨Y, h⟩ ↦ ?_
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
⊢ HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C

Tactic:
have : HasProductsOfShape (Shrink.{w} ι) C :=
    hasLimitsOfShape_of_equivalence (Discrete.equivalence e)
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
⊢ IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C

Tactic:
have : IsIPCOfShape.{w} (Shrink.{w} ι) C := .of_equiv e
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this_1 : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
this : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
⊢ IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete (Shrink.{w, u_1} ι))

Tactic:
have : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w} ι)) :=
    .of_equivalence (Discrete.equivalence e)
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this_1 : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
this_2 : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅
  piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i } :=
  Iso.trans (Y := piObj.{u_1, v, u} fun (j : ι) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (Iso.symm (Pi.reindex e.symm fun (j : ι) ↦ Y.obj { as := j }))
rw : P.ind (piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i })
⊢ P.ind (limit Y)

Tactic:
rw [(ind.{w} P).prop_iff_of_iso iso]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this_1 : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
this_2 : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅
  piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i } :=
  Iso.trans (Y := piObj.{u_1, v, u} fun (j : ι) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (Iso.symm (Pi.reindex e.symm fun (j : ι) ↦ Y.obj { as := j }))
⊢ P.ind (piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i })

Tactic:
ind_pi_of_ind fun i ↦ h _

Premises used: _private.0.CategoryTheory.ObjectProperty.ind_pi_of_ind, CategoryTheory.Discrete.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
ι : Type u_1
inst_1 : Small.{w, u_1} ι
inst_2 : IsClosedUnderLimitsOfShape.{u_1, u_1, v, u} P (Discrete ι)
inst_3 : HasProductsOfShape.{u_1, u, v} ι C
inst_4 : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
h_1 : strictLimitsOfShape.{u_1, u_1, v, u} P.ind (Discrete ι) X
Y : Functor.{u_1, v, u_1, u} (Discrete ι) C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : Equiv.{u_1 + 1, w + 1} ι (Shrink.{w, u_1} ι) := equivShrink ι
this_1 : HasProductsOfShape.{w, u, v} (Shrink.{w, u_1} ι) C
this_2 : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : IsClosedUnderLimitsOfShape.{w, w, v, u} P (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅
  piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i } :=
  Iso.trans (Y := piObj.{u_1, v, u} fun (j : ι) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (Iso.symm (Pi.reindex e.symm fun (j : ι) ↦ Y.obj { as := j }))
⊢ P.ind (piObj.{w, v, u} fun (i : Shrink.{w, u_1} ι) ↦ Y.obj { as := (e.symm : (a : Shrink.{w, u_1} ι) → ι) i })

Tactic:
exact ind_pi_of_ind fun i ↦ h _

Premises used: _private.0.CategoryTheory.ObjectProperty.ind_pi_of_ind
-- 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
W : MorphismProperty.{v_1, u_1} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
inst_2 : HasKernel f
⊢ W.kernels.Nonempty

Tactic:
ObjectProperty.nonempty_of_prop (kernels.of_isLimit f _ (kernelIsKernel f) hf)

Premises used: CategoryTheory.MorphismProperty.kernels.of_isLimit, CategoryTheory.ObjectProperty.nonempty_of_prop, CategoryTheory.Limits.kernelIsKernel
-- 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
W : MorphismProperty.{v_1, u_1} C
Y X₁ X₂ : C
f : X₁ ⟶ X₂
k : KernelFork f
hk : IsLimit k
hf : W f
i : k.pt ≅ Y
⊢ (i.inv ≫ Fork.ι k) ≫ f = 0

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
W : MorphismProperty.{v_1, u_1} C
Y X₁ X₂ : C
f : X₁ ⟶ X₂
k : KernelFork f
hk : IsLimit k
hf : W f
i : k.pt ≅ Y
⊢ W.kernels Y

Tactic:
exact .of_isLimit f (KernelFork.ofι (i.inv ≫ k.ι) (by simp))
      (IsLimit.ofIsoLimit hk (Fork.ext i)) 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
W : MorphismProperty.{v_1, u_1} C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
inst_2 : HasCokernel f
⊢ W.cokernels.Nonempty

Tactic:
ObjectProperty.nonempty_of_prop (cokernels.of_isColimit f _ (cokernelIsCokernel f) hf)

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.ObjectProperty.nonempty_of_prop, 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
W : MorphismProperty.{v_1, u_1} C
Y X₁ X₂ : C
f : X₁ ⟶ X₂
k : CokernelCofork f
hk : IsColimit k
hf : W f
i : k.pt ≅ Y
⊢ f ≫ Cofork.π k ≫ i.hom = 0

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
W : MorphismProperty.{v_1, u_1} C
Y X₁ X₂ : C
f : X₁ ⟶ X₂
k : CokernelCofork f
hk : IsColimit k
hf : W f
i : k.pt ≅ Y
⊢ W.cokernels Y

Tactic:
exact .of_isColimit f (CokernelCofork.ofπ (k.π ≫ i.hom) (by simp))
      (IsColimit.ofIsoColimit hk (Cofork.ext i)) 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.IsClosedUnderKernels
X Y : C
f : X ⟶ Y
k : KernelFork f
hk : IsLimit k
hX : P X
hY : P Y
⊢ P k.pt

Tactic:
IsClosedUnderKernels.kernels_le _ (.of_isLimit _ k hk ⟨hX, hY⟩)

Premises used: CategoryTheory.MorphismProperty.kernels.of_isLimit, CategoryTheory.ObjectProperty.IsClosedUnderKernels.kernels_le, And.intro
-- 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 : C
f : X ⟶ Y
inst_3 : HasKernel f
hX : P X
hY : P Y
⊢ P (kernel f)

Tactic:
(P.prop_of_isLimit_kernelFork (kernelIsKernel f) hX hY :)

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit_kernelFork, CategoryTheory.Limits.limit, CategoryTheory.Limits.kernelIsKernel