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
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
inr :
  ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hx : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ U from hfx)

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd, Iff.mp, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- 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 : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
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
inr :
  Q' (R :=
    (↑((↑U : Scheme).presheaf.stalk ((Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))) :
      Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
rw [← hQ'.arrow_mk_iso_iff (Scheme.Hom.resLEStalkMap f e ⟨x, hx⟩)]

Premises used: Subtype.mk, AlgebraicGeometry.Scheme.Hom.resLEStalkMap, RingHom.RespectsIso.arrow_mk_iso_iff
-- 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 : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
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
⊢ Q' (R :=
    (↑((↑U : Scheme).presheaf.stalk ((Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))) :
      Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)))

Tactic:
this (IsZariskiLocalAtSource.resLE _ hf) _ ⟨hV, hU⟩

Premises used: And.intro, AlgebraicGeometry.IsZariskiLocalAtSource.resLE
-- 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 : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
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
⊢ Q' (R :=
    (↑((↑U : Scheme).presheaf.stalk ((Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))) :
      Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)))

Tactic:
exact this (IsZariskiLocalAtSource.resLE _ hf) _ ⟨hV, hU⟩

Premises used: And.intro, AlgebraicGeometry.IsZariskiLocalAtSource.resLE
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
h : IsAffine X ∧ IsAffine Y
⊢ IsAffine X

Tactic:
obtain ⟨hX, hY⟩ := h
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
h : IsAffine X ∧ IsAffine Y
hX : IsAffine X
⊢ IsAffine Y

Tactic:
obtain ⟨hX, hY⟩ := h
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
        (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
        Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
wlog :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))

Tactic:
this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.isoSpec, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.hom, DFunLike.coe
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
refine_1 : P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
refine_2 : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
⊢ Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))

Tactic:
refine this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.isoSpec, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.hom, DFunLike.coe
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
refine_1 : P (f ≫ Y.isoSpec.hom)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : P f
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)

Tactic:
rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
w w₁ : CommRingCat
h : Spec Γ(Y, ⊤) = Spec Γ(Y, ⊤) ∧ Spec Γ(X, ⊤) = Spec Γ(X, ⊤)
⊢ ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S

Tactic:
use Γ(Y, ⊤), Γ(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
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
inr :
  ∀
    (this :
      Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
have : Q' ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom).stalkMap (X.isoSpec.hom x)).hom := by
      refine this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_
      · rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
      · use Γ(Y, ⊤), Γ(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
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))
⊢ Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))

Tactic:
rw [Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp,
      hQ'.cancel_right_isIso, CommRingCat.hom_comp, hQ'.cancel_left_isIso] at this

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, RingHom.RespectsIso.cancel_left_isIso, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))
⊢ X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x

Tactic:
simp
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))
⊢ X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x

Tactic:
have heq : (X.isoSpec.inv (X.isoSpec.hom x)) = x := by simp
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))
heq : X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x
inr inr₁ inr₂ inr₃ :
  ∀ (this : Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (heq : X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x), Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
rwa [hQ'.arrow_mk_iso_iff (f.arrowStalkMapIsoOfEq heq)] at this

Premises used: AlgebraicGeometry.Scheme.Hom.arrowStalkMapIsoOfEq, RingHom.RespectsIso.arrow_mk_iso_iff
-- 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_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
obtain :
  ∀ (R S : CommRingCat.{u}) (hY : IsAffine.{u} (Spec R)) (x : ↥(Spec S)) (hX : IsAffine.{u} (Spec S))
    {f : Spec S ⟶ Spec R} (hf : P f), Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨R, S, rfl, rfl⟩ := hXY

Premises used: rfl