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
S T : C
E : ZeroHypercover.{w, v, u} J S
obtain :
  ∀ (ι : Type (max u v)) (Y : ι → C) (f : (i : ι) → Y i ⟶ S)
    (h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f),
    ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, CategoryTheory.PreZeroHypercover.presieve₀, 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 S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
Z : C
g : Z ⟶ S
hg rwa rwa₁ rwa₂ rwa₃ : Presieve.ofArrows Y f g
⊢ E.presieve₀ g

Tactic:
rwa [h]
-- 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
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows Y f g
obtain :
  ∀ ⦃Y_1 : C⦄ (j : E.I₀) (hg : Presieve.ofArrows Y f (E.f j)),
    ∃ (j_1 : E.I₀) (h : E.X j = E.X j_1), E.f j = eqToHom h ≫ E.f j_1
⊢ ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j

Tactic:
obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, 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 S
ι : Type (max u v)
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y_1 f
Y : C
j : E.I₀
hg : Presieve.ofArrows Y_1 f (E.f j)
h₁ : E.f j = eqToHom ⋯ ≫ E.f j
⊢ ∃ (j_1 : E.I₀) (h : E.X j = E.X j_1), E.f j = eqToHom h ≫ E.f j_1

Tactic:
use j, rfl

Premises used: rfl
-- 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
ι : Type (max u v)
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y_1 f
Y : C
j : E.I₀
hg : Presieve.ofArrows Y_1 f (E.f j)
⊢ E.f j = eqToHom ⋯ ≫ E.f j

Tactic:
simp
-- 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
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
⊢ ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j

Tactic:
have (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g) :
        ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j := by
      obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
      use j, rfl
      simp
-- 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
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
this : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j
choose :
  ∀ (j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀)
    (h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg))
    (h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)),
    ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
choose j h₁ h₂ using this
-- 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
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Exists.intro
-- 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
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
refine : (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) ⋯).presieve₀ ∈ J.coverings S
⊢ ∃ (ι : Type (max u v)) (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩
-- 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
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover ∈ J.coverings S

Tactic:
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
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
h₃ :
  (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) ⋯).presieve₀ =
    PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover
⊢ (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) ⋯).presieve₀ ∈ J.coverings S

Tactic:
convert! 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
E : ZeroHypercover.{w, v, u} J S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) ⋯).presieve₀ =
    PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover

Tactic:
le_antisymm (fun Z g ⟨i⟩ ↦ ⟨_⟩) (h ▸ fun Z g ⟨i⟩ ↦ .mk' i (h₁ _ _ _) (h₂ _ _ _))

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.PreZeroHypercover.presieve₀, CategoryTheory.Presieve.ofArrows.mk', Eq.rec, CategoryTheory.PreZeroHypercover.restrictIndex, le_antisymm, _private.0.CategoryTheory.Precoverage.ZeroHypercover.instSmall.match_2, Eq.symm, 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 S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → (hg : Presieve.ofArrows Y f g) → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ (E.restrictIndex fun (i : ι) ↦ j (Y i) (f i) ⋯).presieve₀ =
    PreZeroHypercover.presieve₀.{w, v, u} E.toPreZeroHypercover

Tactic:
exact le_antisymm (fun Z g ⟨i⟩ ↦ ⟨_⟩) (h ▸ fun Z g ⟨i⟩ ↦ .mk' i (h₁ _ _ _) (h₂ _ _ _))

Premises used: le_antisymm
-- 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
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
h :
  PreZeroHypercover.presieve₀.{w', v, u}
      (PreZeroHypercover.restrictIndex.{w', w, v, u} (pullback₁ f E).toPreZeroHypercover (ι := Small.Index E)
        (Small.restrictFun E)) ∈
    J.coverings T
⊢ (pullback₁ f E).Small

Tactic:
use Small.Index E, Small.restrictFun E

Premises used: CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun, CategoryTheory.Precoverage.ZeroHypercover.Small.Index
-- 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
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
i : E.restrictIndexOfSmall.I₀
dsimp : HasPullback (Y := E.X (Small.restrictFun E i)) f (E.f (Small.restrictFun E i))
⊢ HasPullback f (E.restrictIndexOfSmall.f i)

Tactic:
dsimp
-- 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
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
i : E.restrictIndexOfSmall.I₀
⊢ HasPullback (Y := E.X (Small.restrictFun E i)) f (E.f (Small.restrictFun E i))

Tactic:
infer_instance
-- 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
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
⊢ ∀ (i : E.restrictIndexOfSmall.I₀), HasPullback f (E.restrictIndexOfSmall.f i)

Tactic:
have _ (i) : HasPullback f (E.restrictIndexOfSmall.f i) := by dsimp; infer_instance
-- 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
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
h : ∀ (i : E.restrictIndexOfSmall.I₀), HasPullback f (E.restrictIndexOfSmall.f i)
⊢ PreZeroHypercover.presieve₀.{w', v, u}
      (PreZeroHypercover.restrictIndex.{w', w, v, u} (pullback₁ f E).toPreZeroHypercover (ι := Small.Index E)
        (Small.restrictFun E)) ∈
    J.coverings T

Tactic:
((restrictIndexOfSmall.{w'} E).pullback₁ f).mem₀

Premises used: CategoryTheory.Limits.limit.π, Set.Mem, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, CategoryTheory.Limits.limit, Classical.choose, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.Small.Index
-- 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
inst_1 : E.Small
T : C
f : T ⟶ S
inst_2 : J.IsStableUnderBaseChange
inst_3 : ∀ (i : E.I₀), HasPullback f (E.f i)
h : ∀ (i : E.restrictIndexOfSmall.I₀), HasPullback f (E.restrictIndexOfSmall.f i)
⊢ PreZeroHypercover.presieve₀.{w', v, u}
      (PreZeroHypercover.restrictIndex.{w', w, v, u} (pullback₁ f E).toPreZeroHypercover (ι := Small.Index E)
        (Small.restrictFun E)) ∈
    J.coverings T

Tactic:
exact ((restrictIndexOfSmall.{w'} E).pullback₁ f).mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} X
⊢ R ∈ J.coverings X ↔ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
⟨fun hR ↦ ?_, fun ⟨𝒰, hR⟩ ↦ hR ▸ 𝒰.mem₀⟩

Premises used: Membership.mem, Eq.rec, _private.0.CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover.match_1, Iff.intro, CategoryTheory.Precoverage.coverings, CategoryTheory.Precoverage.ZeroHypercover.mem₀, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} X
refine : ∀ (hR : R ∈ J.coverings X), ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ R ∈ J.coverings X ↔ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
refine ⟨fun hR ↦ ?_, fun ⟨𝒰, hR⟩ ↦ hR ▸ 𝒰.mem₀⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} X
hR : R ∈ J.coverings X
obtain :
  ∀ (ι : Type (max u v)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X) (hR : Presieve.ofArrows Y f ∈ J.coverings X),
    ∃ (𝒰 : J.ZeroHypercover X), Presieve.ofArrows Y f = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hR : Presieve.ofArrows Y f ∈ J.coverings X
w : J.ZeroHypercover X
h :
  Presieve.ofArrows Y f =
    Presieve.ofArrows { I₀ := ι, X := Y, f := f, mem₀ := hR : J.ZeroHypercover X }.X
      { I₀ := ι, X := Y, f := f, mem₀ := hR : J.ZeroHypercover X }.f
⊢ ∃ (𝒰 : J.ZeroHypercover X), Presieve.ofArrows Y f = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
use ⟨⟨ι, Y, f⟩, hR⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
R : Presieve.{v, u} X
hR : R ∈ J.coverings X
obtain : ∀ (E : PreZeroHypercover X) (hR : E.presieve₀ ∈ J.coverings X), E.presieve₀ ∈ K.coverings X
⊢ R ∈ K.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover

Premises used: CategoryTheory.Presieve.exists_eq_preZeroHypercover, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ J.coverings X
⊢ E.presieve₀ ∈ K.coverings X

Tactic:
h (E := ⟨E, hR⟩)

Premises used: Set.Mem
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ J.coverings X
⊢ E.presieve₀ ∈ K.coverings X

Tactic:
exact h (E := ⟨E, hR⟩)
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : Precoverage.{v, u} C
inst_1 : J.Small
S : C
E : ZeroHypercover.{w', v, u} J S
⊢ E.restrictIndexOfSmall.Small

Tactic:
have : ZeroHypercover.Small.{w} (ZeroHypercover.restrictIndexOfSmall.{max u v} E) :=
    Small.zeroHypercoverSmall _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : Precoverage.{v, u} C
inst_1 : J.Small
S : C
E : ZeroHypercover.{w', v, u} J S
this : E.restrictIndexOfSmall.Small
E' : ZeroHypercover.{w, v, u} J S := E.restrictIndexOfSmall.restrictIndexOfSmall
h :
  PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := E'.I₀)
        (Function.comp (β := ZeroHypercover.Small.Index E) (ZeroHypercover.Small.restrictFun E)
            (ZeroHypercover.Small.restrictFun E.restrictIndexOfSmall) :
          E'.I₀ → E.I₀)) ∈
    J.coverings S
⊢ E.Small

Tactic:
use E'.I₀, ZeroHypercover.Small.restrictFun _ ∘ ZeroHypercover.Small.restrictFun _

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

Tactic:
E'.mem₀

Premises used: Set.Mem, CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun, CategoryTheory.PreZeroHypercover.restrictIndex, Classical.choose, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.Small.Index
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : Precoverage.{v, u} C
inst_1 : J.Small
S : C
E : ZeroHypercover.{w', v, u} J S
this : E.restrictIndexOfSmall.Small
E' : ZeroHypercover.{w, v, u} J S := E.restrictIndexOfSmall.restrictIndexOfSmall
⊢ PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := E'.I₀)
        (Function.comp (β := ZeroHypercover.Small.Index E) (ZeroHypercover.Small.restrictFun E)
            (ZeroHypercover.Small.restrictFun E.restrictIndexOfSmall) :
          E'.I₀ → E.I₀)) ∈
    J.coverings S

Tactic:
exact E'.mem₀

Premises used: CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Precoverage.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J : Precoverage.{v_1, u_1} D
inst_2 : J.Small
X : C
E : (comap F J).ZeroHypercover X
⊢ E.Small

Tactic:
⟨(E.map F le_rfl).restrictIndexOfSmall.I₀, ZeroHypercover.Small.restrictFun _, ?_⟩

Premises used: le_rfl, CategoryTheory.Precoverage.ZeroHypercover.map, CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, CategoryTheory.PreZeroHypercover.I₀, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.Small.mk, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Precoverage.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J : Precoverage.{v_1, u_1} D
inst_2 : J.Small
X : C
E : (comap F J).ZeroHypercover X
refine :
  PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (ZeroHypercover.map F E ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (ZeroHypercover.map F E ⋯) :
          ZeroHypercover.Small.Index (ZeroHypercover.map F E ⋯) → (ZeroHypercover.map F E ⋯).I₀)) ∈
    (comap F J).coverings X
⊢ E.Small

Tactic:
refine ⟨(E.map F le_rfl).restrictIndexOfSmall.I₀, ZeroHypercover.Small.restrictFun _, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Precoverage.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J : Precoverage.{v_1, u_1} D
inst_2 : J.Small
X : C
E : (comap F J).ZeroHypercover X
⊢ PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (ZeroHypercover.map F E ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (ZeroHypercover.map F E ⋯) :
          ZeroHypercover.Small.Index (ZeroHypercover.map F E ⋯) → (ZeroHypercover.map F E ⋯).I₀)) ∈
    (comap F J).coverings X

Tactic:
simpa using (E.map F le_rfl).restrictIndexOfSmall.mem₀

Premises used: le_rfl, CategoryTheory.Precoverage.ZeroHypercover.map, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
inst_1 : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve.{v, u} X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ E.Small

Tactic:
⟨(E.weaken (inf_le_left)).restrictIndexOfSmall.I₀,
        ZeroHypercover.Small.restrictFun _, ⟨?_, ?_⟩⟩

Premises used: CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun, CategoryTheory.Precoverage.ZeroHypercover.weaken, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, CategoryTheory.PreZeroHypercover.I₀, And.intro, Exists.intro, inf_le_left, CategoryTheory.Precoverage.ZeroHypercover.Small.mk, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
inst_1 : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve.{v, u} X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
refine_1 :
  PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ∈
    J.coverings S
refine_2 :
  PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ∈
    K.coverings S
⊢ E.Small

Tactic:
refine ⟨(E.weaken (inf_le_left)).restrictIndexOfSmall.I₀,
        ZeroHypercover.Small.restrictFun _, ⟨?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
inst_1 : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve.{v, u} X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ∈
    J.coverings S

Tactic:
(E.weaken (inf_le_left)).restrictIndexOfSmall.mem₀

Premises used: Set.Mem, setOf, CategoryTheory.Precoverage.ZeroHypercover.weaken, Set.inter, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, Classical.choose, CategoryTheory.Precoverage.ZeroHypercover.mem₀, inf_le_left, CategoryTheory.Precoverage.ZeroHypercover.Small.Index
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
inst_1 : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve.{v, u} X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ∈
    J.coverings S

Tactic:
exact (E.weaken (inf_le_left)).restrictIndexOfSmall.mem₀

Premises used: CategoryTheory.Precoverage.ZeroHypercover.weaken, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, CategoryTheory.Precoverage.ZeroHypercover.mem₀, inf_le_left