-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z_1 : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : HasPullback f g
hf : Q f
hfst : P.diagonal (X := pullback f g) (pullback.fst f g)
heq :
  Eq (α :=
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
        Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
          CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom ⋯ ⋯))
            (Iso.hom (pullbackSymmetry g f) ≫
              CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (pullback.diagonal (pullback.fst f g) :
                  pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (Iso.hom (diagonalObjPullbackFstIso f g) :
                  pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                    pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
⊢ P (X :=
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
      (pullback.diagonal g))
    (Y := pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
        Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
          CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom ⋯ ⋯))
            (Iso.hom (pullbackSymmetry g f) ≫
              CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (pullback.diagonal (pullback.fst f g) :
                  pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (Iso.hom (diagonalObjPullbackFstIso f g) :
                  pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                    pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
have H : P (X :=
  pullback (Y := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.diagonal g)
    (pullback.fst (pullback.snd g g ≫ g) f))
  (Y := pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
  (Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
      CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom sorry sorry))
        (Iso.hom (pullbackSymmetry g f) ≫
          CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
            (pullback.diagonal (pullback.fst f g) :
              pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
            (Iso.hom (diagonalObjPullbackFstIso f g) :
              pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
    pullback (Y := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.diagonal g)
        (pullback.fst (pullback.snd g g ≫ g) f) ⟶
      pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
Tactic: rw [cancel_left_of_respectsIso (P := P)]