-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasEqualizers.{v_1, u_1} C
inst_4 : HasPullbacks.{v_1, u_1} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H :
  Eq (α := pullback s v ⟶ pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)
h₀ :
  Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
    (pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.fst s v :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
    (CategoryStruct.comp (Y := pullback s v)
        (CategoryStruct.comp (Y :=
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
            (Iso.inv (equalizerPullbackMapIso hf hg v) :
              pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
                equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
                  (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
            (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) :
              equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
                  (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
                pullback s v) :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
        (pullback.fst s v : pullback s v ⟶ X) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
h₁ :
  Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    (pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.snd s v :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    (CategoryStruct.comp (Y := pullback s v)
        (CategoryStruct.comp (Y :=
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
            (Iso.inv (equalizerPullbackMapIso hf hg v) :
              pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
                equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
                  (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
            (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) :
              equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
                  (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
                pullback s v) :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
        (pullback.snd s v : pullback s v ⟶ T) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
    (pullback.snd (equalizer.ι f g) (pullback.fst s v) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
    (CategoryStruct.comp (Y :=
        equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (Iso.inv (equalizerPullbackMapIso hf hg v) :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            pullback s v) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)

Tactic:
ext