-- 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)
h₀ :
  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) ⟶
      Y)
    ((pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) ≫
        pullback.fst (pullback.snd g g ≫ g) f) ≫
      pullback.fst g g)
    (CategoryStruct.comp (Y := pullback g g)
      (CategoryStruct.comp (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)
          (pullback.fst (pullback.snd g g ≫ g) f :
            pullback (X := pullback g g) (pullback.snd g g ≫ g) f ⟶ pullback g 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 g g)
      (pullback.fst g g : pullback g g ⟶ Y))
h₁ :
  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) ⟶
      Y)
    ((pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) ≫
        pullback.fst (pullback.snd g g ≫ g) f) ≫
      pullback.snd g g)
    (CategoryStruct.comp (Y := pullback g g)
      (CategoryStruct.comp (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)
          (pullback.fst (pullback.snd g g ≫ g) f :
            pullback (X := pullback g g) (pullback.snd g g ≫ g) f ⟶ pullback g 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 g g)
      (pullback.snd g g : pullback g g ⟶ Y))
⊢ 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 g g)
    (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) ≫
        pullback.fst (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 g g)
    (CategoryStruct.comp (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)
        (pullback.fst (pullback.snd g g ≫ g) f : pullback (X := pullback g g) (pullback.snd g g ≫ g) f ⟶ pullback g 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 g g)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext