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
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))))))
⊢ Eq (α := (cylinder f g).X p ⟶ F.X (PreZeroHypercover.Hom.s₀ (Hom.toHom (Hom.comp (cylinderHom f g) f)) p))
    (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.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)

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₀
⊢ Eq (α := E.X (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ⟶ S)
    (f.h₀ (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)))))
    (g.h₀ (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₀
⊢ 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)))))))

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₀
⊢ 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)))))))

Tactic:
have : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) (by simp) ≫
        pullback.snd (F.f _) (F.f _) := 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 :
  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)))))))
dsimp :
  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)))) ≫
      g.h₀ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
⊢ Eq (α := (cylinder f g).X p ⟶ F.X (PreZeroHypercover.Hom.s₀ (Hom.toHom (Hom.comp (cylinderHom f g) g)) 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) g)) p)

Tactic:
dsimp only [cylinder_X, Hom.comp_s₀, cylinder_I₀, Function.comp_apply, cylinderHom_s₀,
      Hom.comp_h₀, cylinderHom_h₀]

Premises used: CategoryTheory.PreOneHypercover.cylinder_X, CategoryTheory.PreOneHypercover.Hom.comp_h₀, CategoryTheory.PreOneHypercover.Hom.comp_s₀, CategoryTheory.PreOneHypercover.cylinder_I₀, Function.comp_apply, CategoryTheory.PreOneHypercover.cylinderHom_s₀, CategoryTheory.PreOneHypercover.cylinderHom_h₀
-- 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 :
  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.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))))))
        (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:
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
⊢ ∃ (W : PreOneHypercover S) (h : W.Hom E), Nonempty (Homotopy (h.comp f) (h.comp g))

Tactic:
⟨cylinder f g, PreOneHypercover.cylinderHom f g, ⟨cylinderHomotopy f g⟩⟩

Premises used: CategoryTheory.PreOneHypercover.cylinder, CategoryTheory.PreOneHypercover.cylinderHom, Nonempty.intro, Exists.intro, CategoryTheory.PreOneHypercover.cylinderHomotopy
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
rw :
  Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := Limits.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) ∈
    (J : (a : C) → Set (Sieve a)) S
⊢ (PreOneHypercover.cylinder f g).sieve₀ ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
rw [PreOneHypercover.sieve₀_cylinder]

Premises used: CategoryTheory.PreOneHypercover.sieve₀_cylinder
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
⊢ Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := Limits.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) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
J.bindOfArrows E.mem₀ fun i ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.bindOfArrows
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
refine :
  ∀ (i : E.I₀),
    Membership.mem (γ := Set (Sieve.{v, u} (E.X i))) ((J : (a : C) → Set (Sieve a)) (E.X i))
      (Sieve.generate
        (Sieve.pullback (X := Limits.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.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := Limits.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) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
refine J.bindOfArrows E.mem₀ fun i ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.bindOfArrows
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i : E.I₀
rw :
  Membership.mem (γ := Set (Sieve.{v, u} (E.X i))) ((J : (a : C) → Set (Sieve a)) (E.X i))
    (Sieve.pullback (X := Limits.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)))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (E.X i))) ((J : (a : C) → Set (Sieve a)) (E.X i))
    (Sieve.generate
      (Sieve.pullback (X := Limits.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)

Tactic:
rw [Sieve.generate_sieve]

Premises used: CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i : E.I₀
⊢ Membership.mem (γ := Set (Sieve.{v, u} (E.X i))) ((J : (a : C) → Set (Sieve a)) (E.X i))
    (Sieve.pullback (X := Limits.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)))

Tactic:
J.pullback_stable _ (mem_sieve₁' F _ _)

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i : E.I₀
⊢ Membership.mem (γ := Set (Sieve.{v, u} (E.X i))) ((J : (a : C) → Set (Sieve a)) (E.X i))
    (Sieve.pullback (X := Limits.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)))

Tactic:
exact J.pullback_stable _ (mem_sieve₁' F _ _)

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
rw :
  Membership.mem (γ :=
    Set (Sieve.{v, u} (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))))
    ((J : (a : C) → Set (Sieve a))
      (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j)))
    (Sieve.pullback (X :=
      Limits.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 ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.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)))))
⊢ Membership.mem (γ :=
    Set (Sieve.{v, u} (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))))
    ((J : (a : C) → Set (Sieve a))
      (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j)))
    ((PreOneHypercover.cylinder f g).sieve₁' i j)

Tactic:
rw [PreOneHypercover.sieve₁'_cylinder]

Premises used: CategoryTheory.PreOneHypercover.sieve₁'_cylinder
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
⊢ Membership.mem (γ :=
    Set (Sieve.{v, u} (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))))
    ((J : (a : C) → Set (Sieve a))
      (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j)))
    (Sieve.pullback (X :=
      Limits.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 ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.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:
J.pullback_stable _ (mem_sieve₁' E _ _)

Premises used: Set.Mem, CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
⊢ Membership.mem (γ :=
    Set (Sieve.{v, u} (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))))
    ((J : (a : C) → Set (Sieve a))
      (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j)))
    (Sieve.pullback (X :=
      Limits.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 ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.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:
exact J.pullback_stable _ (mem_sieve₁' E _ _)

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{w, v, u} J S
F : OneHypercover.{w', v, u} J S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
⊢ ∃ (W : J.OneHypercover S) (h : W.Hom E), Nonempty (Homotopy (Hom.comp h f) (Hom.comp h g))

Tactic:
⟨cylinder f g, PreOneHypercover.cylinderHom f g, ⟨PreOneHypercover.cylinderHomotopy f g⟩⟩

Premises used: CategoryTheory.PreOneHypercover.cylinderHom, Nonempty.intro, Exists.intro, CategoryTheory.GrothendieckTopology.OneHypercover.cylinder, CategoryTheory.PreOneHypercover.cylinderHomotopy
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E F : OneHypercover.{u_1, v, u} J S
f g : E ⟶ F
H : Homotopy f g
⊢ (toHOneHypercover J S).map f = (toHOneHypercover J S).map g

Tactic:
Quotient.sound _ ⟨H⟩

Premises used: Nonempty.intro, CategoryTheory.Quotient.sound
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
⊢ Nonempty (HOneHypercover.{v, u, u_1} J S)

Tactic:
⟨⟨Nonempty.some inferInstance⟩⟩

Premises used: inferInstance, Nonempty.some, Nonempty.intro, CategoryTheory.Quotient.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
f g : X ⟶ Y
obtain :
  ∀ (f : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)),
    ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X), h ≫ (toHOneHypercover J S).map f = h ≫ g
⊢ ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X), h ≫ f = h ≫ g

Tactic:
obtain ⟨(f : X.1 ⟶ Y.1), rfl⟩ := (toHOneHypercover J S).map_surjective f

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover, CategoryTheory.Quotient.as, rfl, CategoryTheory.Functor.map_surjective