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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      G.map (F.p₁ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        G.map (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    t.ι (f.s₀ b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      G.map (F.p₂ (f.s₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        G.map (f.h₁ (b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op

Tactic:
exact t.condition_assoc ⟨(f.s₀ b.1.1, f.s₀ b.1.2), f.s₁ b.2⟩ _

Premises used: CategoryTheory.PreOneHypercover.Hom.s₁, Prod.mk, Sigma.fst, CategoryTheory.PreOneHypercover.Hom.toHom, Prod.fst, Sigma.mk, CategoryTheory.PreZeroHypercover.Hom.s₀, Sigma.snd, Prod.snd, CategoryTheory.Limits.Multifork.condition_assoc
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
refine_2 : Multifork.IsLimit.lift hE (fun (a : E.I₀) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i
⊢ Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (F.multifork G).ι i =
    t.ι i

Tactic:
simp only [multicospanIndex_left, multicospanShape_L, multifork_ι]

Premises used: CategoryTheory.PreOneHypercover.multifork_ι, CategoryTheory.PreOneHypercover.multicospanShape_L, CategoryTheory.PreOneHypercover.multicospanIndex_left
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
⊢ hgf.a i ≫ F.p₁ (hgf.H i) = (g.comp f).h₀ i

Tactic:
have h1 := hgf.wl i
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = (g.comp f).h₀ i
⊢ Eq (α :=
    t.pt ⟶
      (F.multicospanIndex G).right
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i)))
    (t.ι
        (F.multicospanShape.fst
          (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i)
            (hgf.H i))) ≫
      (F.multicospanIndex G).fst
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i)))
    (t.ι
        (F.multicospanShape.snd
          (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i)
            (hgf.H i))) ≫
      (F.multicospanIndex G).snd
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2) ((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i) (hgf.H i)))

Tactic:
have h2 := t.condition ⟨⟨_, _⟩, hgf.H i⟩
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
refine_2 : t.ι i ≫ G.map ((Hom.id F).h₀ i).op = t.ι i
⊢ Multifork.IsLimit.lift hE (fun (a : E.I₀) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i

Tactic:
rw [← g.w₀, op_comp, Functor.map_comp, ← E.multifork_ι, Multifork.IsLimit.fac_assoc,
      Category.assoc, ← Functor.map_comp, ← op_comp, ← h1, op_comp, Functor.map_comp,
      reassoc_of% h2, ← Functor.map_comp, ← op_comp, hgf.wr i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.PreOneHypercover.multifork_ι, CategoryTheory.PreZeroHypercover.Hom.w₀, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.Limits.Multifork.IsLimit.fac_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.PreOneHypercover.Homotopy.wr
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι i ≫ G.map ((Hom.id F).h₀ i).op = t.ι 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
⊢ m = Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
Multifork.IsLimit.hom_ext hE fun i ↦ ?_

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext, CategoryTheory.PreOneHypercover.multicospanIndex
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
refine_3 :
  ∀ (i : E.multicospanShape.L),
    m ≫ (E.multifork G).ι i =
      Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
        (E.multifork G).ι i
⊢ m = Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
refine Multifork.IsLimit.hom_ext hE fun i ↦ ?_

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- 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
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₂ : m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₃ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i)) ≫ (f.h₀ i).op) = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₄ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i))) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₅ : m ≫ (F.multifork G).ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₆ refine_3₇ : t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i

Tactic:
rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]

Premises used: CategoryTheory.op_comp, CategoryTheory.PreOneHypercover.multifork_ι, CategoryTheory.PreZeroHypercover.Hom.w₀, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.Limits.Multifork.IsLimit.fac, CategoryTheory.Functor.map_comp
-- 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 : E.I₀
k : F.I₁ (f.s₀ i) (g.s₀ i)
⊢ f.h₀ i ≫ F.f (f.s₀ i) = g.h₀ i ≫ F.f (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_1 g_1 f g : E.Hom F
p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
k :
  ULift.{max w w', w}
    (E.I₁ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) (q.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))) ⟶ S)
    (cylinderf f g (p.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ≫ 𝟙 S)
    (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)))) ≫
      E.f (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_1 g_1 f g : E.Hom F
p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
k :
  ULift.{max w w', w}
    (E.I₁ (p.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
⊢ Eq (α := cylinderX f g (q.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ⟶ S)
    (cylinderf f g (q.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))) ≫ 𝟙 S)
    (pullback.fst
        (pullback.lift (f.h₀ (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (q.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
        (F.toPullback (q.snd (β := 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
i j : (cylinder f g).I₀
k : (cylinder f g).I₁ i j
⊢ CategoryStruct.comp (Y := pullback ((cylinder f g).f i) ((cylinder f g).f j)) ((cylinder f g).toPullback k)
      (pullback.fst ((cylinder f g).f i) ((cylinder f g).f j)) =
    pullback.fst
        (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) ⋯) ≫
      pullback.fst ((cylinder f g).f i) ((cylinder f g).f j)

Tactic:
simp [toPullback]

Premises used: CategoryTheory.PreOneHypercover.toPullback
-- 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
⊢ CategoryStruct.comp (Y := pullback ((cylinder f g).f i) ((cylinder f g).f j)) ((cylinder f g).toPullback k)
      (pullback.snd ((cylinder f g).f i) ((cylinder f g).f j)) =
    pullback.fst
        (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) ⋯) ≫
      pullback.snd ((cylinder f g).f i) ((cylinder f g).f j)

Tactic:
simp [toPullback]

Premises used: CategoryTheory.PreOneHypercover.toPullback
-- 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 : E.I₀
⊢ f.h₀ i ≫ F.f (f.s₀ i) = g.h₀ i ≫ F.f (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
⊢ (cylinder f g).sieve₀ =
    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)

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
refine_1 :
  (cylinder f g).sieve₀ ≤
    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)
refine_2 :
  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₀
⊢ (cylinder f g).sieve₀ =
    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)

Tactic:
refine 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
refine_1 :
  Presieve.ofArrows (cylinder f g).X (cylinder f g).f ≤
    (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)).arrows
⊢ (cylinder f g).sieve₀ ≤
    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)

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

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
Y : C
i : (cylinder f g).I₀
⊢ 𝟙 ((cylinder f g).X i) ≫ (cylinder f g).f 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
Y : C
i : (cylinder f g).I₀
refine_1 :
  Sieve.arrows
    (Sieve.pullback (X :=
      pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
        F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
      (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.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (Y := (cylinder f g).X 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)))))
⊢ (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)).arrows
    ((cylinder f g).f i)

Tactic:
refine ⟨_, 𝟙 _, (cylinder f g).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
Y : C
i : (cylinder f g).I₀
refine_1 :
  Sieve.arrows (X :=
    pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
      F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (F.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (Y := (cylinder f g).X i)
    (pullback.snd
        (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)))) ≫
      F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
⊢ Sieve.arrows
    (Sieve.pullback (X :=
      pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
        F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
      (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.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (Y := (cylinder f g).X 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)))))

Tactic:
simp only [Sieve.pullback_apply, pullback.condition]

Premises used: CategoryTheory.Sieve.pullback_apply, CategoryTheory.Limits.pullback.condition
-- 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
Y : C
i : (cylinder f g).I₀
⊢ Sieve.arrows (X :=
    pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
      F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (F.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (Y := (cylinder f g).X i)
    (pullback.snd
        (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)))) ≫
      F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))

Tactic:
Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ _) _

Premises used: CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.Sieve.downward_closed, CategoryTheory.Limits.limit
-- 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
Y : C
i : (cylinder f g).I₀
⊢ Sieve.arrows (X :=
    pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
      F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (F.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (Y := (cylinder f g).X i)
    (pullback.snd
        (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)))) ≫
      F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))

Tactic:
exact Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ _) _

Premises used: CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.Sieve.downward_closed