-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)
H :
  P (X := pullback f g) (Y := pullback (X := pullback g g) (pullback.snd g g ≫ 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 f 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)

Tactic:
iterate 4 rw [cancel_left_of_respectsIso (P := P)]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso