awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
⊢ IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)

Tactic:
have : IsAffine (𝒰.forgetQc.sigma.X default) := by dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
obtain :
  ∀ (φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)) (hφ : Spec.map φ = f),
    Presieve.IsSheafFor F
      (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
        (𝒰.forgetQc (P := P).sigma (P := P).f default))
⊢ Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))

Tactic:
obtain ⟨φ, hφ⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Iso.hom (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ Spec.map φ =
    𝒰.forgetQc (P := P).sigma (P := P).f default

Tactic:
simp [hφ, f]
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
rw : Presieve.IsSheafFor F (Presieve.singleton (Spec.map φ))
⊢ Presieve.IsSheafFor F
    (Presieve.singleton (Y := 𝒰.forgetQc (P := P).sigma (P := P).X default)
      (𝒰.forgetQc (P := P).sigma (P := P).f default))

Tactic:
rw [Presieve.isSheafFor_singleton_iff_of_iso _ (Spec.map φ)
      (𝒰.forgetQc.sigma.X default).isoSpec (by simp [hφ, f])]

Premises used: Inhabited.default, AlgebraicGeometry.Scheme.Cover.sigma, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Spec.map, CategoryTheory.PreZeroHypercover.X, CategoryTheory.Presieve.isSheafFor_singleton_iff_of_iso, AlgebraicGeometry.Scheme.Cover.forgetQc, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Presieve.IsSheafFor F (Presieve.singleton (Spec.map φ))

Tactic:
hff _ ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
refine_1 : P (Spec.map φ)
refine_2 : Surjective (Spec.map φ)
⊢ Presieve.IsSheafFor F (Presieve.singleton (Spec.map φ))

Tactic:
refine hff _ ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ P (Spec.map φ)

Tactic:
simpa only [hφ, f] using IsZariskiLocalAtSource.comp (𝒰.forgetQc.sigma.map_prop _) _

Premises used: AlgebraicGeometry.Scheme.Cover.sigma, AlgebraicGeometry.Scheme.Cover.map_prop, AlgebraicGeometry.Scheme.Cover.forgetQc, AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
refine_2 : Surjective (X := Spec Γ(∐ 𝒰.X, ⊤)) (Iso.inv (∐ 𝒰.X).isoSpec ≫ Sigma.desc 𝒰.f)
⊢ Surjective (Spec.map φ)

Tactic:
simp only [hφ, f, Cover.sigma_I₀, PUnit.default_eq_unit, Cover.sigma_X, Cover.sigma_f, f]

Premises used: AlgebraicGeometry.Scheme.Cover.sigma_X, PUnit.default_eq_unit, AlgebraicGeometry.Scheme.Cover.sigma_I₀, AlgebraicGeometry.Scheme.Cover.sigma_f
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Surjective (X := ∐ 𝒰.X) (Sigma.desc 𝒰.f)

Tactic:
have : Surjective (Sigma.desc 𝒰.f) := inferInstanceAs <| Surjective (Sigma.desc 𝒰.forgetQc.f)
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, u_1, u + 1, u_1 + 1} Schemeᵒᵖ (Type u_1)
inst_2 : IsZariskiLocalAtSource P
h :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
right : Finite.{u + 1} 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc (P := P).sigma (P := P)
this_1 : IsAffine.{u} (𝒰.forgetQc (P := P).sigma (P := P).X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  Iso.inv (𝒰.forgetQc (P := P).sigma (P := P).X default).isoSpec ≫ 𝒰.forgetQc (P := P).sigma (P := P).f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
this : Surjective (X := ∐ 𝒰.X) (Sigma.desc 𝒰.f)
⊢ Surjective (X := Spec Γ(∐ 𝒰.X, ⊤)) (Iso.inv (∐ 𝒰.X).isoSpec ≫ Sigma.desc 𝒰.f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
A : Type u_1
inst_1 : Category.{v_1, u_1} A
inst_2 : P.IsMultiplicative
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Schemeᵒᵖ A
inst_3 : IsZariskiLocalAtSource P
⊢ Presheaf.IsSheaf (propQCTopology P) F ↔
    Presheaf.IsSheaf zariskiTopology F ∧
      ∀ {R S : CommRingCat.{u}} (f : R ⟶ S),
        P (Spec.map f) →
          Surjective (Spec.map f) →
            ∀ (M : A), Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (Opposite.op M)) (Presieve.singleton (Spec.map f))

Tactic:
grind [Presheaf.IsSheaf, isSheaf_type_propQCTopology_iff]

Premises used: AlgebraicGeometry.isSheaf_type_propQCTopology_iff, CategoryTheory.Presheaf.IsSheaf
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
h :
  ∀ ⦃V : Scheme.{u}⦄ (f : V ⟶ X.left),
    Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P)))) f ↔
      (Sieve.ofArrows 𝒰.X 𝒰.f).arrows f
⊢ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P))) =
    Sieve.ofArrows 𝒰.X 𝒰.f

Tactic:
ext V f
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
h :
  (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯) ↔
    ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
⊢ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P)))) f ↔
    (Sieve.ofArrows 𝒰.X 𝒰.f).arrows f

Tactic:
simp only [Sieve.overEquiv_iff, Sieve.generate_apply]

Premises used: CategoryTheory.Sieve.generate_apply, CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
h :
  (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯) →
    ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
h₁ :
  (∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) →
    ∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯
⊢ (∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
      𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯) ↔
    ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Over S
k : 𝒰.I₀
h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ (𝒰.X k).asOver S
hcomp : Eq (α := CategoryTheory.Over.mk (f ≫ X.hom) ⟶ X) (h ≫ Hom.asOver (𝒰.f k) S) (Over.homMk f ⋯)
⊢ ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

Tactic:
⟨𝒰.X k, h.left, 𝒰.f k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, congrArg, CategoryTheory.Over.Hom.left, CategoryTheory.PreZeroHypercover.X, CategoryTheory.CommaMorphism.left, And.intro, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Over S
k : 𝒰.I₀
h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ (𝒰.X k).asOver S
hcomp : Eq (α := CategoryTheory.Over.mk (f ≫ X.hom) ⟶ X) (h ≫ Hom.asOver (𝒰.f k) S) (Over.homMk f ⋯)
⊢ ∃ (Y : Scheme.{u}) (h : V ⟶ Y) (g : Y ⟶ X.left), Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

Tactic:
exact ⟨𝒰.X k, h.left, 𝒰.f k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
⊢ 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S

Tactic:
have : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S := comp_over (𝒰.f k) S
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ h ≫ ((𝒰.X k).asOver S).hom = (CategoryTheory.Over.mk (f ≫ X.hom)).hom

Tactic:
simp [← hcomp, this]
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
h₁ :
  Eq (α := CategoryTheory.Over.mk (f ≫ X.hom) ⟶ X)
    (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h ⋯) (Hom.asOver (𝒰.f k) S)) (Over.homMk f ⋯)
⊢ ∃ (Y : Over S) (h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ Y) (g : Y ⟶ X),
    𝒰.toPresieveOver (P := P) g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
refine ⟨(𝒰.X k).asOver S, Over.homMk h (by simp [← hcomp, this]), (𝒰.f k).asOver S, ⟨k⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
h₁ :
  Eq (α := (CategoryTheory.Over.mk (f ≫ X.hom)).left ⟶ X.left)
    (Over.Hom.left (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h ⋯) (Hom.asOver (𝒰.f k) S)))
    (Over.Hom.left (Over.homMk f ⋯))
⊢ Eq (α := CategoryTheory.Over.mk (f ≫ X.hom) ⟶ X)
    (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h ⋯) (Hom.asOver (𝒰.f k) S)) (Over.homMk f ⋯)

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ Eq (α := (CategoryTheory.Over.mk (f ≫ X.hom)).left ⟶ X.left)
    (Over.Hom.left (CategoryStruct.comp (Y := (𝒰.X k).asOver S) (Over.homMk h ⋯) (Hom.asOver (𝒰.f k) S)))
    (Over.Hom.left (Over.homMk f ⋯))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
simp_rw :
  LE.le (α := Sieve X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P))) : Sieve X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
    Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R
⊢ 𝒰.toPresieveOver (P := P) ≤ R.arrows ↔
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)

Tactic:
simp_rw [← Sieve.giGenerate.gc.le_iff_le, ← Sieve.overEquiv_le_overEquiv_iff]

Premises used: CategoryTheory.Sieve.overEquiv_le_overEquiv_iff, GaloisConnection.le_iff_le, CategoryTheory.Sieve.giGenerate, GaloisInsertion.gc
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
inst_1 : Cover.Over S (P := P) 𝒰
rw rw₁ :
  Sieve.ofArrows 𝒰.X 𝒰.f ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R ↔
    Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R
⊢ LE.le (α := Sieve X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate (𝒰.toPresieveOver (P := P))) : Sieve X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
    Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f) ≤ (Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R

Tactic:
rw [overEquiv_generate_toPresieveOver_eq_ofArrows]

Premises used: AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
Y X : Over S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S (P := P) 𝒰
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (Presieve.pullbackArrows f (𝒰.toPresieveOver (P := P)))

Tactic:
⟨𝒰.pullbackCoverOver' S f.left, inferInstance, ?_⟩

Premises used: Set.Mem, CategoryTheory.Over.Hom.left, setOf, inferInstance, Exists.intro, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
Y X : Over S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S (P := P) 𝒰
refine :
  Presieve.pullbackArrows f (𝒰.toPresieveOver (P := P)) =
    (Cover.pullbackCoverOver' (P := P) S 𝒰 (Over.Hom.left f)).toPresieveOver (P := P)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (Presieve.pullbackArrows f (𝒰.toPresieveOver (P := P)))

Tactic:
refine ⟨𝒰.pullbackCoverOver' S f.left, inferInstance, ?_⟩