awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{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
inst_2 : HasPullbacks.{v_2, u_2} A
inst_3 : HasPullbacks.{v_1, u_1} T
inst_4 : PreservesLimitsOfShape WalkingCospan L
X : T
inst_5 : P.IsStableUnderComposition
inst_6 : P.IsStableUnderBaseChange
inst_7 : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
rw : P (L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom)
⊢ P Y.hom

Tactic:
rw [show Y.hom = L.map (pres.π.app .left).left ≫ (pres.diag.obj .left).hom by 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
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
inst_2 : HasPullbacks.{v_2, u_2} A
inst_3 : HasPullbacks.{v_1, u_1} T
inst_4 : PreservesLimitsOfShape WalkingCospan L
X : T
inst_5 : P.IsStableUnderComposition
inst_6 : P.IsStableUnderBaseChange
inst_7 : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
apply : P (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom)

Tactic:
apply P.comp_mem _ _ (P.of_isPullback h.flip ?_) (hpres _)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{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
inst_2 : HasPullbacks.{v_2, u_2} A
inst_3 : HasPullbacks.{v_1, u_1} T
inst_4 : PreservesLimitsOfShape WalkingCospan L
X : T
inst_5 : P.IsStableUnderComposition
inst_6 : P.IsStableUnderBaseChange
inst_7 : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.diag.map WalkingCospan.Hom.inr).left ≫ (pres.diag.obj WalkingCospan.one).hom)

Tactic:
simpa using hpres .right

Premises used: CategoryTheory.Limits.WalkingCospan.right
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{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
inst_2 : HasPullbacks.{v_2, u_2} A
inst_3 : HasPullbacks.{v_1, u_1} T
inst_4 : PreservesLimitsOfShape WalkingCospan L
X : T
inst_5 : P.IsStableUnderComposition
inst_6 : P.IsStableUnderBaseChange
inst_7 : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.diag.map WalkingCospan.Hom.inr).left)

Tactic:
exact P.of_postcomp _ (pres.diag.obj WalkingCospan.one).hom (hpres .one)
      (by simpa using hpres .right)

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.Limits.WalkingCospan.one, CategoryTheory.MorphismProperty.of_postcomp, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Functor.obj
-- 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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
X : T
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
inst_6 : HasPullbacks.{v_2, u_2} A
inst_7 : HasPullbacks.{v_1, u_1} T
inst_8 : PreservesLimitsOfShape WalkingCospan L
inst : HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))
inst₁ : (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan
⊢ CreatesLimitsOfShape (C := P.CostructuredArrow ⊤ L X) WalkingCospan (CostructuredArrow.forget P ⊤ L 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
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
X : T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
inst_5 : HasPullbacks.{v_2, u_2} A
inst_6 : HasPullbacks.{v_1, u_1} T
inst_7 : PreservesLimitsOfShape WalkingCospan L
⊢ HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))

Tactic:
inferInstanceAs (HasLimitsOfShape WalkingCospan (CostructuredArrow L X))

Premises used: CategoryTheory.MorphismProperty.CostructuredArrow.createsLimitsOfShape_walkingCospan._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
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
X : T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
inst_5 : HasPullbacks.{v_2, u_2} A
inst_6 : HasPullbacks.{v_1, u_1} T
inst_7 : PreservesLimitsOfShape WalkingCospan L
⊢ HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))

Tactic:
exact inferInstanceAs (HasLimitsOfShape WalkingCospan (CostructuredArrow L 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
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
X : T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
inst_5 : HasPullbacks.{v_2, u_2} A
inst_6 : HasPullbacks.{v_1, u_1} T
inst_7 : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan

Tactic:
CostructuredArrow.closedUnderLimitsOfShape_walkingCospan _ _

Premises used: CategoryTheory.MorphismProperty.costructuredArrowObj, CategoryTheory.MorphismProperty.commaObj, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_walkingCospan
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{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
X : T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
inst_5 : HasPullbacks.{v_2, u_2} A
inst_6 : HasPullbacks.{v_1, u_1} T
inst_7 : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan

Tactic:
exact CostructuredArrow.closedUnderLimitsOfShape_walkingCospan _ _

Premises used: CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_walkingCospan
-- 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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
X : T
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderBaseChange
inst_5 : P.HasOfPostcompProperty P
inst_6 : HasPullbacks.{v_2, u_2} A
inst_7 : HasPullbacks.{v_1, u_1} T
inst_8 : PreservesLimitsOfShape WalkingCospan L
inst : HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))
inst₁ : (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan
⊢ HasPullbacks (P.CostructuredArrow ⊤ L X)

Tactic:
apply +allowSynthFailures hasLimitsOfShape_of_closedUnderLimitsOfShape

Premises used: CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{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
X : T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.HasOfPostcompProperty P
inst_5 : HasPullbacks.{v_2, u_2} A
inst_6 : HasPullbacks.{v_1, u_1} T
inst_7 : PreservesLimitsOfShape WalkingCospan L
⊢ PreservesLimitsOfShape WalkingCospan (CostructuredArrow.toOver P L X)

Tactic:
have : PreservesLimitsOfShape WalkingCospan
      (CostructuredArrow.toOver P L X ⋙ Over.forget P ⊤ X) :=
    inferInstanceAs <| PreservesLimitsOfShape WalkingCospan <|
      CostructuredArrow.forget P ⊤ L X ⋙ CategoryTheory.CostructuredArrow.toOver L X
  preservesLimitsOfShape_of_reflects_of_preserves _ (Over.forget _ _ X)

Premises used: CategoryTheory.MorphismProperty.CostructuredArrow.toOver, _private.0.CategoryTheory.MorphismProperty.CostructuredArrow.instPreservesLimitsOfShapeTopOverWalkingCospanToOver._proof_1, CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, 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
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
inst_2 : L.Faithful
inst_3 : L.Full
Y : A
inst_4 : P.ContainsIdentities
inst_5 : P.RespectsIso
X : StructuredArrow (L.obj Y) L
p : ObjectProperty.colimitsOfShape (MorphismProperty.structuredArrowObj L P) (Discrete PEmpty.{1}) X
t : IsInitial X := ⋯.some
e : X ≅ mk (𝟙 (L.obj Y)) := t.uniqueUpToIso mkIdInitial
⊢ MorphismProperty.structuredArrowObj L P X

Tactic:
simpa [MorphismProperty.structuredArrowObj_iff,
      P.structuredArrow_iso_iff e] using P.id_mem (L.obj Y)

Premises used: CategoryTheory.MorphismProperty.structuredArrowObj_iff, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Functor.obj, CategoryTheory.MorphismProperty.structuredArrow_iso_iff
-- 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
⊢ Y.hom =
    hd.lift
      { pt := X,
        π :=
          { app := fun (j : J) ↦ (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }

Tactic:
hd.hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- 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
refine :
  ∀ (j : J),
    Y.hom ≫ ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone).π.app j =
      hd.lift
          { pt := X,
            π :=
              {
                app := fun (j : J) ↦
                  (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ } } ≫
        ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone).π.app j
⊢ Y.hom =
    hd.lift
      { pt := X,
        π :=
          { app := fun (j : J) ↦ (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }

Tactic:
refine hd.hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- 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
j : J
simp :
  Y.hom ≫ ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone).π.app j =
    (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom
⊢ Y.hom ≫ ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone).π.app j =
    hd.lift
        { pt := X,
          π :=
            {
              app := fun (j : J) ↦
                (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } } ≫
      ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone).π.app j

Tactic:
simp only [IsLimit.fac]

Premises used: CategoryTheory.Limits.IsLimit.fac
-- 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
j : J
⊢ Y.hom ≫ ((proj X L ⋙ L).mapCone d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).cone).π.app j =
    (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom

Tactic:
simp
-- 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
⊢ Y.hom =
    hd.lift
      { pt := X,
        π :=
          { app := fun (j : J) ↦ (d.toLimitPresentation (P := MorphismProperty.structuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }

Tactic:
have heq : Y.hom = hd.lift { pt := X, π := { app j := (d.diag.obj j).hom } } := by
      refine hd.hom_ext fun j ↦ ?_
      simp only [IsLimit.fac]
      simp
-- 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 := ⋯ } }
rw :
  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)))
⊢ MorphismProperty.structuredArrowObj L P Y

Tactic:
rw [P.structuredArrowObj_iff, heq, ← (hc _).lift_comp_conePointUniqueUpToIso_hom hd,
      P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom, CategoryTheory.MorphismProperty.structuredArrowObj_iff, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso