-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
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)
⊢ 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)
have 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) sorry sorry)
            (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry))
          (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) sorry sorry)
                (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry))
          (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry) (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) :
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
                (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) ⟶
              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)
Tactic: ext