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
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', 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)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i)))) =
    (G.p₁ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) i) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))))

Tactic:
simpa using f.w₁₁ k

Premises used: CategoryTheory.PreOneHypercover.Hom.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 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', 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)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i)))) =
    (G.p₁ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) i) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))))

Tactic:
simpa using g.w₁₁ k

Premises used: CategoryTheory.PreOneHypercover.Hom.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 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', 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)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j)))) =
    (G.p₂ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) j) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))

Tactic:
simpa using f.w₁₂ k

Premises used: CategoryTheory.PreOneHypercover.Hom.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 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', 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)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j)))) =
    (G.p₂ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) j) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', 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₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))

Tactic:
simpa using g.w₁₂ k

Premises used: CategoryTheory.PreOneHypercover.Hom.w₁₂
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
rw :
  Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
    ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂)))
    (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
    ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂)

Tactic:
rw [E.sieve₁'_eq_sieve₁]

Premises used: CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁, CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
    ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂)))
    (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)))

Tactic:
mem₁ _ _ _ _ _ pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
i₁ i₂ : E.I₀
inst_1 : HasPullback (E.f i₁) (E.f i₂)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
    ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂)))
    (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)))

Tactic:
exact mem₁ _ _ _ _ _ pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
inst_2 : E.HasPullbacks
mem₀ : PreZeroHypercover.sieve₀.{u_2, v, u} E.toPreZeroHypercover ∈ (J : (a : C) → Set (Sieve a)) S
mem₁' :
  ∀ (i₁ i₂ : E.I₀),
    Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
      ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂)
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
rw :
  Sieve.pullback (X := Limits.pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) ∈
    (J : (a : C) → Set (Sieve a)) W
⊢ E.sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) W

Tactic:
rw [E.sieve₁_eq_pullback_sieve₁' _ _ w]

Premises used: CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁'
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
inst_2 : E.HasPullbacks
mem₀ : PreZeroHypercover.sieve₀.{u_2, v, u} E.toPreZeroHypercover ∈ (J : (a : C) → Set (Sieve a)) S
mem₁' :
  ∀ (i₁ i₂ : E.I₀),
    Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
      ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂)
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ Sieve.pullback (X := Limits.pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) ∈
    (J : (a : C) → Set (Sieve a)) W

Tactic:
J.pullback_stable' _ (mem₁' i₁ i₂)

Premises used: Set.Mem, CategoryTheory.GrothendieckTopology.pullback_stable'
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
inst_2 : E.HasPullbacks
mem₀ : PreZeroHypercover.sieve₀.{u_2, v, u} E.toPreZeroHypercover ∈ (J : (a : C) → Set (Sieve a)) S
mem₁' :
  ∀ (i₁ i₂ : E.I₀),
    Membership.mem (γ := Set (Sieve.{v, u} (Limits.pullback (E.f i₁) (E.f i₂))))
      ((J : (a : C) → Set (Sieve a)) (Limits.pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂)
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ Sieve.pullback (X := Limits.pullback (E.f i₁) (E.f i₂)) (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) ∈
    (J : (a : C) → Set (Sieve a)) W

Tactic:
exact J.pullback_stable' _ (mem₁' i₁ i₂)

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable'
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
h :
  ∀
    (I :
      Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v, u} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W) (E.sieve₁ p₁ p₂) ⋯)),
    (c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map p₁.op) ≫ F.obj (P := Presheaf.IsSheaf J).map I.f.op =
      (c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map p₂.op) ≫ F.obj (P := Presheaf.IsSheaf J).map I.f.op
⊢ c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map p₁.op = c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map p₂.op

Tactic:
apply F.property.hom_ext ⟨_, E.mem₁ _ _ _ _ w⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
T : C
g : T ⟶ W
j : E.I₁ i₁ i₂
h : T ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
h₁ :
  (c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map p₁.op) ≫ F.obj (P := Presheaf.IsSheaf J).map g.op =
    (c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map p₂.op) ≫ F.obj (P := Presheaf.IsSheaf J).map g.op
⊢ Eq (α :=
    c.pt ⟶
      F.obj (P := Presheaf.IsSheaf J).obj
        (Opposite.op
          (Cover.Arrow.Y (J := J) (S :=
            Subtype.mk (p := fun (S : Sieve.{v, u} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W) (E.sieve₁ p₁ p₂) ⋯)
            { Y := T, f := g, hf := ⋯ })))
    ((c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map p₁.op) ≫
      F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (Cover.Arrow.f { Y := T, f := g, hf := ⋯ })))
    ((c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map p₂.op) ≫
      F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (Cover.Arrow.f { Y := T, f := g, hf := ⋯ })))

Tactic:
dsimp
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
T : C
g : T ⟶ W
j : E.I₁ i₁ i₂
h : T ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
h₁ :
  c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map (h ≫ E.p₁ j).op =
    c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map (h ≫ E.p₂ j).op
⊢ (c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map p₁.op) ≫ F.obj (P := Presheaf.IsSheaf J).map g.op =
    (c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map p₂.op) ≫ F.obj (P := Presheaf.IsSheaf J).map g.op

Tactic:
simp only [assoc, ← Functor.map_comp, ← op_comp, fac₁, fac₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
T : C
g : T ⟶ W
j : E.I₁ i₁ i₂
h : T ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
h₁ :
  c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map (E.p₁ j).op ≫ F.obj (P := Presheaf.IsSheaf J).map h.op =
    c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map (E.p₂ j).op ≫ F.obj (P := Presheaf.IsSheaf J).map h.op
⊢ c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map (h ≫ E.p₁ j).op =
    c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map (h ≫ E.p₂ j).op

Tactic:
simp only [op_comp, Functor.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
T : C
g : T ⟶ W
j : E.I₁ i₁ i₂
h : T ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
⊢ c.ι i₁ ≫ F.obj (P := Presheaf.IsSheaf J).map (E.p₁ j).op ≫ F.obj (P := Presheaf.IsSheaf J).map h.op =
    c.ι i₂ ≫ F.obj (P := Presheaf.IsSheaf J).map (E.p₂ j).op ≫ F.obj (P := Presheaf.IsSheaf J).map h.op

Tactic:
simpa using c.condition ⟨⟨i₁, i₂⟩, j⟩ =≫ F.obj.map h.op

Premises used: Quiver.Hom.op, Prod.mk, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Limits.Multifork.condition, CategoryTheory.Functor.map, Sigma.mk
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
i₀ : E.I₀
⊢ multiforkLift c ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op = c.ι i₀

Tactic:
simp [multiforkLift]

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift
-- 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
J : GrothendieckTopology.{v, u} C
S : C
E : OneHypercover.{u_2, v, u} J S
F : Sheaf.{v, v_1, u, u_1} J A
c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))
m : c.pt ⟶ (E.multifork (F.obj (P := Presheaf.IsSheaf J))).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork (F.obj (P := Presheaf.IsSheaf J))).ι i = c.ι i
apply :
  ∀ (i : E.I₀),
    m ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i).op =
      (fun (c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))) ↦ multiforkLift c) c ≫
        F.obj (P := Presheaf.IsSheaf J).map (E.f i).op
⊢ m = (fun (c : Multifork (E.multicospanIndex (F.obj (P := Presheaf.IsSheaf J)))) ↦ multiforkLift c) c

Tactic:
apply F.property.hom_ext_ofArrows _ E.mem₀

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext_ofArrows