-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (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 : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ Eq (α :=
    pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
      pullback s (𝒰.f i))
    (pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) :
      pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
        pullback s (𝒰.f i))
    (CategoryStruct.comp (Y :=
        equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
          (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
          (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
        (Iso.inv (equalizerPullbackMapIso hf hg (𝒰.f i)) :
          pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
            equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
              (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
            (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) :
          equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
              (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) ⟶
            pullback s (𝒰.f i)) :
      pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
        pullback s (𝒰.f i))
have h₀ : Eq (α := pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ X)
  (pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ≫ pullback.fst s (𝒰.f i) :
    pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ X)
  (CategoryStruct.comp (Y := pullback s (𝒰.f i))
      (CategoryStruct.comp (Y :=
          equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
            (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
            (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry))
          (Iso.inv (equalizerPullbackMapIso hf hg (𝒰.f i)) :
            pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
              equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
                (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
                (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry))
          (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry) :
            equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
                (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
                (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry) ⟶
              pullback s (𝒰.f i)) :
        pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
          pullback s (𝒰.f i))
      (pullback.fst s (𝒰.f i) : pullback s (𝒰.f i) ⟶ X) :
    pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ X)
Tactic: ext