-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
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_1 g_1 f g : E.Hom F
x x_1 : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
k :
  ULift.{max w w', w}
    (E.I₁ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
      (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
⊢ Eq (α :=
    pullback (X :=
        pullback (X := cylinderX f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
          cylinderX f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (Z :=
        pullback (X := E.X (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
          E.X (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.map (cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (pullback.fst
            (pullback.lift (f.h₀ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
              (g.h₀ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
            (F.toPullback (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (pullback.fst
            (pullback.lift (f.h₀ (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
              (g.h₀ (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
            (F.toPullback (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ⟶
      S)
    ((pullback.fst
          (pullback.map (cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (E.f (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (E.f (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (pullback.fst
              (pullback.lift (f.h₀ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
                (g.h₀ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
              (F.toPullback (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
            (pullback.fst
              (pullback.lift (f.h₀ (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
                (g.h₀ (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
              (F.toPullback (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
            (𝟙 S) ⋯ ⋯)
          (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
        pullback.fst (cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) ≫
      cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
    ((pullback.fst
          (pullback.map (cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (E.f (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (E.f (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (pullback.fst
              (pullback.lift (f.h₀ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
                (g.h₀ (x.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
              (F.toPullback (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
            (pullback.fst
              (pullback.lift (f.h₀ (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
                (g.h₀ (x_1.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
              (F.toPullback (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
            (𝟙 S) ⋯ ⋯)
          (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
        pullback.snd (cylinderf f g (x.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) ≫
      cylinderf f g (x_1.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition