awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
⊢ P (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))

Tactic:
H U
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
⊢ P (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))

Tactic:
exact H U
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hs' :
  ∀ (r : ↥s),
    sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X :=
      (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme)) (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
U : (↑X.affineOpens : Type u)
of_basicOpenCover :
  ∀ (r : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _
      (Localization.Away (M := (↑Γ(X, (↑U : X.Opens)) : Type u))
        ((CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            (↑r : (↑Γ(Y, ⊤) : Type u)) :
          (↑Γ(X, (↑U : X.Opens)) : Type u)))
      _ _
      (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) (↑r : (↑Γ(Y, ⊤) : Type u)))
⊢ P (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))

Tactic:
apply h₃ _ _ hs
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hs' :
  ∀ (r : ↥s),
    sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X :=
      (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme)) (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
U : (↑X.affineOpens : Type u)
r : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
⊢ ∀ (r : ↥s) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) (↑V : X.Opens) e))

Tactic:
simp_rw [sourceAffineLocally_morphismRestrict] at hs'

Premises used: AlgebraicGeometry.sourceAffineLocally_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
U : (↑X.affineOpens : Type u)
r : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
hs' :
  ∀ (r : ↥s) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) (↑V : X.Opens) e))
⊢ (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
          (X.basicOpen (U := (↑U : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                  (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
              (↑r : (↑Γ(Y, ⊤) : Type u))))
          ⋯) :
      X.Opens) ≤
    f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))

Tactic:
simp [Scheme.Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f
⊢ (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ≤
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
fun _ _ _ hf U V ↦ hPQ (hf U V)

Premises used: AlgebraicGeometry.sourceAffineLocally, AlgebraicGeometry.targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
obtain :
  ∀ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u))
    (hBrr' : Y.basicOpen r = Y.basicOpen r') (hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)),
    ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
      X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
obtain ⟨r, r', hBrr', hBfx⟩ := exists_basicOpen_le_affine_inter U₁.2 U₂.2 (f x)
    ⟨hfx₁, e₂ hx₂⟩

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.exists_basicOpen_le_affine_inter, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
⊢ IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))

Tactic:
have ha : IsAffineOpen (X.basicOpen (f.appLE U₂ V₂ e₂ r')) := V₂.2.basicOpen _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
⊢ x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')

Tactic:
simpa [Scheme.Hom.appLE, ← Scheme.preimage_basicOpen] using And.intro hx₂ (hBrr' ▸ hBfx)

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, And.intro, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
⊢ x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')

Tactic:
have hxa : x ∈ X.basicOpen (f.appLE U₂ V₂ e₂ r') := by
    simpa [Scheme.Hom.appLE, ← Scheme.preimage_basicOpen] using And.intro hx₂ (hBrr' ▸ hBfx)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
obtain :
  ∀ (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u))
    (s' :
      (↑Γ(X,
            X.basicOpen (U := (↑V₂ : X.Opens))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                  (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
                r')) :
        Type u))
    (hBss' : X.basicOpen s = X.basicOpen s') (hBx : x ∈ X.basicOpen s),
    ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
      X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
obtain ⟨s, s', hBss', hBx⟩ := exists_basicOpen_le_affine_inter V₁.2 ha x ⟨hx₁, hxa⟩

Premises used: And.intro, AlgebraicGeometry.exists_basicOpen_le_affine_inter, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)
s' :
  (↑Γ(X,
        X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r')) :
    Type u)
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
⊢ IsLocalization.Away (R := (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r' :
      (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    (↑Γ(X,
          X.basicOpen (U := (↑V₂ : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
              r')) :
      Type u)

Tactic:
haveI := V₂.2.isLocalization_basicOpen (f.appLE U₂ V₂ e₂ r')
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)
s' :
  (↑Γ(X,
        X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r')) :
    Type u)
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r' :
      (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    (↑Γ(X,
          X.basicOpen (U := (↑V₂ : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
              r')) :
      Type u)
⊢ IsLocalization.Away r' (↑Γ(Y, Y.basicOpen r') : Type u)

Tactic:
haveI := U₂.2.isLocalization_basicOpen r'