awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥X
hy : Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)
of_sSup_eq_top :
  ∀ (i : ι) (hi : Membership.mem (α := ↥Y) (U i) (f x : ↥Y)), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy

Premises used: TopologicalSpace.Opens.mem_iSup, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥X
hy : Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)
i : ι
hi : Membership.mem (α := ↥Y) (U i) (f x : ↥Y)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
((RingHom.toMorphismProperty P).arrow_mk_iso_iff <|
      morphismRestrictStalkMap f (U i) ⟨x, hi⟩).mp <| hf i ⟨x, hi⟩

Premises used: AlgebraicGeometry.morphismRestrictStalkMap, Subtype.mk, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥X
hy : Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)
i : ι
hi : Membership.mem (α := ↥Y) (U i) (f x : ↥Y)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
exact ((RingHom.toMorphismProperty P).arrow_mk_iso_iff <|
      morphismRestrictStalkMap f (U i) ⟨x, hi⟩).mp <| hf i ⟨x, hi⟩

Premises used: AlgebraicGeometry.morphismRestrictStalkMap, Subtype.mk, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
restrict :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ IsZariskiLocalAtSource.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)

Tactic:
apply IsZariskiLocalAtSource.mk'

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥(↑U : Scheme)
restrict : P (R := (↑(Y.presheaf.stalk ((U.ι ≫ f) x)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (U.ι x)))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U.ι ≫ f) x))

Tactic:
rw [Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp, hP.cancel_right_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥(↑U : Scheme)
⊢ P (R := (↑(Y.presheaf.stalk ((U.ι ≫ f) x)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (U.ι x)))

Tactic:
hf _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥(↑U : Scheme)
⊢ P (R := (↑(Y.presheaf.stalk ((U.ι ≫ f) x)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (U.ι x)))

Tactic:
exact hf _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
rw : Membership.mem (γ := X.Opens) ⊤ x
⊢ x ∈ iSup U

Tactic:
rw [hU]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
⊢ Membership.mem (γ := X.Opens) ⊤ x

Tactic:
trivial
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
of_sSup_eq_top : ∀ (hy : x ∈ iSup U), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
have hy : x ∈ iSup U := by rw [hU]; trivial
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
hy : x ∈ iSup U
of_sSup_eq_top : ∀ (i : ι) (hi : x ∈ U i), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy

Premises used: TopologicalSpace.Opens.mem_iSup, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
hy : x ∈ iSup U
i : ι
hi : x ∈ U i
⊢ P
    (RingHom.comp (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U i).ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) x hi)))
      (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))

Tactic:
simpa [Scheme.Hom.stalkMap_comp] using hf i ⟨x, hi⟩

Premises used: Subtype.mk, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
⊢ (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso

Tactic:
have hP' : (RingHom.toMorphismProperty P).RespectsIso :=
    RingHom.toMorphismProperty_respectsIso_iff.mp hP
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
trans :
  stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) ⋯)
trans₁ :
  (∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ)
          ⋯)) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)

Tactic:
trans ∀ (p : PrimeSpectrum S), P (Localization.localRingHom _ p.asIdeal φ.hom rfl)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) ⋯)

Tactic:
forall_congr' fun p ↦
      (RingHom.toMorphismProperty P).arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso _ _)

Premises used: AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, forall_congr', AlgebraicGeometry.stalkwise
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) ⋯)

Tactic:
exact forall_congr' fun p ↦
      (RingHom.toMorphismProperty P).arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso _ _)

Premises used: AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, forall_congr'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ (∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ)
          ⋯)) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)

Tactic:
⟨fun H p hp ↦ H ⟨p, hp⟩, fun H p ↦ H p.1 p.2⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.isPrime, Iff.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ (∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ)
          ⋯)) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)

Tactic:
exact ⟨fun H p hp ↦ H ⟨p, hp⟩, fun H p ↦ H p.1 p.2⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
hP₂ : IsStableUnderBaseChange.{u_1} (of P)
⊢ P.IsStableUnderBaseChange

Tactic:
letI := HasAffineProperty.of_isZariskiLocalAtTarget P
  HasAffineProperty.isStableUnderBaseChange hP₂

Premises used: AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
⊢ ∃ (Y : Scheme.{u}) (p : Y ⟶ X), Surjective p ∧ P p ∧ IsAffine Y

Tactic:
⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩

Premises used: inferInstance, And.intro, AlgebraicGeometry.Surjective.mk, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
refine_1 : ∀ (x : ↥X), ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), p a = x
refine_2 : P p
⊢ ∃ (Y : Scheme.{u}) (p : Y ⟶ X), Surjective p ∧ P p ∧ IsAffine Y

Tactic:
refine ⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
x : ↥X
refine_1 :
  ∀ (i : X.affineCover.finiteSubcover.I₀) (x : ↥(X.affineCover.finiteSubcover.X i)),
    ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), Eq (α := ↥X) (p a : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
⊢ ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), p a = x

Tactic:
obtain ⟨i, x, rfl⟩ := X.affineCover.finiteSubcover.exists_eq x

Premises used: AlgebraicGeometry.Scheme.OpenCover.finiteSubcover, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
i : X.affineCover.finiteSubcover.I₀
x : ↥(X.affineCover.finiteSubcover.X i)
h :
  Eq (α := ↥X) (p ((Sigma.ι X.affineCover.finiteSubcover.X i) x : ↥(∐ X.affineCover.finiteSubcover.X)) : ↥X)
    ((X.affineCover.finiteSubcover.f i) x : ↥X)
⊢ ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), Eq (α := ↥X) (p a : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)

Tactic:
use Sigma.ι X.affineCover.finiteSubcover.X i x

Premises used: AlgebraicGeometry.Scheme.OpenCover.finiteSubcover, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Sigma.ι, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
i : X.affineCover.finiteSubcover.I₀
x : ↥(X.affineCover.finiteSubcover.X i)
h : Eq (α := ↥X) ((Sigma.ι X.affineCover.finiteSubcover.X i ≫ p) x : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
h₁ h₂ : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
⊢ Eq (α := ↥X) (p ((Sigma.ι X.affineCover.finiteSubcover.X i) x : ↥(∐ X.affineCover.finiteSubcover.X)) : ↥X)
    ((X.affineCover.finiteSubcover.f i) x : ↥X)

Tactic:
rw [← Scheme.Hom.comp_apply, Sigma.ι_desc]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
refine_2 :
  ∀
    (i :
      PreZeroHypercover.I₀ (S := ∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i) :
          PreZeroHypercover (C := Scheme) (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i))),
    P (X :=
      PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ≫
          p :
        PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ⟶
          X)
⊢ P p

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (sigmaOpenCover _)]

Premises used: AlgebraicGeometry.sigmaOpenCover, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
i :
  PreZeroHypercover.I₀ (S := ∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i) :
      PreZeroHypercover (C := Scheme) (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i))
⊢ P (X :=
    PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ≫
        p :
      PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ⟶
        X)

Tactic:
simpa [p] using IsZariskiLocalAtSource.of_isOpenImmersion _

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
⊢ ∀
    (i :
      PreZeroHypercover.I₀ (S := ∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i) :
          PreZeroHypercover (C := Scheme) (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i))),
    P (X :=
      PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ≫
          p :
        PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ⟶
          X)

Tactic:
exact fun i ↦ by simpa [p] using IsZariskiLocalAtSource.of_isOpenImmersion _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
H₁ :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
⊢ P.DescendsAlong P'

Tactic:
apply MorphismProperty.DescendsAlong.mk'

Premises used: CategoryTheory.MorphismProperty.DescendsAlong.mk'