-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
p : (cylinder f g).I₀
this :
  Eq (α :=
    E.X (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ⟶
      F.X (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
    (CategoryStruct.comp (Y :=
      pullback (X := F.X (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
        F.X (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
      (pullback.lift (f.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
      (pullback.snd (F.f (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))))
⊢ Eq (α :=
    cylinderX f g (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ⟶
      F.X (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (pullback.snd
        (pullback.lift (f.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
        (F.toPullback (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ≫
      F.p₂ (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
    (pullback.fst
        (pullback.lift (f.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
        (F.toPullback (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ≫
      CategoryStruct.comp (Y :=
        pullback (X := F.X (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
          F.X (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (F.f (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (F.f (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
        (pullback.lift (f.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
        (pullback.snd (F.f (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (F.f (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))))
have rw : Eq (α :=
  cylinderX f g (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ⟶
    F.X (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
  (pullback.snd
      (pullback.lift (f.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
      (F.toPullback (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ≫
    F.p₂ (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
  (pullback.snd
      (pullback.lift (f.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
      (F.toPullback (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ≫
    CategoryStruct.comp (Y :=
      pullback (X := F.X (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
        F.X (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
      (F.toPullback (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (pullback.snd (F.f (f.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))))
Tactic: rw [pullback.condition_assoc]