-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} 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
h₀ :
  Eq (α :=
    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) ⋯ ⋯) ⟶
      X)
    (CategoryStruct.comp (Y := pullback s v)
        (CategoryStruct.comp (Y :=
            pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
            (Iso.hom (equalizerPullbackMapIso hf hg 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) ⋯ ⋯) ⟶
                pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst 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) :
          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.fst s v : pullback s v ⟶ X) :
      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) ⋯ ⋯) ⟶
        X)
    (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ 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) ⋯ ⋯) ⟶
        X)
⊢ Eq (α :=
    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)
    (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (Iso.hom (equalizerPullbackMapIso hf hg 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) ⋯ ⋯) ⟶
            pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst 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) :
      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)
    (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)
have h₁ : Eq (α :=
  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) ⟶
    T)
  (CategoryStruct.comp (Y := pullback s v)
      (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
          (Iso.hom (equalizerPullbackMapIso hf hg 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) ⟶
              pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst 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) :
        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.snd s v : pullback s v ⟶ T) :
    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) ⟶
      T)
  (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry) (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) ≫ pullback.snd 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) ⟶
      T)
Tactic: ext