-- 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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
h :
  Eq (α :=
    (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
        (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).left)
    (CategoryStruct.comp (Y :=
      Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (Functor.map (𝟭 (P.Over Q X)) g ≫
              Over.homMk (P := P) (Q := Q)
                (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
                  B.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
                ⋯ ⋯)) :
        (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
          (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.fst (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))
    (CategoryStruct.comp (Y :=
      Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (Over.homMk (P := P) (Q := Q)
                (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
                  A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
                ⋯ ⋯ ≫
              Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)) :
        (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
          (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.fst (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))
⊢ Eq (α :=
    (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
        (Functor.map (𝟭 (P.Over Q X)) g ≫
          Over.homMk (P := P) (Q := Q)
            (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
              B.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
            ⋯ ⋯)))
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
        (Over.homMk (P := P) (Q := Q)
            (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
              A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
            ⋯ ⋯ ≫
          Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)))
have h₁ : Eq (α := (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶ X)
  (CategoryStruct.comp (Y :=
    Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
          (Functor.map (𝟭 (P.Over Q X)) g ≫
            Over.homMk (P := P) (Q := Q)
              (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
                B.toComma (P := P) (Q := Q) (W := ⊤).hom sorry)
              sorry sorry)) :
      (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
        (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.snd (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))
  (CategoryStruct.comp (Y :=
    Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
          (Over.homMk (P := P) (Q := Q)
              (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
                A.toComma (P := P) (Q := Q) (W := ⊤).hom sorry)
              sorry sorry ≫
            Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)) :
      (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
        (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.snd (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))
Tactic: apply pullback.hom_ext