awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : C
inst_1 : HasCoproducts.{u, v_1, u_1} C
inst_2 : MonoCoprod.{v_1, u_1} C
J I : Type u
ι : J ⟶ I
hι :
  Function.Injective (α := (fun (X : Type u) ↦ X) J) (β := (fun (X : Type u) ↦ X) I)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ι) : (a : (fun (X : Type u) ↦ X) J) → (fun (X : Type u) ↦ X) I)
⊢ Mono.{v_1, u_1} (X := Functor.obj.{u, v_1, u + 1, u_1} (Functor.obj sigmaConst A) J)
    (Functor.map (Functor.obj sigmaConst A) ι)

Tactic:
MonoCoprod.mono_map'_of_injective (fun (i : I) ↦ A) ι hι

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.colimit, CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.Sigma.map', DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : C
inst_1 : HasCoproducts.{u, v_1, u_1} C
inst_2 : MonoCoprod.{v_1, u_1} C
J I : Type u
ι : J ⟶ I
hι :
  Function.Injective (α := (fun (X : Type u) ↦ X) J) (β := (fun (X : Type u) ↦ X) I)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ι) : (a : (fun (X : Type u) ↦ X) J) → (fun (X : Type u) ↦ X) I)
⊢ Mono.{v_1, u_1} (X := Functor.obj.{u, v_1, u + 1, u_1} (Functor.obj sigmaConst A) J)
    (Functor.map (Functor.obj sigmaConst A) ι)

Tactic:
exact MonoCoprod.mono_map'_of_injective (fun (i : I) ↦ A) ι hι

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective, DFunLike.coe
-- 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
B : Type u_3
J : Type u_4
inst_1 : Category.{v_2, u_2} A
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} J
L : Functor.{v_2, v_1, u_2, u_1} A T
R : Functor.{v_3, v_1, u_3, u_1} B T
D : J ⥤ MorphismProperty.Comma L R P ⊤ ⊤
inst_4 : (commaObj L R P).IsClosedUnderLimitsOfShape J
inst_5 : HasLimit (D ⋙ forget L R P ⊤ ⊤)
⊢ HasLimit D

Tactic:
haveI : CreatesLimit D (forget L R P ⊤ ⊤) := forgetCreatesLimitOfClosed _ D
  hasLimit_of_created D (forget L R P ⊤ ⊤)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.MorphismProperty.Comma.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
B : Type u_3
J : Type u_4
inst_1 : Category.{v_2, u_2} A
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} J
L : Functor.{v_2, v_1, u_2, u_1} A T
R : Functor.{v_3, v_1, u_3, u_1} B T
D : J ⥤ MorphismProperty.Comma L R P ⊤ ⊤
inst_4 : (commaObj L R P).IsClosedUnderColimitsOfShape J
inst_5 : HasColimit (D ⋙ forget L R P ⊤ ⊤)
⊢ HasColimit D

Tactic:
haveI : CreatesColimit D (forget L R P ⊤ ⊤) := forgetCreatesColimitOfClosed _ D
  hasColimit_of_created D (forget L R P ⊤ ⊤)

Premises used: CategoryTheory.MorphismProperty.Comma.forget, Top.top, CategoryTheory.hasColimit_of_created
-- 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 : CostructuredArrow L (L.obj Y)
p : ObjectProperty.limitsOfShape (MorphismProperty.costructuredArrowObj L P) (Discrete PEmpty.{1}) X
t : IsTerminal X := ⋯.some
e : X ≅ mk (𝟙 (L.obj Y)) := t.uniqueUpToIso mkIdTerminal
⊢ MorphismProperty.costructuredArrowObj L P X

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

Premises used: CategoryTheory.MorphismProperty.costructuredArrow_iso_iff, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Functor.obj, CategoryTheory.MorphismProperty.costructuredArrowObj_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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
⊢ Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }

Tactic:
hd.hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
refine :
  ∀ (j : J),
    ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
        Y.hom =
      ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app
          j ≫
        hd.desc
          { pt := X,
            ι :=
              {
                app := fun (j : J) ↦
                  (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ } }
⊢ Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }

Tactic:
refine hd.hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
j : J
simp :
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      Y.hom =
    (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom
⊢ ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      Y.hom =
    ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      hd.desc
        { pt := X,
          ι :=
            {
              app := fun (j : J) ↦
                (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } }

Tactic:
simp only [Functor.const_obj_obj, IsColimit.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.const_obj_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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
j : J
⊢ ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      Y.hom =
    (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj 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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
⊢ Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }

Tactic:
have heq : Y.hom = hd.desc { pt := X, ι := { app j := (d.diag.obj j).hom } } := by
      refine hd.hom_ext fun j ↦ ?_
      simp only [Functor.const_obj_obj, IsColimit.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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
heq :
  Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }
rw :
  P (X :=
    Cocone.pt (F := d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
      (c (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)))
    (Y := X)
    (IsColimit.desc (hc (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L))
        { pt := X,
          ι :=
            {
              app := fun (j : J) ↦
                (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } } :
      Cocone.pt (F := d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
          (c (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)) ⟶
        Cocone.pt.{v_3, v_1, u_3, u_1} (J := J) (F :=
          d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
          { pt := X,
            ι :=
              {
                app := fun (j : J) ↦
                  (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ } })
⊢ MorphismProperty.costructuredArrowObj L P Y

Tactic:
rw [P.costructuredArrowObj_iff, heq, ← hd.coconePointUniqueUpToIso_hom_desc (hc _),
      P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc, CategoryTheory.MorphismProperty.costructuredArrowObj_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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
heq :
  Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }
⊢ P (X :=
    Cocone.pt (F := d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
      (c (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)))
    (Y := X)
    (IsColimit.desc (hc (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L))
        { pt := X,
          ι :=
            {
              app := fun (j : J) ↦
                (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } } :
      Cocone.pt (F := d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
          (c (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)) ⟶
        Cocone.pt.{v_3, v_1, u_3, u_1} (J := J) (F :=
          d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
          { pt := X,
            ι :=
              {
                app := fun (j : J) ↦
                  (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ } })

Tactic:
H _ _ d.prop_diag_obj

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.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 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
heq :
  Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }
⊢ P (X :=
    Cocone.pt (F := d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
      (c (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)))
    (Y := X)
    (IsColimit.desc (hc (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L))
        { pt := X,
          ι :=
            {
              app := fun (j : J) ↦
                (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } } :
      Cocone.pt (F := d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
          (c (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)) ⟶
        Cocone.pt.{v_3, v_1, u_3, u_1} (J := J) (F :=
          d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag ⋙ proj L X ⋙ L)
          { pt := X,
            ι :=
              {
                app := fun (j : J) ↦
                  (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
                naturality := ⋯ } })

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
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)
⊢ 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)

Tactic:
have h : IsPullback (L.map (pres.π.app .left).left) (L.map (pres.π.app .right).left)
        (L.map (pres.diag.map WalkingCospan.Hom.inl).left)
          (L.map (pres.diag.map WalkingCospan.Hom.inr).left) :=
      IsPullback.of_isLimit_cone <| isLimitOfPreserves
        (CategoryTheory.CostructuredArrow.toOver L X ⋙ CategoryTheory.Over.forget X) pres.isLimit
-- 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 Y.hom
⊢ MorphismProperty.costructuredArrowObj L P Y

Tactic:
rw [MorphismProperty.costructuredArrowObj_iff]

Premises used: CategoryTheory.MorphismProperty.costructuredArrowObj_iff
-- 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)
⊢ Y.hom = L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom

Tactic:
simp