-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
/-- If `Q` is a property of ring maps that can be checked on prime ideals, the
associated property of scheme morphisms can be checked on stalks. -/
lemma of_stalkMap (hQ : OfLocalizationPrime Q) (H : ∀ x, Q (f.stalkMap x).hom) : P f

Proof state:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
⊢ ∀ (i : ↑X.affineOpens), P ((↑i).ι ≫ f)

Tactic:
intro U

Result:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
⊢ P ((↑U).ι ≫ f)

Proof state:
case intro.intro.intro.intro.a
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
P : Ideal ↑S
hP : P.IsPrime
H : Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))
⊢ Q (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)

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

Result:
no goals

Proof state:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine Y → P f
hY : ¬IsAffine Y
⊢ P f

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

Result:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine Y → P f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), P (f ∣_ ↑i)

Proof state:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
x : ↑↑(↑↑U).toPresheafedSpace
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U).ι ≫ f) x))

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

Result:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
x : ↑↑(↑↑U).toPresheafedSpace
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((ConcreteCategory.hom (↑U).ι.base) x)))

Proof state:
case intro.intro.intro.intro
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↑↑(Spec S).toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ Q (CommRingCat.Hom.hom φ)

Tactic:
apply hQ

Result:
case intro.intro.intro.intro.a
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↑↑(Spec S).toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ ∀ (J : Ideal ↑S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Q)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) J) J (CommRingCat.Hom.hom φ) ⋯)

Proof state:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
⊢ ∀ (x : ↑↑(↑↑U).toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U).ι ≫ f) x))

Tactic:
intro x

Result:
case inr
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 fun {R S} [CommRing R] [CommRing S] => Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme} {f : X ⟶ Y},
    (∀ (x : ↑↑X.toPresheafedSpace), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
x : ↑↑(↑↑U).toPresheafedSpace
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U).ι ≫ f) x))