-- 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 g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y_1 Y : C
k : E.I₁ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
h :
  pullback (X := pullback ((cylinder f g).f i) ((cylinder f g).f j)) (Z :=
        pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
          E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
          (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (pullback.fst
            (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
              (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
            (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (pullback.fst
            (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
              (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
            (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (𝟙 S) ⋯ ⋯)
        (E.toPullback k) =
      (cylinder f g).Y
        { down := k :
          ULift.{max w w', w}
            (E.I₁ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
              (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) } →
    pullback.fst
        (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
          (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (pullback.fst
            (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
              (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
            (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (pullback.fst
            (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
              (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
            (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
          (𝟙 S) ⋯ ⋯)
        (E.toPullback k) =
      (cylinder f g).toPullback
        { down := k :
          ULift.{max w w', w}
            (E.I₁ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
              (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) }
⊢ Sieve.arrows (X := pullback ((cylinder f g).f i) ((cylinder f g).f j))
    (Sieve.ofArrows (cylinder f g).Y fun (j_1 : (cylinder f g).I₁ i j) ↦ (cylinder f g).toPullback j_1) (Y :=
    pullback (X := pullback ((cylinder f g).f i) ((cylinder f g).f j)) (Z :=
      pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) ⋯ ⋯)
      (E.toPullback k))
    (pullback.fst
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) ⋯ ⋯)
      (E.toPullback k))

Tactic:
convert! Sieve.ofArrows_mk _ _ (ULift.up k)

Premises used: CategoryTheory.Sieve.ofArrows_mk, ULift.up