-- 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
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y : C
k : (cylinder f g).I₁ i j
⊢ Sieve.arrows (X := pullback ((cylinder f g).f i) ((cylinder f g).f j))
    (Sieve.pullback (X :=
      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.sieve₁' (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)))))
    ((cylinder f g).toPullback k)
have refine_1 : Eq (α :=
  (cylinder f g).Y k ⟶
    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.snd
      (pullback.map (cylinderf f g (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (cylinderf f g (j.snd (β := 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.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)))) sorry)
          (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)))) sorry)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) sorry sorry)
      (pullback.lift (E.p₁ k.down) (E.p₂ k.down) sorry) ≫
    E.toPullback k.down)
  (CategoryStruct.comp (Y := pullback ((cylinder f g).f i) ((cylinder f g).f j)) ((cylinder f g).toPullback k)
    (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)))) sorry)
        (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)))) sorry)
        (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (𝟙 S) sorry sorry))
Tactic: refine ⟨E.Y k.down, pullback.snd _ _, E.toPullback k.down, Presieve.ofArrows.mk k.down, ?_⟩