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
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
i₀ : E.I₀
dsimp :
  m ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op =
    multiforkLift c ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op
⊢ 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

Tactic:
dsimp only
-- 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
i₀ : E.I₀
rw : m ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op = c.ι i₀
⊢ m ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op =
    multiforkLift c ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op

Tactic:
rw [multiforkLift_map]

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map
-- 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
i₀ : E.I₀
⊢ m ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op = c.ι i₀

Tactic:
hm i₀

Premises used: CategoryTheory.Limits.Multifork.ι
-- 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
i₀ : E.I₀
⊢ m ≫ F.obj (P := Presheaf.IsSheaf J).map (E.f i₀).op = c.ι i₀

Tactic:
exact hm i₀
-- 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_1 S : C
⊢ PreZeroHypercover.sieve₀.{w, v, u} (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
simp only [PreOneHypercover.sieve₀_trivial, J.top_mem]

Premises used: CategoryTheory.GrothendieckTopology.top_mem, CategoryTheory.PreOneHypercover.sieve₀_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
J : GrothendieckTopology.{v, u} C
S_1 S : C
x x_1 : PreZeroHypercover.I₀.{w, v, u} (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S))
x_2 : C
x_3 : x_2 ⟶ PreZeroHypercover.X (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x
x_4 : x_2 ⟶ PreZeroHypercover.X (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x_1
h :
  x_3 ≫ PreZeroHypercover.f (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x =
    x_4 ≫ PreZeroHypercover.f (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x_1
⊢ x_3 = x_4

Tactic:
simp only [PreOneHypercover.trivial_toPreZeroHypercover, PreZeroHypercover.singleton_X,
      PreZeroHypercover.singleton_f, Category.comp_id] at h

Premises used: CategoryTheory.PreZeroHypercover.singleton_X, CategoryTheory.PreOneHypercover.trivial_toPreZeroHypercover, CategoryTheory.Category.comp_id, CategoryTheory.PreZeroHypercover.singleton_f
-- 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_1 S : C
x x_1 : PreZeroHypercover.I₀.{w, v, u} (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S))
x_2 : C
x_3 : x_2 ⟶ PreZeroHypercover.X (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x
x_4 : x_2 ⟶ PreZeroHypercover.X (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x_1
h : x_3 = x_4
subst : PreOneHypercover.sieve₁ (PreOneHypercover.trivial S) x_3 x_3 ∈ (J : (a : C) → Set (Sieve a)) x_2
⊢ PreOneHypercover.sieve₁ (PreOneHypercover.trivial S) x_3 x_4 ∈ (J : (a : C) → Set (Sieve a)) x_2

Tactic:
subst h
-- 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_1 S : C
x x_1 : PreZeroHypercover.I₀.{w, v, u} (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S))
x_2 : C
x_3 : x_2 ⟶ PreZeroHypercover.X (PreOneHypercover.toPreZeroHypercover (PreOneHypercover.trivial S)) x
⊢ PreOneHypercover.sieve₁ (PreOneHypercover.trivial S) x_3 x_3 ∈ (J : (a : C) → Set (Sieve a)) x_2

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
J : GrothendieckTopology.{v, u} C
S_1 S : C
⊢ Nonempty (OneHypercover.{u_2, v, u} J S)

Tactic:
⟨trivial J S⟩

Premises used: Nonempty.intro, CategoryTheory.GrothendieckTopology.OneHypercover.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
J : GrothendieckTopology.{v, u} C
S : C
inst_2 : HasPullbacks.{v, u} C
E : OneHypercover.{u_2, v, u} J S
F : OneHypercover.{u_3, v, u} J S
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_4 : ∀ (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₂ : (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₁
p₂ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₂
h :
  p₁ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₁ =
    p₂ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₂
rw :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.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 i₂.1) (F.f i₂.2))).arrows f) ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)))) ∈
    (J : (a : C) → Set (Sieve a)) W
⊢ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).sieve₁ p₁ p₂ ∈
    (J : (a : C) → Set (Sieve a)) W

Tactic:
rw [PreOneHypercover.sieve₁_inter h]

Premises used: CategoryTheory.PreOneHypercover.sieve₁_inter
-- 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
inst_2 : HasPullbacks.{v, u} C
E : OneHypercover.{u_2, v, u} J S
F : OneHypercover.{u_3, v, u} J S
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_4 : ∀ (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₂ : (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₁
p₂ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₂
h :
  p₁ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₁ =
    p₂ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₂
⊢ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) ≫ E.f i₁.1 = (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2)) ≫ E.f i₂.1

Tactic:
simpa using h
-- 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
inst_2 : HasPullbacks.{v, u} C
E : OneHypercover.{u_2, v, u} J S
F : OneHypercover.{u_3, v, u} J S
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_4 : ∀ (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₂ : (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₁
p₂ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₂
h :
  p₁ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₁ =
    p₂ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₂
refine :
  ∀ (x : C) (x_1 : x ⟶ W),
    (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows x_1 →
      Sieve.pullback x_1
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2))) ∈
        (J : (a : C) → Set (Sieve a)) x
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.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 i₂.1) (F.f i₂.2))).arrows f) ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)))) ∈
    (J : (a : C) → Set (Sieve a)) W

Tactic:
refine J.bind_covering (E.mem₁ _ _ _ _ (by simpa using h)) fun _ _ _ ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.bind_covering, 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
inst_2 : HasPullbacks.{v, u} C
E : OneHypercover.{u_2, v, u} J S
F : OneHypercover.{u_3, v, u} J S
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_4 : ∀ (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₂ : (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₁
p₂ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₂
h :
  p₁ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₁ =
    p₂ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₂
x : C
x_1 : x ⟶ W
h_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows x_1
⊢ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) ≫ F.f i₁.2 = (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)) ≫ F.f i₂.2

Tactic:
simpa [Category.assoc, ← pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- 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
inst_2 : HasPullbacks.{v, u} C
E : OneHypercover.{u_2, v, u} J S
F : OneHypercover.{u_3, v, u} J S
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_4 : ∀ (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₂ : (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₁
p₂ : W ⟶ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).X i₂
h :
  p₁ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₁ =
    p₂ ≫ (PreOneHypercover.inter.{v, u, u_2, u_3} E.toPreOneHypercover F.toPreOneHypercover).f i₂
x : C
x_1 : x ⟶ W
h_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows x_1
⊢ Sieve.pullback x_1 (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2))) ∈
    (J : (a : C) → Set (Sieve a)) x

Tactic:
exact J.pullback_stable _
      (F.mem₁ _ _ _ _ (by simpa [Category.assoc, ← pullback.condition]))

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.preOneHypercover.sieve₀.arrows f ↔ (↑S : Sieve X).arrows f
⊢ S.preOneHypercover.sieve₀ = (↑S : Sieve X)

Tactic:
ext Y f
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
h : S.preOneHypercover.sieve₀.arrows f → (↑S : Sieve X).arrows f
h₁ : (↑S : Sieve X).arrows f → S.preOneHypercover.sieve₀.arrows f
⊢ S.preOneHypercover.sieve₀.arrows f ↔ (↑S : Sieve X).arrows f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
Y_1 Y : C
g : S.preOneHypercover.I₀
w : Y_1 ⟶ S.preOneHypercover.X g
⊢ (↑S : Sieve X).arrows (w ≫ S.preOneHypercover.f g)

Tactic:
S.1.downward_closed g.hf _

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
Y_1 Y : C
g : S.preOneHypercover.I₀
w : Y_1 ⟶ S.preOneHypercover.X g
⊢ (↑S : Sieve X).arrows (w ≫ S.preOneHypercover.f g)

Tactic:
exact S.1.downward_closed g.hf _

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
hf : (↑S : Sieve X).arrows f
⊢ S.preOneHypercover.sieve₀.arrows f

Tactic:
Sieve.ofArrows_mk _ _ ({ hf := hf, .. } : S.Arrow)

Premises used: CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
hf : (↑S : Sieve X).arrows f
⊢ S.preOneHypercover.sieve₀.arrows f

Tactic:
exact Sieve.ofArrows_mk _ _ ({ hf := hf, .. } : S.Arrow)

Premises used: CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
h : ∀ ⦃Y : C⦄ (f : Y ⟶ W), (S.preOneHypercover.sieve₁ p₁ p₂).arrows f ↔ Sieve.arrows ⊤ f
⊢ S.preOneHypercover.sieve₁ p₁ p₂ = ⊤

Tactic:
ext Y f
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
h : (S.preOneHypercover.sieve₁ p₁ p₂).arrows f
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f ↔ Sieve.arrows ⊤ f

Tactic:
simp only [Sieve.top_apply, iff_true]

Premises used: CategoryTheory.Sieve.top_apply, iff_true
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f

Tactic:
⟨{ w := w, .. }, f, rfl, rfl⟩

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f

Tactic:
exact ⟨{ w := w, .. }, f, rfl, rfl⟩
-- 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
X : C
S : J.Cover X
⊢ S.preOneHypercover.sieve₀ ∈ (J : (a : C) → Set (Sieve a)) X

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
J : GrothendieckTopology.{v, u} C
X : C
S : J.Cover X
f₁ f₂ : S.preOneHypercover.I₀
x : C
p₁ : x ⟶ S.preOneHypercover.X f₁
p₂ : x ⟶ S.preOneHypercover.X f₂
w : p₁ ≫ S.preOneHypercover.f f₁ = p₂ ≫ S.preOneHypercover.f f₂
⊢ S.preOneHypercover.sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) x

Tactic:
simp [S.preOneHypercover_sieve₁ f₁ f₂ p₁ p₂ w]

Premises used: CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, u_2, u, u_2 + 1} Cᵒᵖ (Type u_2)
S : C
E : PreZeroHypercover.{u_3, v, u} S
h : Presieve.IsSeparatedFor P E.presieve₀
x y : P.obj (Opposite.op S)
hi :
  ∀ (i : E.I₀),
    Eq (α := (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (E.X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (E.f i).op) :
            (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op S))) →
              (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (E.X i))))
          x :
        (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (E.X i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (E.f i).op) :
            (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op S))) →
              (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (E.X i))))
          y :
        (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (E.X i))))
⊢ x = y

Tactic:
h.ext fun _ _ ⟨i⟩ ↦ hi i

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, _private.0.CategoryTheory.PreZeroHypercover.ext_of_isSeparatedFor.match_1, Eq, DFunLike.coe
-- 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 : PreZeroHypercover.{u_2, v, u} S
inst_2 dsimp : E.HasPullbacks
⊢ E.toPreOneHypercover.HasPullbacks

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
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_2 : E.HasPullbacks
⊢ E.HasPullbacks

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
rw :
  LE.le (α := Sieve.{v, u} (pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j))) ⊤
    (E.toPreOneHypercover.sieve₁' i j)
⊢ Eq (α := Sieve.{v, u} (pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)))
    (E.toPreOneHypercover.sieve₁' i j) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
_ : Sieve.arrows ⊤ f → Sieve.arrows (E.toPreOneHypercover.sieve₁' i j) f
⊢ Sieve.arrows ⊤ f → Sieve.arrows (E.toPreOneHypercover.sieve₁' i j) f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
⊢ f ≫ 𝟙 (pullback (E.f i) (E.f j)) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
refine :
  Presieve.ofArrows.{v, u, u_2} E.toPreOneHypercover.Y
    (fun (j_1 : E.toPreOneHypercover.I₁ i j) ↦ E.toPreOneHypercover.toPullback j_1) (𝟙 (pullback (E.f i) (E.f j)))
⊢ Sieve.arrows (E.toPreOneHypercover.sieve₁' i j) f

Tactic:
refine ⟨pullback (E.f i) (E.f j), f, 𝟙 _, ?_, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
⊢ Presieve.ofArrows.{v, u, u_2} E.toPreOneHypercover.Y
    (fun (j_1 : E.toPreOneHypercover.I₁ i j) ↦ E.toPreOneHypercover.toPullback j_1) (𝟙 (pullback (E.f i) (E.f j)))

Tactic:
Presieve.ofArrows.mk' ⟨⟩ rfl ?_

Premises used: CategoryTheory.Presieve.ofArrows.mk', PUnit.unit, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
refine : 𝟙 (pullback (E.f i) (E.f j)) = eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit
⊢ Presieve.ofArrows.{v, u, u_2} E.toPreOneHypercover.Y
    (fun (j_1 : E.toPreOneHypercover.I₁ i j) ↦ E.toPreOneHypercover.toPullback j_1) (𝟙 (pullback (E.f i) (E.f j)))

Tactic:
refine Presieve.ofArrows.mk' ⟨⟩ rfl ?_

Premises used: CategoryTheory.Presieve.ofArrows.mk', rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
h₀ :
  𝟙 (pullback (E.f i) (E.f j)) ≫ pullback.fst (E.f i) (E.f j) =
    CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit)
      (pullback.fst (E.f i) (E.f j))
h₁ :
  𝟙 (pullback (E.f i) (E.f j)) ≫ pullback.snd (E.f i) (E.f j) =
    CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit)
      (pullback.snd (E.f i) (E.f j))
⊢ 𝟙 (pullback (E.f i) (E.f j)) = eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
⊢ 𝟙 (pullback (E.f i) (E.f j)) ≫ pullback.fst (E.f i) (E.f j) =
    CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit)
      (pullback.fst (E.f i) (E.f j))

Tactic:
simp [PreOneHypercover.toPullback]

Premises used: CategoryTheory.PreOneHypercover.toPullback