awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this_2 : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
this : ∃ r ∈ s, x ∈ X.basicOpen r
refine_1 :
  ∀ (r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)) (hr : r ∈ s)
    (hrs : x ∈ X.basicOpen r),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
    (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
obtain ⟨r, hr, hrs⟩ := this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
    (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
⟨⟨U, hU⟩, ⟨X.basicOpen r, hV.basicOpen r⟩, hrs, (X.basicOpen_le r).trans e, ?_⟩

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.Scheme.basicOpen_le, Subtype.mk, AlgebraicGeometry.Scheme.basicOpen, Exists.intro, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
refine_1 :
  Q
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
        (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen r) ⋯) : X.Opens) ⋯))
⊢ ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
    (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
refine ⟨⟨U, hU⟩, ⟨X.basicOpen r, hV.basicOpen r⟩, hrs, (X.basicOpen_le r).trans 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
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
refine_1 : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))
⊢ Q
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
        (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen r) ⋯) : X.Opens) ⋯))

Tactic:
rw [← f.appLE_map e (homOfLE (X.basicOpen_le r)).op]

Premises used: Quiver.Hom.op, AlgebraicGeometry.Scheme.basicOpen_le, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
refine_1 :
  ∀ (this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
haveI : IsLocalization.Away r Γ(X, X.basicOpen r) := hV.isLocalization_basicOpen r
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this_2 : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
hfs r hr _

Premises used: AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this_2 : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
exact hfs r hr _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
refine_2 :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (hxV : x ∈ (↑V : X.Opens))
    (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens))
    (hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))),
    ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
obtain ⟨U, V, hxV, e, hf⟩ := hf x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf_1 :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
hxV : x ∈ (↑V : X.Opens)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
h : P (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
use U, V, hxV, 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
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf_1 :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
hxV : x ∈ (↑V : X.Opens)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
h :
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
⊢ P (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)

Tactic:
simp only [iff_of_isAffine (P := P), Scheme.Hom.appLE, homOfLE_leOfHom] at hf ⊢

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine