awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
x x_1 : (E.sigmaOfIsColimit hc).I₀
x_2 : PUnit.{w + 1}
⊢ ∀ (i : E.I₁'),
    d.inj i ≫
        (Cofan.IsColimit.desc hd fun (i : E.I₁') ↦
            E.p₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj i.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
          (E.sigmaOfIsColimit hc).f x =
      d.inj i ≫
        (Cofan.IsColimit.desc hd fun (i : E.I₁') ↦
            E.p₂ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj i.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
          (E.sigmaOfIsColimit hc).f x_1

Tactic:
simp [E.w]

Premises used: CategoryTheory.PreOneHypercover.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
i : E.I₁'
a b : PUnit.{w + 1}
r : (E.sigmaOfIsColimit hc hd).I₁ a b
⊢ d.inj i ≫ (E.sigmaOfIsColimit hc hd).p₁ r =
    E.p₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫ c.inj i.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1

Tactic:
simp [sigmaOfIsColimit]

Premises used: CategoryTheory.PreOneHypercover.sigmaOfIsColimit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
i : E.I₁'
a b : PUnit.{w + 1}
r : (E.sigmaOfIsColimit hc hd).I₁ a b
⊢ d.inj i ≫ (E.sigmaOfIsColimit hc hd).p₂ r =
    E.p₂ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫ c.inj i.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2

Tactic:
simp [sigmaOfIsColimit]

Premises used: CategoryTheory.PreOneHypercover.sigmaOfIsColimit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
⊢ ((E.sigmaOfIsColimit hc hd).multifork F).pt ≅
    Cone.pt.{w, v_1, w, u_1} (J := WalkingMulticospan (E.sigmaOfIsColimit hc hd).multicospanShape)
      (Functor.obj
        (Equivalence.functor
          (Equivalence.symm
            (MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map
                (Quiver.Hom.op
                  (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                    E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                      c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)))
              (F.map
                (Quiver.Hom.op
                  (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                    E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                      c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))))
        (E.forkOfIsColimit hc hd F))

Tactic:
exact .refl _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i ≅
      MulticospanIndex.left
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape (X := F.obj (op c.pt))
          (F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)))
          (F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))
        i

Tactic:
exact fun _ ↦ .refl _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i ≅
      MulticospanIndex.right
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape (X := F.obj (op c.pt))
          (F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)))
          (F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))
        i

Tactic:
exact fun _ ↦ .refl _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E : PreOneHypercover.{w, v, u} S_1
S : C
x x_1 : PreZeroHypercover.I₀.{w, v, u} (PreZeroHypercover.singleton (𝟙 S))
x_2 : PUnit.{w + 1}
⊢ 𝟙 S ≫ PreZeroHypercover.f (PreZeroHypercover.singleton (𝟙 S)) x =
    𝟙 S ≫ PreZeroHypercover.f (PreZeroHypercover.singleton (𝟙 S)) x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
⊢ Eq (α := Sieve.{v, u} S) (Sieve.generate (PreZeroHypercover.presieve₀.{u_2, v, u} (toPreZeroHypercover (trivial S))))
    ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S W : C
p : W ⟶ S
h :
  ∀ ⦃Y : C⦄ (f : Y ⟶ W),
    Sieve.arrows (sieve₁ (trivial S) (i₁ := PUnit.unit) (i₂ := PUnit.unit) p p) f ↔ Sieve.arrows ⊤ f
⊢ Eq (α := Sieve.{v, u} W) (sieve₁ (trivial S) (i₁ := PUnit.unit) (i₂ := PUnit.unit) p p) ⊤

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S W : C
p : W ⟶ S
Y : C
f : Y ⟶ W
⊢ Sieve.arrows (sieve₁ (trivial S) (i₁ := PUnit.unit) (i₂ := PUnit.unit) p p) f ↔ Sieve.arrows ⊤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
⊢ Nonempty (PreOneHypercover.{w, v, u} S)

Tactic:
⟨trivial S⟩

Premises used: Nonempty.intro, CategoryTheory.PreOneHypercover.trivial
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 : PreOneHypercover.{w, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread.0.I₀
k : Prod.{u_2, u_3} (E.I₁ i.1 j.1) (F.I₁ i.2 j.2)
⊢ (E.p₁ k.1 ≫ E.f i.1) ≫ 𝟙 S =
    E.p₁ k.1 ≫
      E.f
        (Sigma.fst (β := fun (i : E.I₀) ↦
          PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
            ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
          ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
              (a : E.I₀ × F.toPreZeroHypercover.1) →
                (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
            i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 : PreOneHypercover.{w, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread.0.I₀
k : Prod.{u_2, u_3} (E.I₁ i.1 j.1) (F.I₁ i.2 j.2)
⊢ (F.p₁ k.2 ≫ F.f i.2) ≫ 𝟙 S =
    F.p₁ k.2 ≫
      F.f
        (Sigma.snd (β := fun (i : E.I₀) ↦
          PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
            ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
          ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
              (a : E.I₀ × F.toPreZeroHypercover.1) →
                (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
            i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 : PreOneHypercover.{w, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread.0.I₀
k : Prod.{u_2, u_3} (E.I₁ i.1 j.1) (F.I₁ i.2 j.2)
⊢ (E.p₁ k.1 ≫ E.f i.1) ≫ 𝟙 S =
    E.p₂ k.1 ≫
      E.f
        (Sigma.fst (β := fun (i : E.I₀) ↦
          PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
            ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
          ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
              (a : E.I₀ × F.toPreZeroHypercover.1) →
                (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
            j))

Tactic:
simp [E.w]

Premises used: CategoryTheory.PreOneHypercover.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 : PreOneHypercover.{w, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread.0.I₀
k : Prod.{u_2, u_3} (E.I₁ i.1 j.1) (F.I₁ i.2 j.2)
⊢ (F.p₁ k.2 ≫ F.f i.2) ≫ 𝟙 S =
    F.p₂ k.2 ≫
      F.f
        (Sigma.snd (β := fun (i : E.I₀) ↦
          PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
            ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
          ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
              (a : E.I₀ × F.toPreZeroHypercover.1) →
                (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
            j))

Tactic:
simp [F.w]

Premises used: CategoryTheory.PreOneHypercover.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 : PreOneHypercover.{w, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
⊢ ∀ ⦃i₁ i₂ : (PreZeroHypercover.inter.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).I₀⦄
    (j : Prod.{u_2, u_3} (E.I₁ i₁.1 i₂.1) (F.I₁ i₁.2 i₂.2)),
    Eq (α := pullback (E.p₁ j.1 ≫ E.f i₁.1) (F.p₁ j.2 ≫ F.f i₁.2) ⟶ S)
      (pullback.map (E.p₁ j.1 ≫ E.f i₁.1) (F.p₁ j.2 ≫ F.f i₁.2)
          (E.f
            (Sigma.fst (β := fun (i : E.I₀) ↦
              PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
                ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
              ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                  (a : E.I₀ × F.toPreZeroHypercover.1) →
                    (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
                i₁)))
          (F.f
            (Sigma.snd (β := fun (i : E.I₀) ↦
              PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
                ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
              ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                  (a : E.I₀ × F.toPreZeroHypercover.1) →
                    (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
                i₁)))
          (E.p₁ j.1) (F.p₁ j.2) (𝟙 S) ⋯ ⋯ ≫
        (PreZeroHypercover.inter.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).f i₁)
      (pullback.map (E.p₁ j.1 ≫ E.f i₁.1) (F.p₁ j.2 ≫ F.f i₁.2)
          (E.f
            (Sigma.fst (β := fun (i : E.I₀) ↦
              PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
                ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
              ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                  (a : E.I₀ × F.toPreZeroHypercover.1) →
                    (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
                i₂)))
          (F.f
            (Sigma.snd (β := fun (i : E.I₀) ↦
              PreZeroHypercover.I₀.{u_3, v, u} (C := C) (S := E.X i)
                ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_3, v, u} (E.f i) F.toPreZeroHypercover) i))
              ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                  (a : E.I₀ × F.toPreZeroHypercover.1) →
                    (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
                i₂)))
          (E.p₂ j.1) (F.p₂ j.2) (𝟙 S) ⋯ ⋯ ≫
        (PreZeroHypercover.inter.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).f i₂)

Tactic:
simp [E.w]

Premises used: CategoryTheory.PreOneHypercover.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
h :
  ∀ ⦃Y : C⦄ (f : Y ⟶ W),
    ((E.inter F).sieve₁ p₁ p₂).arrows f ↔
      (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
            fun (x : C) (f : x ⟶ W)
              (x_1 :
                (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
            Sieve.pullback f
              (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
        f
⊢ (E.inter F).sieve₁ p₁ p₂ =
    Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
      fun (x : C) (f : x ⟶ W)
        (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))

Tactic:
ext Y f

Premises used: CategoryTheory.PreOneHypercover.Y
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f ↔
    (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun (x : C) (f : x ⟶ W)
            (x_1 :
              (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f

Tactic:
⟨fun ⟨k, a, h₁, h₂⟩ ↦ ?_, fun ⟨Z, a, b, ⟨k, e, h₁, h₂⟩, ⟨l, u, u₁, u₂⟩, hab⟩ ↦ ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.PreOneHypercover.toPreZeroHypercover, CategoryTheory.Sieve.bind, CategoryTheory.Sieve.arrows, _private.0.CategoryTheory.PreOneHypercover.sieve₁_inter.match_1, Prod.fst, _private.0.CategoryTheory.PreOneHypercover.sieve₁_inter.match_2, CategoryTheory.Limits.pullback.fst, Iff.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.PreOneHypercover.sieve₁, CategoryTheory.Sieve.pullback, Prod.snd, CategoryTheory.PreOneHypercover.inter
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
h :
  ((E.inter F).sieve₁ p₁ p₂).arrows f →
    ∀ (k : (E.inter F).I₁ i j) (a : Y ⟶ (E.inter F).Y k) (h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k)
      (h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k),
      (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
            fun (x : C) (f : x ⟶ W)
              (x_1 :
                (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
            Sieve.pullback f
              (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
        f
h₁ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun (x : C) (f : x ⟶ W)
            (x_1 :
              (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f →
    ∀ (Z : C) (a : Y ⟶ Z) (b : Z ⟶ W) (k : E.I₁ i.1 j.1) (e : Z ⟶ E.Y k)
      (h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k)
      (h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k) (l : F.I₁ i.2 j.2) (u : Y ⟶ F.Y l)
      (u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l)
      (u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l) (hab : a ≫ b = f),
      ((E.inter F).sieve₁ p₁ p₂).arrows f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f ↔
    (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun (x : C) (f : x ⟶ W)
            (x_1 :
              (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f

Tactic:
refine ⟨fun ⟨k, a, h₁, h₂⟩ ↦ ?_, fun ⟨Z, a, b, ⟨k, e, h₁, h₂⟩, ⟨l, u, u₁, u₂⟩, hab⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
h : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    f

Tactic:
⟨pullback p ((E.inter F).toPullback k), pullback.lift f a ?_,
        pullback.fst _ _, ?_, ?_, ?_⟩

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.lift, CategoryTheory.Presieve.bind, And.intro, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.PreOneHypercover.toPullback, CategoryTheory.PreOneHypercover.inter