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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
x : ↥(↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ Q (R := (↑((↑(↑U : Y.Opens) : Scheme).presheaf.stalk ((f ∣_ (↑U : Y.Opens)) x)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ∣_ (↑U : Y.Opens)) x))

Tactic:
exact (hQi.arrow_mk_iso_iff (AlgebraicGeometry.morphismRestrictStalkMap f U x)).mpr (H x.val)

Premises used: Iff.mpr, AlgebraicGeometry.morphismRestrictStalkMap, Subtype.val, 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
        (hX : IsAffine X), P f)
    (hX : ¬IsAffine X), P f
wlog :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
⊢ P f

Tactic:
wlog hX : IsAffine X generalizing X f

Premises used: AlgebraicGeometry.IsAffine
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
inr : ∀ (i : (↑X.affineOpens : Type u)), P ((↑i : X.Opens).ι ≫ f)
⊢ P f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
U : (↑X.affineOpens : Type u)
inr : ∀ (x : ↥(↑(↑U : X.Opens) : Scheme)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U : X.Opens).ι ≫ f) x))
⊢ P ((↑U : X.Opens).ι ≫ f)

Tactic:
refine this ?_ U.2

Premises used: Subtype.property
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
U : (↑X.affineOpens : Type u)
x : ↥(↑(↑U : X.Opens) : Scheme)
inr :
  Q (R := (↑(Y.presheaf.stalk (((↑U : X.Opens).ι ≫ f) x)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((↑U : X.Opens).ι x)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U : X.Opens).ι ≫ f) x))

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

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
U : (↑X.affineOpens : Type u)
x : ↥(↑(↑U : X.Opens) : Scheme)
⊢ Q (R := (↑(Y.presheaf.stalk (((↑U : X.Opens).ι ≫ f) x)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((↑U : X.Opens).ι x)))

Tactic:
H x.val

Premises used: Subtype.val
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
U : (↑X.affineOpens : Type u)
x : ↥(↑(↑U : X.Opens) : Scheme)
⊢ Q (R := (↑(Y.presheaf.stalk (((↑U : X.Opens).ι ≫ f) x)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((↑U : X.Opens).ι x)))

Tactic:
exact H x.val

Premises used: Subtype.val
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
        (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
        (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f)
    (hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
wlog :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
⊢ P f

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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
inr : P (f ≫ Y.isoSpec.hom)
⊢ P f

Tactic:
rw [← P.cancel_right_of_respectsIso (g := Y.isoSpec.hom)]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Iso.hom, 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
inr : P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
⊢ P (f ≫ Y.isoSpec.hom)

Tactic:
rw [← P.cancel_left_of_respectsIso (f := X.isoSpec.inv)]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)

Tactic:
this inferInstance (fun x ↦ ?_) inferInstance ?_

Premises used: inferInstance
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
inr : ∀ (x : ↥(Spec Γ(X, ⊤))), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) x))
inr₁ : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)

Tactic:
refine this inferInstance (fun x ↦ ?_) inferInstance ?_

Premises used: inferInstance
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
x : ↥(Spec Γ(X, ⊤))
inr :
  Q (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv x : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv x)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) x))

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

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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
x : ↥(Spec Γ(X, ⊤))
⊢ Q (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv x : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv x)))

Tactic:
apply 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
obtain :
  ∀ (R S : CommRingCat.{u}) (hY : IsAffine.{u} (Spec R)) (hX : IsAffine.{u} (Spec S)) {f : Spec S ⟶ Spec R}
    (H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))), P f
⊢ P f

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

Premises used: rfl
-- 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_1 : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
f : Spec S ⟶ Spec R
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
obtain :
  ∀ (φ : R ⟶ S) (H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))), P (Spec.map φ)
⊢ P f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- 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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
rw : Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ)

Tactic:
rw [Spec_iff (P := P)]

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_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
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
a :
  ∀ (J : Ideal (↑S : Type u)) (x : J.IsPrime),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) J) J (CommRingCat.Hom.hom φ) ⋯)
⊢ Q (CommRingCat.Hom.hom φ)

Tactic:
apply hQ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P_1 : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P_1 @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
P : Ideal (↑S : Type u)
hP : P.IsPrime
⊢ Q (R := (↑((Spec R).presheaf.stalk ((Spec.map φ) { asIdeal := P, isPrime := hP })) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))

Tactic:
specialize H ⟨P, hP⟩

Premises used: PrimeSpectrum.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P_1 : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P_1 @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
P : Ideal (↑S : Type u)
hP : P.IsPrime
H :
  Q (R := (↑((Spec R).presheaf.stalk ((Spec.map φ) { asIdeal := P, isPrime := hP })) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))
a a₁ a₂ a₃ :
  ∀
    (H :
      Q (R :=
        (↑(CommRingCat.of
              (Localization.AtPrime
                (PrimeSpectrum.comap (CommRingCat.Hom.hom φ)
                    { asIdeal := P, isPrime := hP : PrimeSpectrum (↑S : Type u) }).asIdeal)) :
          Type u))
        (S :=
        (↑(CommRingCat.of
              (Localization.AtPrime { asIdeal := P, isPrime := hP : PrimeSpectrum (↑S : Type u) }.asIdeal)) :
          Type u))
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (Localization.localRingHom
              (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) { asIdeal := P, isPrime := hP }).asIdeal
              { asIdeal := P, isPrime := hP }.asIdeal (CommRingCat.Hom.hom φ) ⋯)))),
    Q (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (S := Localization.AtPrime P)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)
⊢ Q (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)

Tactic:
rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)] at H

Premises used: AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, 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)
inr :
  ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)),
    U ≤ ⊤ → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)

Premises used: TopologicalSpace.Opens.mem_top, TopologicalSpace.Opens.isBasis_iff_nbhd, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe