awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
J : Type u_3
inst_2 : Category.{v_3, u_3} J
P : MorphismProperty.{v_1, u_1} T
inst_3 : P.RespectsIso
inst_4 : PreservesLimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasLimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasLimit D] → Cone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasLimit D] {X : T} (s : Functor.obj (Functor.const J) X ⟶ D),
    (∀ (j : J), P (s.app j)) →
      P (X := { pt := X, π := s : Cone D }.pt) (Y := (c D).pt) (IsLimit.lift (hc D) { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : ObjectProperty.LimitOfShape (MorphismProperty.structuredArrowObj L P) J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone) :=
  isLimitOfPreserves (proj X L ⋙ L) d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).isLimit
heq :
  Y.hom =
    hd.lift
      { pt := X,
        π :=
          { app := fun (j : J) ↦ (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }
⊢ P (X := X) (Y :=
    Cone.pt (F := d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)
      (c (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)))
    (IsLimit.lift (hc (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L))
        { pt := X,
          π :=
            {
              app := fun (j : J) ↦
                (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } } :
      Cone.pt.{v_3, v_1, u_3, u_1} (J := J) (F :=
          d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)
          { pt := X,
            π :=
              {
                app := fun (j : J) ↦
                  (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ :
                NatTrans (Functor.obj (Functor.const J) X)
                  (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L) } :
            Cone (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L) } ⟶
        Cone.pt (F := d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)
          (c (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)))

Tactic:
H _ _ d.prop_diag_obj

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
J : Type u_3
inst_2 : Category.{v_3, u_3} J
P : MorphismProperty.{v_1, u_1} T
inst_3 : P.RespectsIso
inst_4 : PreservesLimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasLimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasLimit D] → Cone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasLimit D] {X : T} (s : Functor.obj (Functor.const J) X ⟶ D),
    (∀ (j : J), P (s.app j)) →
      P (X := { pt := X, π := s : Cone D }.pt) (Y := (c D).pt) (IsLimit.lift (hc D) { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : ObjectProperty.LimitOfShape (MorphismProperty.structuredArrowObj L P) J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone) :=
  isLimitOfPreserves (proj X L ⋙ L) d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).isLimit
heq :
  Y.hom =
    hd.lift
      { pt := X,
        π :=
          { app := fun (j : J) ↦ (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }
⊢ P (X := X) (Y :=
    Cone.pt (F := d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)
      (c (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)))
    (IsLimit.lift (hc (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L))
        { pt := X,
          π :=
            {
              app := fun (j : J) ↦
                (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } } :
      Cone.pt.{v_3, v_1, u_3, u_1} (J := J) (F :=
          d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)
          { pt := X,
            π :=
              {
                app := fun (j : J) ↦
                  (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ :
                NatTrans (Functor.obj (Functor.const J) X)
                  (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L) } :
            Cone (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L) } ⟶
        Cone.pt (F := d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)
          (c (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag ⋙ proj X L ⋙ L)))

Tactic:
exact H _ _ d.prop_diag_obj
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Over.{v_1, u_1} X) P.overObj (Discrete PEmpty.{1})

Tactic:
CostructuredArrow.closedUnderLimitsOfShape_discrete_empty P

Premises used: CategoryTheory.MorphismProperty.costructuredArrowObj, CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty, CategoryTheory.MorphismProperty.overObj
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Over.{v_1, u_1} X) P.overObj WalkingCospan

Tactic:
CostructuredArrow.closedUnderLimitsOfShape_walkingCospan _ _

Premises used: CategoryTheory.MorphismProperty.costructuredArrowObj, CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_walkingCospan, CategoryTheory.MorphismProperty.overObj
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ ObjectProperty.IsClosedUnderColimitsOfShape (C := Under.{v_1, u_1} X) P.underObj (Discrete PEmpty.{1})

Tactic:
StructuredArrow.closedUnderColimitsOfShape_discrete_empty (L := 𝟭 _) P

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.StructuredArrow.closedUnderColimitsOfShape_discrete_empty, CategoryTheory.MorphismProperty.underObj, CategoryTheory.Under, CategoryTheory.MorphismProperty.structuredArrowObj, CategoryTheory.Under.Hom
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
rw : ObjectProperty.IsClosedUnderLimitsOfShape (C := Over.{v_1, u_1} (Opposite.op X)) P.op.overObj WalkingCospan
⊢ ObjectProperty.IsClosedUnderColimitsOfShape (C := Under.{v_1, u_1} X) P.underObj WalkingSpan

Tactic:
rw [ObjectProperty.isClosedUnderColimitsOfShape_iff_op, ←
    ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff _ _ (Over.opEquivOpUnder _),
    MorphismProperty.inverseImage_op_underObj,
    ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence _ walkingSpanOpEquiv]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op, CategoryTheory.Over.opEquivOpUnder, CategoryTheory.Limits.walkingSpanOpEquiv, CategoryTheory.MorphismProperty.inverseImage_op_underObj, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Over.{v_1, u_1} (Opposite.op X)) P.op.overObj WalkingCospan

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst_1 : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_2 : P.ContainsIdentities
inst_3 : P.RespectsIso
inst : HasLimitsOfShape (Discrete PEmpty.{1}) (Comma.{v_1, 0, v_1, u_1, 0, u_1} (𝟭 T) (Functor.fromPUnit X))
inst₁ :
  ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma.{v_1, 0, v_1, u_1, 0, u_1} (𝟭 T) (Functor.fromPUnit X))
    (commaObj (𝟭 T) (Functor.fromPUnit X) P) (Discrete PEmpty.{1})
⊢ CreatesLimitsOfShape (C := P.Over ⊤ X) (Discrete PEmpty.{1}) (Over.forget P ⊤ X)

Tactic:
apply +allowSynthFailures forgetCreatesLimitsOfShapeOfClosed

Premises used: CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ HasLimitsOfShape (Discrete PEmpty.{1}) (Comma.{v_1, 0, v_1, u_1, 0, u_1} (𝟭 T) (Functor.fromPUnit X))

Tactic:
inferInstanceAs (HasLimitsOfShape _ (Over X))

Premises used: CategoryTheory.MorphismProperty.Over.instCreatesLimitsOfShapeTopOverDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso._proof_1
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ HasLimitsOfShape (Discrete PEmpty.{1}) (Comma.{v_1, 0, v_1, u_1, 0, u_1} (𝟭 T) (Functor.fromPUnit X))

Tactic:
exact inferInstanceAs (HasLimitsOfShape _ (Over X))
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma.{v_1, 0, v_1, u_1, 0, u_1} (𝟭 T) (Functor.fromPUnit X))
    (commaObj (𝟭 T) (Functor.fromPUnit X) P) (Discrete PEmpty.{1})

Tactic:
apply Over.closedUnderLimitsOfShape_discrete_empty _

Premises used: CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk (P := P) ⊤ (𝟙 X) ⋯
h :
  a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    CommaMorphism.left
      (Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (Over.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯))
⊢ a = Over.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk (P := P) ⊤ (𝟙 X) ⋯
h : a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left = Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom
⊢ a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    CommaMorphism.left
      (Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (Over.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯))

Tactic:
simp only [mk_left, homMk_hom, Over.homMk_left]

Premises used: CategoryTheory.Over.homMk_left, CategoryTheory.MorphismProperty.Over.mk_left, CategoryTheory.MorphismProperty.Over.homMk_hom
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk (P := P) ⊤ (𝟙 X) ⋯
h :
  a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      (toComma (P := P) (Q := ⊤) (W := ⊤) (Over.mk (P := P) ⊤ (𝟙 X) ⋯)).hom
⊢ a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left = Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
rw [← Over.w a]

Premises used: CategoryTheory.MorphismProperty.Over.w
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk (P := P) ⊤ (𝟙 X) ⋯
⊢ a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      (toComma (P := P) (Q := ⊤) (W := ⊤) (Over.mk (P := P) ⊤ (𝟙 X) ⋯)).hom

Tactic:
simp only [mk_left, Functor.const_obj_obj, mk_hom, Category.comp_id]

Premises used: CategoryTheory.MorphismProperty.Over.mk_hom, CategoryTheory.Category.comp_id, CategoryTheory.MorphismProperty.Over.mk_left, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
⊢ HasTerminal (P.Over ⊤ X)

Tactic:
let h : IsTerminal (Over.mk ⊤ (𝟙 X) (P.id_mem X)) := Over.mkIdTerminal P X
  h.hasTerminal

Premises used: CategoryTheory.MorphismProperty.Over.mkIdTerminal, CategoryTheory.Limits.IsTerminal.hasTerminal
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
⊢ HasPullbacks (P.Over ⊤ X)

Tactic:
CostructuredArrow.hasPullbacks _ _

Premises used: CategoryTheory.MorphismProperty.CostructuredArrow.hasPullbacks
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
inst_6 : HasFiniteWidePullbacks.{v_1, u_1} T
⊢ HasFiniteLimits (P.Over ⊤ X)

Tactic:
hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.forget P ⊤ X)

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits, CategoryTheory.MorphismProperty.Over.forget, Top.top
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
⊢ PreservesFiniteLimits (C := P.Over ⊤ X) (Over.forget P ⊤ X)

Tactic:
preservesFiniteLimits_of_preservesTerminal_and_pullbacks (Over.forget P ⊤ X)

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks, CategoryTheory.MorphismProperty.Over.forget, Top.top
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X_1 : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
X Y : T
f : X ⟶ Y
J : Type
x : SmallCategory J
x_1 : FinCategory J
⊢ PreservesLimitsOfShape (C := P.Over ⊤ Y) J (pullback P ⊤ f ⋙ Over.forget P ⊤ X)

Tactic:
have : PreservesLimitsOfShape J
        (MorphismProperty.Over.pullback P ⊤ f ⋙ MorphismProperty.Over.forget _ _ _) :=
      inferInstanceAs <| PreservesLimitsOfShape J <|
        Over.forget _ _ _ ⋙ CategoryTheory.Over.pullback f
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X_1 : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
X Y : T
f : X ⟶ Y
J : Type
x : SmallCategory J
x_1 : FinCategory J
this : PreservesLimitsOfShape (C := P.Over ⊤ Y) J (pullback P ⊤ f ⋙ Over.forget P ⊤ X)
⊢ PreservesLimitsOfShape (C := P.Over ⊤ Y) J (pullback P ⊤ f)

Tactic:
preservesLimitsOfShape_of_reflects_of_preserves
      (MorphismProperty.Over.pullback P ⊤ f) (MorphismProperty.Over.forget _ _ _)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.MorphismProperty.Over.pullback, CategoryTheory.MorphismProperty.Over.forget, Top.top
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X_1 : T
inst_1 : HasPullbacks.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
X Y : T
f : X ⟶ Y
J : Type
x : SmallCategory J
x_1 : FinCategory J
this : PreservesLimitsOfShape (C := P.Over ⊤ Y) J (pullback P ⊤ f ⋙ Over.forget P ⊤ X)
⊢ PreservesLimitsOfShape (C := P.Over ⊤ Y) J (pullback P ⊤ f)

Tactic:
exact preservesLimitsOfShape_of_reflects_of_preserves
      (MorphismProperty.Over.pullback P ⊤ f) (MorphismProperty.Over.forget _ _ _)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.MorphismProperty.Over.pullback, CategoryTheory.MorphismProperty.Over.forget, Top.top
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst_1 : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_2 : P.ContainsIdentities
inst_3 : P.RespectsIso
inst : HasColimitsOfShape (Discrete PEmpty.{1}) (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
inst₁ :
  ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
    (commaObj (Functor.fromPUnit X) (𝟭 T) P) (Discrete PEmpty.{1})
⊢ CreatesColimitsOfShape (C := P.Under ⊤ X) (Discrete PEmpty.{1}) (Under.forget P ⊤ X)

Tactic:
apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed

Premises used: CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitsOfShapeOfClosed
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ HasColimitsOfShape (Discrete PEmpty.{1}) (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))

Tactic:
inferInstanceAs (HasColimitsOfShape _ (Under X))

Premises used: CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso._proof_1
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ HasColimitsOfShape (Discrete PEmpty.{1}) (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))

Tactic:
exact inferInstanceAs (HasColimitsOfShape _ (Under X))
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
    (commaObj (Functor.fromPUnit X) (𝟭 T) P) (Discrete PEmpty.{1})

Tactic:
apply Under.closedUnderColimitsOfShape_discrete_empty _

Premises used: CategoryTheory.Under.closedUnderColimitsOfShape_discrete_empty
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Under ⊤ X
⊢ (toComma (P := P) (Q := ⊤) (W := ⊤) (Under.mk (P := P) ⊤ (𝟙 X) ⋯)).hom ≫ Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
    Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Under ⊤ X
a : Under.mk (P := P) ⊤ (𝟙 X) ⋯ ⟶ Y
h :
  a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).right =
    CommaMorphism.right
      (Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (Under.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯))
⊢ a = Under.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Under ⊤ X
a : Under.mk (P := P) ⊤ (𝟙 X) ⋯ ⟶ Y
⊢ a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).right =
    CommaMorphism.right
      (Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (Under.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯))

Tactic:
simp [← Under.w a]

Premises used: CategoryTheory.MorphismProperty.Under.w
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
⊢ HasInitial (P.Under ⊤ X)

Tactic:
(Under.mkIdInitial P X).hasInitial

Premises used: CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.MorphismProperty.Under.mkIdInitial
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst_1 : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_2 : HasPushouts.{v_1, u_1} T
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.HasOfPrecompProperty P
inst : HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
inst₁ :
  ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
    (commaObj (Functor.fromPUnit X) (𝟭 T) P) WalkingSpan
⊢ CreatesColimitsOfShape (C := P.Under ⊤ X) WalkingSpan (Under.forget P ⊤ X)

Tactic:
apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed

Premises used: CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitsOfShapeOfClosed
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
⊢ HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))

Tactic:
inferInstanceAs (HasColimitsOfShape WalkingSpan (Under X))

Premises used: CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderWalkingSpanForgetOfHasPushoutsOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty._proof_1
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
⊢ HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))

Tactic:
exact inferInstanceAs (HasColimitsOfShape WalkingSpan (Under X))