awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
val : (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover).I₀
⊢ P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inr val))
    ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inr val))

Tactic:
𝒰.map_prop _

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop, Sum.elim
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
val : (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover).I₀
⊢ P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inr val))
    ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inr val))

Tactic:
exact 𝒰.map_prop _

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ QuasiCompactCover 𝒰.qculift (P := P).toPreZeroHypercover

Tactic:
.of_hom (PreZeroHypercover.sumInr _ _)

Premises used: AlgebraicGeometry.QuasiCompactCover.of_hom, CategoryTheory.PreZeroHypercover.sumInr
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ Precoverage.ZeroHypercover.Small 𝒰

Tactic:
⟨𝒰.forgetQc.qculift.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀,
      ⟨?_, ?_⟩⟩

Premises used: AlgebraicGeometry.QuasiCompactCover.uliftHom, AlgebraicGeometry.Scheme.Cover.qculift, CategoryTheory.PreZeroHypercover.I₀, And.intro, Exists.intro, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Precoverage.ZeroHypercover.Small.mk, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.Cover.forgetQc, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Sum.elim
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
refine_1 :
  (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    qcPrecoverage.coverings S
refine_2 :
  (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    (precoverage P).coverings S
⊢ Precoverage.ZeroHypercover.Small 𝒰

Tactic:
refine ⟨𝒰.forgetQc.qculift.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀,
      ⟨?_, ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
refine_1 :
  QuasiCompactCover
    (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
      (Sum.elim 𝒰.forgetQc (P := P).idx
        (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover))))
⊢ (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    qcPrecoverage.coverings S

Tactic:
rw [Scheme.presieve₀_mem_qcPrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (i : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀),
    CategoryStruct.comp (Y :=
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).X
          (Sum.inr i))
        ((fun (i : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀) ↦
            (𝟙 ((QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i) :
              (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i ⟶
                (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i))
          i)
        ((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
          (Sum.inr i)) =
      (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).f i
⊢ ∀ (i : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀),
    CategoryStruct.comp (Y :=
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).X
          (Sum.inr i))
        ((fun (i : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀) ↦
            (𝟙 ((QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i) :
              (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i ⟶
                (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i))
          i)
        ((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
          (Sum.inr i)) =
      (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).f i

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover
    (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
      (Sum.elim 𝒰.forgetQc (P := P).idx
        (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover))))

Tactic:
exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
refine_2 :
  (∀ (x : ↥S),
      ∃ (i :
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
        Membership.mem (γ := Set ↥S)
          (Set.range (ι :=
            ↥((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                    (Sum.elim 𝒰.forgetQc (P := P).idx
                      (PreZeroHypercover.Hom.s₀
                        (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).X
                i))
            ⇑((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                    (Sum.elim 𝒰.forgetQc (P := P).idx
                      (PreZeroHypercover.Hom.s₀
                        (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
                i))
          x) ∧
    ∀
      (i :
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
      P
        ((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
          i)
⊢ (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
        (Sum.elim 𝒰.forgetQc (P := P).idx
          (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).presieve₀ ∈
    (precoverage P).coverings S

Tactic:
rw [Scheme.presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (∀ (x : ↥S),
      ∃ (i :
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
        Membership.mem (γ := Set ↥S)
          (Set.range (ι :=
            ↥((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                    (Sum.elim 𝒰.forgetQc (P := P).idx
                      (PreZeroHypercover.Hom.s₀
                        (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).X
                i))
            ⇑((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                    (Sum.elim 𝒰.forgetQc (P := P).idx
                      (PreZeroHypercover.Hom.s₀
                        (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
                i))
          x) ∧
    ∀
      (i :
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
      P
        ((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
          i)

Tactic:
⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩

Premises used: AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.QuasiCompactCover.uliftHom, Sum.inl, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.map_prop, CategoryTheory.PreZeroHypercover.Hom.s₀, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.Cover.forgetQc, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Sum.elim
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (∀ (x : ↥S),
      ∃ (i :
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
        Membership.mem (γ := Set ↥S)
          (Set.range (ι :=
            ↥((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                    (Sum.elim 𝒰.forgetQc (P := P).idx
                      (PreZeroHypercover.Hom.s₀
                        (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).X
                i))
            ⇑((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
                    (Sum.elim 𝒰.forgetQc (P := P).idx
                      (PreZeroHypercover.Hom.s₀
                        (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
                i))
          x) ∧
    ∀
      (i :
        (𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
            (Sum.elim 𝒰.forgetQc (P := P).idx
              (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).I₀),
      P
        ((𝒰.restrictIndex (ι := 𝒰.forgetQc (P := P).qculift (P := P).I₀)
              (Sum.elim 𝒰.forgetQc (P := P).idx
                (PreZeroHypercover.Hom.s₀ (QuasiCompactCover.uliftHom 𝒰.forgetQc (P := P).toPreZeroHypercover)))).f
          i)

Tactic:
exact ⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
rw :
  (∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f) ↔
    ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
⊢ R ∈ (propQCPrecoverage P).coverings S ↔
    ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀

Tactic:
rw [Precoverage.mem_iff_exists_zeroHypercover]

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
h_1 : ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
𝒰 : Cover (precoverage P) S
left : QuasiCompactCover 𝒰.toPreZeroHypercover
h : R = 𝒰.presieve₀
⊢ 𝒰.presieve₀ ∈ qcPrecoverage.coverings S

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
refine :
  (∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f) →
    ∀ (𝒰 : (propQCPrecoverage P).ZeroHypercover S) (h : R = Presieve.ofArrows 𝒰.X 𝒰.f),
      QuasiCompactCover (𝒰.weaken ⋯).toPreZeroHypercover
⊢ (∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f) ↔
    ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀

Tactic:
refine ⟨fun ⟨𝒰, h⟩ ↦ ⟨𝒰.weaken propQCPrecoverage_le_precoverage, ?_, h⟩,
    fun ⟨𝒰, _, h⟩ ↦ ⟨⟨𝒰.1, ⟨by simpa, 𝒰.mem₀⟩⟩, h⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
h_1 : ∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f
𝒰 : (propQCPrecoverage P).ZeroHypercover S
h : R = Presieve.ofArrows 𝒰.X 𝒰.f
rw : (𝒰.weaken ⋯).presieve₀ ∈ qcPrecoverage.coverings S
⊢ QuasiCompactCover (𝒰.weaken ⋯).toPreZeroHypercover

Tactic:
rw [← Scheme.presieve₀_mem_qcPrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
h_1 : ∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f
𝒰 : (propQCPrecoverage P).ZeroHypercover S
h : R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ (𝒰.weaken ⋯).presieve₀ ∈ qcPrecoverage.coverings S

Tactic:
𝒰.mem₀.1

Premises used: Set.Mem, setOf, And.left, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
R : Presieve S
h_1 : ∃ (𝒰 : (propQCPrecoverage P).ZeroHypercover S), R = Presieve.ofArrows 𝒰.X 𝒰.f
𝒰 : (propQCPrecoverage P).ZeroHypercover S
h : R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ (𝒰.weaken ⋯).presieve₀ ∈ qcPrecoverage.coverings S

Tactic:
exact 𝒰.mem₀.1

Premises used: And.left, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

Tactic:
⟨f.singleton_mem_qcPrecoverage, ?_⟩

Premises used: Set.Mem, AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage, setOf, Set.inter, And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
refine : Presieve.singleton f ∈ (precoverage P).coverings Y
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

Tactic:
refine ⟨f.singleton_mem_qcPrecoverage, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ Presieve.singleton f ∈ (precoverage P).coverings Y

Tactic:
grind [singleton_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
rw : Sieve.generate ⊥ ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) X
⊢ ⊥ ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
rw [← Sieve.generate_bot]

Premises used: CategoryTheory.Sieve.generate_bot
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ Sieve.generate ⊥ ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
Precoverage.generate_mem_toGrothendieck (bot_mem_propQCPrecoverage X)

Premises used: Set.Mem, CategoryTheory.Precoverage.generate_mem_toGrothendieck, AlgebraicGeometry.Scheme.bot_mem_propQCPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ Sieve.generate ⊥ ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
exact Precoverage.generate_mem_toGrothendieck (bot_mem_propQCPrecoverage X)

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck, AlgebraicGeometry.Scheme.bot_mem_propQCPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
hR : Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y
⊢ Sieve.generate (Presieve.singleton f) ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) Y

Tactic:
apply Precoverage.generate_mem_toGrothendieck

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

Tactic:
f.singleton_mem_propQCPrecoverage hf

Premises used: AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst : Surjective f
inst_1 : QuasiCompact f
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

Tactic:
exact f.singleton_mem_propQCPrecoverage hf

Premises used: AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ Sieve.ofArrows 𝒰.X 𝒰.f ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) S

Tactic:
Precoverage.generate_mem_toGrothendieck ⟨?_, 𝒰.mem₀⟩

Premises used: Set.Mem, setOf, CategoryTheory.Precoverage.generate_mem_toGrothendieck, And.intro, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
refine : Presieve.ofArrows 𝒰.X 𝒰.f ∈ qcPrecoverage.coverings S
⊢ Sieve.ofArrows 𝒰.X 𝒰.f ∈ (propQCTopology P : (a : Scheme) → Set (Sieve a)) S

Tactic:
refine Precoverage.generate_mem_toGrothendieck ⟨?_, 𝒰.mem₀⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst rwa rwa₁ rwa₂ rwa₃ : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ∈ qcPrecoverage.coverings S

Tactic:
rwa [presieve₀_mem_qcPrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
⊢ zariskiTopology ≤ propQCTopology P

Tactic:
Precoverage.toGrothendieck_mono zariskiPrecoverage_le_propQCPrecoverage

Premises used: CategoryTheory.Precoverage.toGrothendieck_mono, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_propQCPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j k i : ι
h₁ :
  ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (motive := ι × ι → Scheme) (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)
h₂ :
  ⋯.symmetry ⋯ ≫ ⋯.snd (f i) =
    𝟙
        (match (motive := ι × ι → Scheme) (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.snd (f i)
⊢ ⋯.symmetry ⋯ =
    𝟙
      (match (motive := ι × ι → Scheme) (i, i) with
      | (i, j) => ⋯.pullback (f j))

Tactic:
apply (hf i).rep.hom_ext'

Premises used: CategoryTheory.Functor.relativelyRepresentable.hom_ext', CategoryTheory.MorphismProperty.relative.rep
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (motive := ι × ι → Scheme) (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)

Tactic:
simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]

Premises used: CategoryTheory.MorphismProperty.fst'_self_eq_snd, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.snd (f i) =
    𝟙
        (match (motive := ι × ι → Scheme) (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.snd (f i)

Tactic:
simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]

Premises used: CategoryTheory.MorphismProperty.fst'_self_eq_snd, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ Eq (α :=
    Functor.obj yoneda (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
    (CategoryTheory.Functor.map yoneda (pullback₃.p₂ ⋯ (f j) (f k)) ≫ f j)
    (CategoryTheory.Functor.map yoneda (pullback₃.p₃ ⋯ (f j) (f k)) ≫ f k)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ Eq (α :=
    Functor.obj yoneda (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
    (CategoryTheory.Functor.map yoneda (pullback₃.p₂ ⋯ (f j) (f k)) ≫ f j)
    (CategoryTheory.Functor.map yoneda (pullback₃.p₁ ⋯ (f j) (f k)) ≫ f i)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ CategoryStruct.comp (Y := Limits.pullback (⋯.fst' (f k)) (⋯.fst' (f i)))
        (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯)
        (pullback.snd (⋯.fst' (f k)) (⋯.fst' (f i))) ≫
      ⋯.fst' (f i) =
    (pullback.fst (⋯.fst' (f j)) (⋯.fst' (f k)) ≫ ⋯.symmetry ⋯) ≫ ⋯.fst' (f i)

Tactic:
simp