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
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_1 :
  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)
this : IsLocalization.Away r' (↑Γ(Y, Y.basicOpen r') : Type u)
⊢ IsLocalization.Away s' (↑Γ(X, X.basicOpen s') : Type u)

Tactic:
haveI := ha.isLocalization_basicOpen s'
-- 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_1 :
  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)
this_2 : IsLocalization.Away r' (↑Γ(Y, Y.basicOpen r') : Type u)
this : IsLocalization.Away s' (↑Γ(X, X.basicOpen s') : Type u)
rw : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
⊢ X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r

Tactic:
rw [hBss', hBrr']
-- 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_1 :
  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)
this_2 : IsLocalization.Away r' (↑Γ(Y, Y.basicOpen r') : Type u)
this : IsLocalization.Away s' (↑Γ(X, X.basicOpen s') : Type u)
⊢ X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r

Tactic:
have ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r := by
    rw [hBss', hBrr']
    apply le_trans (X.basicOpen_le _)
    simp [Scheme.Hom.appLE]
-- 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₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
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₁.carrier (f x : ↥Y)
obtain :
  ∀ (r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) (hBr : Y.basicOpen r ≤ U₁)
    (hBfx :
      Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)),
    ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
      (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))

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

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, AlgebraicGeometry.PresheafedSpace.Hom.base, 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₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
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₁.carrier (f x : ↥Y)
r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBr : Y.basicOpen r ≤ U₁
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)
obtain :
  ∀ (s : (↑Γ(X, (↑V₂ : X.Opens)) : Type u)) (hBs : X.basicOpen s ≤ V₁)
    (hBx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V₁) x hx₁) : ↥X) ∈ X.basicOpen s),
    ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
      (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))

Tactic:
obtain ⟨s, hBs, hBx⟩ := V₂.2.exists_basicOpen_le ⟨x, hx₁⟩ hx₂

Premises used: Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, 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₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
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₁.carrier (f x : ↥Y)
r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBr : Y.basicOpen r ≤ U₁
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)
s : (↑Γ(X, (↑V₂ : X.Opens)) : Type u)
hBs : X.basicOpen s ≤ V₁
hBx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V₁) x hx₁) : ↥X) ∈ X.basicOpen s
obtain :
  ∀ (r' : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Y.basicOpen r) ⋯) : Y.Opens)) : Type u))
    (s' : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen s) ⋯) : X.Opens)) : Type u))
    (hBx' : x ∈ X.basicOpen s') (e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r')
    (hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))),
    ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
      (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))

Tactic:
obtain ⟨r', s', hBx', e', hf'⟩ := exists_basicOpen_le_appLE_of_appLE_of_isAffine hPa hPl x
    ⟨Y.basicOpen r, U₂.2.basicOpen _⟩ U₂ ⟨X.basicOpen s, V₂.2.basicOpen _⟩ V₂ hBx hx₂ e₂ h₂ hBfx

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, Subtype.mk, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine, 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₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
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₁.carrier (f x : ↥Y)
r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBr : Y.basicOpen r ≤ U₁
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)
s : (↑Γ(X, (↑V₂ : X.Opens)) : Type u)
hBs : X.basicOpen s ≤ V₁
hBx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V₁) x hx₁) : ↥X) ∈ X.basicOpen s
r' : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Y.basicOpen r) ⋯) : Y.Opens)) : Type u)
s' : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen s) ⋯) : X.Opens)) : Type u)
hBx' : x ∈ X.basicOpen s'
e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))

Tactic:
⟨⟨Y.basicOpen r', (U₂.2.basicOpen _).basicOpen _⟩,
    ⟨X.basicOpen s', (V₂.2.basicOpen _).basicOpen _⟩, le_trans (Y.basicOpen_le _) hBr,
    le_trans (X.basicOpen_le _) hBs, hBx', e', hf'⟩

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.Scheme.basicOpen_le, Subtype.mk, AlgebraicGeometry.Scheme.basicOpen, Exists.intro, Subtype.property, le_trans
-- 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₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
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₁.carrier (f x : ↥Y)
r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBr : Y.basicOpen r ≤ U₁
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)
s : (↑Γ(X, (↑V₂ : X.Opens)) : Type u)
hBs : X.basicOpen s ≤ V₁
hBx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V₁) x hx₁) : ↥X) ∈ X.basicOpen s
r' : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Y.basicOpen r) ⋯) : Y.Opens)) : Type u)
s' : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen s) ⋯) : X.Opens)) : Type u)
hBx' : x ∈ X.basicOpen s'
e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))

Tactic:
exact ⟨⟨Y.basicOpen r', (U₂.2.basicOpen _).basicOpen _⟩,
    ⟨X.basicOpen s', (V₂.2.basicOpen _).basicOpen _⟩, le_trans (Y.basicOpen_le _) hBr,
    le_trans (X.basicOpen_le _) hBs, hBx', e', hf'⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e : P = P'
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
subst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
⊢ HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' h : ∀ (R S : Type u) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S), Q f ↔ Q' f
⊢ @Q = @Q'

Tactic:
ext R S _ _ f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
R S : Type u
x : CommRing R
x_1 : CommRing S
f : R →+* S
⊢ Q f ↔ Q' f

Tactic:
(e' f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
R S : Type u
x : CommRing R
x_1 : CommRing S
f : R →+* S
⊢ Q f ↔ Q' f

Tactic:
exact (e' f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ @Q = @Q'

Tactic:
have heq : @Q = @Q' := by
    ext R S _ _ f
    exact (e' f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
heq : @Q = @Q'
rw : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'

Tactic:
rw [← heq]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
heq : @Q = @Q'
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P Q
⊢ P = affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
eq_affineLocally'

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget P

Tactic:
inferInstance

Premises used: inferInstance