-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
inst_3 : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst_4 : P.HasPushoutsAlong f
inst_5 : P.IsStableUnderCobaseChangeAlong f
inst_6 : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
h :
  CategoryStruct.comp (Y :=
      Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
            (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (CommaMorphism.right
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
            (Functor.map (map (P := P) Q hPf ⋙ pushout P Q f) g ≫
              Under.homMk (P := P) (Q := Q)
                (pushout.desc
                  (𝟙
                    (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                      (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := ⊤) (W := Q).right))
                  B.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
                ⋯ ⋯)) :
        (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right) =
    CategoryStruct.comp (Y :=
      Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
            (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (CommaMorphism.right
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
            (Under.homMk (P := P) (Q := Q)
                (pushout.desc
                  (𝟙
                    (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                      (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right))
                  A.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
                ⋯ ⋯ ≫
              Functor.map (𝟭 (P.Under Q Y)) g)) :
        (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right)
⊢ Eq (α :=
    (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
      (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right)
    (CommaMorphism.right
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
        (Functor.map (map (P := P) Q hPf ⋙ pushout P Q f) g ≫
          Under.homMk (P := P) (Q := Q)
            (pushout.desc
              (𝟙
                (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                  (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := ⊤) (W := Q).right))
              B.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
            ⋯ ⋯)))
    (CommaMorphism.right
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
        (Under.homMk (P := P) (Q := Q)
            (pushout.desc
              (𝟙
                (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                  (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right))
              A.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
            ⋯ ⋯ ≫
          Functor.map (𝟭 (P.Under Q Y)) g)))
have h₁ : CategoryStruct.comp (Y := Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
    (pushout.inr (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
      Y ⟶ Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
    (CommaMorphism.right
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
          (Functor.map (map (P := P) Q hPf ⋙ pushout P Q f) g ≫
            Under.homMk (P := P) (Q := Q)
              (pushout.desc
                (𝟙
                  (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                    (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := ⊤) (W := Q).right))
                B.toComma (P := P) (Q := ⊤) (W := Q).hom sorry)
              sorry sorry)) :
      (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right) =
  CategoryStruct.comp (Y :=
    Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
    (pushout.inr (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
      Y ⟶ Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
    (CommaMorphism.right
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
          (Under.homMk (P := P) (Q := Q)
              (pushout.desc
                (𝟙
                  (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                    (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right))
                A.toComma (P := P) (Q := ⊤) (W := Q).hom sorry)
              sorry sorry ≫
            Functor.map (𝟭 (P.Under Q Y)) g)) :
      (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right)
Tactic: apply pushout.hom_ext