awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑T.uncurry : Type (max u v))
dsimp :
  YT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯ ≅
    (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)
⊢ E.X (Sum.inr i) ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) (Sum.inr i))

Tactic:
dsimp [E, F]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑T.uncurry : Type (max u v))
⊢ YT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯ ≅
    (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)

Tactic:
apply eT
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i : E.I₀
⊢ E.X i ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i)

Tactic:
match i with
      | .inl i => dsimp [E, F]; symm; exact eR _ _
      | .inr i => dsimp [E, F]; apply eT
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
Precoverage.RespectsIso.of_forall_exists_iso ?_ ?_ hE

Premises used: CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
refine_1 : ∀ ⦃Z : C⦄ (g : Z ⟶ S), E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)
refine_2 : ∀ ⦃Z : C⦄ (g : Z ⟶ S), F.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), E.presieve₀ (e.hom ≫ g)
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
refine Precoverage.RespectsIso.of_forall_exists_iso ?_ ?_ hE

Premises used: CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
refine_1 : ∀ (g : Z ⟶ S), E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)
⊢ ∀ (g : Z ⟶ S), E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
refine_1 : ∀ (i : E.I₀), ∃ (Y : C) (e : Y ≅ E.X i), F.presieve₀ (e.hom ≫ E.f i)
⊢ E.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), F.presieve₀ (e.hom ≫ g)

Tactic:
⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
i : E.I₀
h : F.presieve₀ ((asIso (e.hom.h₀ i)).symm.hom ≫ E.f i)
⊢ ∃ (Y : C) (e : Y ≅ E.X i), F.presieve₀ (e.hom ≫ E.f i)

Tactic:
use F.X (e.hom.s₀ i), (asIso (e.hom.h₀ i)).symm

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.PreZeroHypercover.X, CategoryTheory.Iso.symm, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
i : E.I₀
⊢ F.presieve₀ ((asIso (e.hom.h₀ i)).symm.hom ≫ E.f i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
refine_2 : ∀ (g : Z ⟶ S), F.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), E.presieve₀ (e.hom ≫ g)
⊢ ∀ (g : Z ⟶ S), F.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), E.presieve₀ (e.hom ≫ g)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
refine_2 : ∀ (i : F.I₀), ∃ (Y : C) (e : Y ≅ F.X i), E.presieve₀ (e.hom ≫ F.f i)
⊢ F.presieve₀ g → ∃ (Y : C) (e : Y ≅ Z), E.presieve₀ (e.hom ≫ g)

Tactic:
⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
i : F.I₀
h : E.presieve₀ ((asIso (e.inv.h₀ i)).symm.hom ≫ F.f i)
⊢ ∃ (Y : C) (e : Y ≅ F.X i), E.presieve₀ (e.hom ≫ F.f i)

Tactic:
use E.X (e.inv.s₀ i), (asIso (e.inv.h₀ i)).symm

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.PreZeroHypercover.X, CategoryTheory.Iso.symm, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.inv, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g : Z ⟶ S
i : F.I₀
⊢ E.presieve₀ ((asIso (e.inv.h₀ i)).symm.hom ≫ F.f i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
⊢ E.presieve₀ ∈ J.coverings S ↔ F.presieve₀ ∈ J.coverings S

Tactic:
⟨fun h ↦ E.presieve₀_mem_of_iso e h, fun h ↦ F.presieve₀_mem_of_iso e.symm h⟩

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
f : S ⟶ T
hf : Presieve.singleton f ∈ J.coverings T
⊢ PreZeroHypercover.presieve₀.{u_1, v, u} (PreZeroHypercover.singleton f) ∈ J.coverings T

Tactic:
simpa [PreZeroHypercover.presieve₀, PreZeroHypercover.singleton, Presieve.ofArrows_pUnit]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, CategoryTheory.PreZeroHypercover.singleton, CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.IsStableUnderComposition
E : ZeroHypercover.{w, v, u} J T
F : ZeroHypercover.{w', v, u} J T
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
rw :
  (PreZeroHypercover.bind.{w', w, v, u} E.toPreZeroHypercover fun (i : E.I₀) ↦
        PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).presieve₀ ∈
    J.coverings T
⊢ (PreZeroHypercover.inter.{w', w, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).presieve₀ ∈ J.coverings T

Tactic:
rw [PreZeroHypercover.inter_def, PreZeroHypercover.presieve₀_reindex]

Premises used: CategoryTheory.PreZeroHypercover.inter_def, CategoryTheory.PreZeroHypercover.presieve₀_reindex
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.IsStableUnderComposition
E : ZeroHypercover.{w, v, u} J T
F : ZeroHypercover.{w', v, u} J T
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ (PreZeroHypercover.bind.{w', w, v, u} E.toPreZeroHypercover fun (i : E.I₀) ↦
        PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).presieve₀ ∈
    J.coverings T

Tactic:
(E.bind (fun i ↦ F.pullback₁ (E.f i))).mem₀

Premises used: CategoryTheory.PreZeroHypercover.f, Set.Mem, CategoryTheory.PreZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.IsStableUnderComposition
E : ZeroHypercover.{w, v, u} J T
F : ZeroHypercover.{w', v, u} J T
inst_3 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ (PreZeroHypercover.bind.{w', w, v, u} E.toPreZeroHypercover fun (i : E.I₀) ↦
        PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).presieve₀ ∈
    J.coverings T

Tactic:
exact (E.bind (fun i ↦ F.pullback₁ (E.f i))).mem₀

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J T
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
⊢ PreZeroHypercover.presieve₀.{w', v, u} (E.reindex e) ∈ J.coverings T

Tactic:
simp [E.mem₀]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderSup
E : ZeroHypercover.{w, v, u} J S
F : ZeroHypercover.{w', v, u} J S
rw :
  PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ⊔
      PreZeroHypercover.presieve₀.{w', v, u} F.toPreZeroHypercover ∈
    J.coverings S
⊢ (PreZeroHypercover.sum.{w', w, v, u} E.toPreZeroHypercover F.toPreZeroHypercover).presieve₀ ∈ J.coverings S

Tactic:
rw [PreZeroHypercover.presieve₀_sum]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_sum
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderSup
E : ZeroHypercover.{w, v, u} J S
F : ZeroHypercover.{w', v, u} J S
⊢ PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ⊔
      PreZeroHypercover.presieve₀.{w', v, u} F.toPreZeroHypercover ∈
    J.coverings S

Tactic:
J.sup_mem_coverings E.mem₀ F.mem₀

Premises used: CategoryTheory.Precoverage.sup_mem_coverings, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
inst_1 : J.IsStableUnderSup
E : ZeroHypercover.{w, v, u} J S
F : ZeroHypercover.{w', v, u} J S
⊢ PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ⊔
      PreZeroHypercover.presieve₀.{w', v, u} F.toPreZeroHypercover ∈
    J.coverings S

Tactic:
exact J.sup_mem_coverings E.mem₀ F.mem₀

Premises used: CategoryTheory.Precoverage.sup_mem_coverings, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T_1 : C
E : ZeroHypercover.{w, v, u} J S
T : C
f : T ⟶ S
hf rwa rwa₁ rwa₂ rwa₃ :
  PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ⊔ Presieve.singleton f ∈ J.coverings S
⊢ PreZeroHypercover.presieve₀.{w, v, u} (E.add f) ∈ J.coverings S

Tactic:
rwa [PreZeroHypercover.presieve₀_add]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_add
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
X Y : C
E : ZeroHypercover.{u_1, v, u} K X
f : Y ⟶ X
⊢ (PreZeroHypercover.presieve₀.{u_1, v, u} E.toPreZeroHypercover).HasPullbacks f

Tactic:
K.hasPullbacks_of_mem _ E.mem₀

Premises used: CategoryTheory.Precoverage.hasPullbacks_of_mem, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T X Y : C
E : PreZeroHypercover.{u_1, v, u} X
f : Y ⟶ X
inst_1 : E.presieve₀.HasPullbacks f
i : E.I₀
⊢ HasPullback (E.f i) f

Tactic:
E.presieve₀.hasPullback f ⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.hasPullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T X Y : C
E : PreZeroHypercover.{u_1, v, u} X
f : Y ⟶ X
inst_1 : E.presieve₀.HasPullbacks f
i : E.I₀
⊢ HasPullback f (E.f i)

Tactic:
hasPullback_symmetry (E.f i) f

Premises used: CategoryTheory.Limits.hasPullback_symmetry, CategoryTheory.PreZeroHypercover.f
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F_1 : Functor.{v, v_1, u, u_1} C D
K : Precoverage.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
E : ZeroHypercover.{w, v, u} J S
h : J ≤ comap F K
rw : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ∈ (comap F K).coverings S
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (K.coverings (F.obj S))
    (PreZeroHypercover.presieve₀.{w, v_1, u_1} (PreZeroHypercover.map F E.toPreZeroHypercover))

Tactic:
rw [PreZeroHypercover.presieve₀_map, ← mem_comap_iff]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_map, CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F_1 : Functor.{v, v_1, u, u_1} C D
K : Precoverage.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
E : ZeroHypercover.{w, v, u} J S
h : J ≤ comap F K
⊢ PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ∈ (comap F K).coverings S

Tactic:
h _ E.mem₀

Premises used: CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F_1 : Functor.{v, v_1, u, u_1} C D
K : Precoverage.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
E : ZeroHypercover.{w, v, u} J S
h : J ≤ comap F K
⊢ PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ∈ (comap F K).coverings S

Tactic:
exact h _ E.mem₀

Premises used: CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
E : ZeroHypercover.{w, v, u} J S
F : PreZeroHypercover.{w, v, u} S
e : E.toPreZeroHypercover ≅ F
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
E.toPreZeroHypercover.presieve₀_mem_of_iso e E.mem₀

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S T : C
E : ZeroHypercover.{w, v, u} J S
inst_1 : Small.{w', w} E.I₀
⊢ PreZeroHypercover.presieve₀.{w', v, u}
      (PreZeroHypercover.restrictIndex.{w', w, v, u} E.toPreZeroHypercover (ι := Shrink.{w', w} E.I₀)
        (⇑(Equiv.symm (equivShrink E.I₀)) : (a : Shrink.{w', w} E.I₀) → E.I₀)) ∈
    J.coverings S

Tactic:
simp [E.mem₀]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
S : C
E : ZeroHypercover.{w, v, u} J S
inst_1 : E.Small
⊢ PreZeroHypercover.presieve₀.{w', v, u} (E.restrictIndex (ι := Index E) (restrictFun E)) ∈ J.coverings S

Tactic:
(Small.exists_restrictIndex_mem E).choose_spec.choose_spec

Premises used: CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem, Exists.choose_spec, Set.Mem, CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun, CategoryTheory.Precoverage.ZeroHypercover.Small.Index