awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_2 :
  (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
      (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
          (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (Sieve.ofArrows (cylinder f g).X (cylinder f g).f).arrows
⊢ Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (cylinder f g).sieve₀

Tactic:
rw [Sieve.generate_le_iff, PreZeroHypercover.sieve₀]

Premises used: CategoryTheory.PreZeroHypercover.sieve₀, CategoryTheory.Sieve.generate_le_iff
-- 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
Z Y_1 : C
i : E.I₀
v : Z ⟶ E.X i
Y : C
j : F.I₁ (f.s₀ i) (g.s₀ i)
o : Z ⟶ F.Y j
hoo' :
  Eq (α := Z ⟶ pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i))) (o ≫ F.toPullback j)
    (v ≫ pullback.lift (f.h₀ i) (g.h₀ i) ⋯)
⊢ CategoryStruct.comp (Y :=
      pullback (Z := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
        (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.toPullback j))
      (pullback.lift v o ⋯) ((cylinder f g).f (Sigma.mk (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)) i j)) =
    v ≫ E.f i

Tactic:
simp
-- 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
Z Y_1 : C
i : E.I₀
v : Z ⟶ E.X i
Y : C
j : F.I₁ (f.s₀ i) (g.s₀ i)
o : Z ⟶ F.Y j
hoo' :
  Eq (α := Z ⟶ pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i))) (o ≫ F.toPullback j)
    (v ≫ pullback.lift (f.h₀ i) (g.h₀ i) ⋯)
⊢ (Sieve.ofArrows (cylinder f g).X (cylinder f g).f).arrows (v ≫ E.f i)

Tactic:
exact ⟨_, pullback.lift v o hoo'.symm, (cylinder f g).f ⟨i, j⟩, Presieve.ofArrows.mk _,
      by simp⟩
-- 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)
⊢ (cylinder f g).f i ≫ 𝟙 S =
    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)))) ≫
      E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))

Tactic:
simp
-- 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)
⊢ (cylinder f g).f j ≫ 𝟙 S =
    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)))) ≫
      E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))

Tactic:
simp
-- 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)
⊢ Eq (α := Sieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j))) ((cylinder f g).sieve₁' i 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)))))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 : 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)

Tactic:
⟨E.Y k.down, pullback.snd _ _, E.toPullback k.down, Presieve.ofArrows.mk k.down, ?_⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Limits.pullback.snd, CategoryTheory.PreOneHypercover.Y, And.intro, Exists.intro, CategoryTheory.PreOneHypercover.toPullback, ULift.down
-- 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 : C
k : (cylinder f g).I₁ i j
⊢ 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)))) ⋯)
            (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) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      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)))) ⋯)
          (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) ⋯ ⋯))

Tactic:
simp only [cylinder_Y, cylinder_f, toPullback_cylinder, pullback.condition]

Premises used: CategoryTheory.PreOneHypercover.cylinder_f, CategoryTheory.PreOneHypercover.toPullback_cylinder, CategoryTheory.Limits.pullback.condition, CategoryTheory.PreOneHypercover.cylinder_Y
-- 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)))
⊢ 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)
    ((cylinder f g).toPullback { down := k })

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

Premises used: CategoryTheory.Sieve.ofArrows_mk, ULift.up
-- 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)))
e_5 :
  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)))) }

Tactic:
simp [toPullback_cylinder f g ⟨k⟩]

Premises used: CategoryTheory.PreOneHypercover.toPullback_cylinder, ULift.up
-- 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 : (cylinder f g).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)))) ≫
        E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) =
      (cylinder f g).f i

Tactic:
simp
-- 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 : (cylinder f g).I₀
k : (cylinder f g).I₁ i j
⊢ E.p₁ k.down =
    CategoryStruct.comp (Y :=
      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.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
      (pullback.fst (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)))))

Tactic:
simp
-- 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 : (cylinder f g).I₀
k : (cylinder f g).I₁ i j
⊢ E.p₁ k.down =
    CategoryStruct.comp (Y :=
      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.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
      (pullback.fst (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)))))

Tactic:
have : E.p₁ k.down = pullback.lift _ _ (E.w k.down) ≫ pullback.fst _ _ := by simp
-- 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
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
⊢ E.p₂ k.down =
    CategoryStruct.comp (Y :=
      pullback (X := E.X (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
      (pullback.snd (E.f (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))

Tactic:
simp
-- 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
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
⊢ E.p₂ k.down =
    CategoryStruct.comp (Y :=
      pullback (X := E.X (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
      (pullback.snd (E.f (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))

Tactic:
have : E.p₂ k.down = pullback.lift _ _ (E.w k.down) ≫ pullback.snd _ _ := by simp
-- 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
p : (cylinder f g).I₀
⊢ F.p₁ (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.p₁ (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 (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:
simp
-- 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
p : (cylinder f g).I₀
⊢ F.p₁ (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.p₁ (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 (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:
have : F.p₁ p.snd = pullback.lift _ _ (F.w p.2) ≫ pullback.fst _ _ := by simp
-- 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
p : (cylinder f g).I₀
this :
  F.p₁ (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.p₁ (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 (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))))))
nth_rw :
  Eq (α := (cylinder f g).X p ⟶ F.X (PreZeroHypercover.Hom.s₀ (Hom.toHom (Hom.comp (cylinderHom f g) f)) p))
    (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)))) ≫
      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.p₁ (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 (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)))))))
    (PreZeroHypercover.Hom.h₀ (Hom.toHom (Hom.comp (cylinderHom f g) f)) p)
⊢ Eq (α := (cylinder f g).X p ⟶ F.X (PreZeroHypercover.Hom.s₀ (Hom.toHom (Hom.comp (cylinderHom f g) f)) p))
    (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))))
    (PreZeroHypercover.Hom.h₀ (Hom.toHom (Hom.comp (cylinderHom f g) f)) p)

Tactic:
nth_rw 1 [this]