-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
/-- Let `Q` be a property of ring maps that is stable under localization.
Then if the associated property of scheme morphisms holds for `f`, `Q` holds on all stalks. -/
lemma stalkMap
    (hQ : ∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (_ : Q f)
      (J : Ideal S) (_ : J.IsPrime), Q (Localization.localRingHom _ J f rfl))
    (hf : P f) (x : X) : Q (f.stalkMap x).hom

Proof state:
case inr.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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↑↑X.toPresheafedSpace
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↑↑X.toPresheafedSpace), IsAffine X ∧ IsAffine Y → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hfx : (ConcreteCategory.hom f.base) x ∈ U
right✝ : U ≤ ⊤
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

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

Result:
case inr.intro.intro.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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↑↑X.toPresheafedSpace
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↑↑X.toPresheafedSpace), IsAffine X ∧ IsAffine Y → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hfx : (ConcreteCategory.hom f.base) x ∈ U
right✝ : U ≤ ⊤
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Proof state:
case inr.intro.intro.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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↑↑X.toPresheafedSpace
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↑↑X.toPresheafedSpace), IsAffine X ∧ IsAffine Y → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hfx : (ConcreteCategory.hom f.base) x ∈ U
right✝ : U ≤ ⊤
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) ⟨x, hx⟩))

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

Result:
no goals

Proof state:
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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↑↑X.toPresheafedSpace
hX : IsAffine X
hY : IsAffine Y
hXY : ∃ R S, Y = Spec R ∧ X = Spec S
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

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

Result:
case 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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↑↑(Spec S).toPresheafedSpace
hX : IsAffine (Spec S)
f : Spec S ⟶ Spec R
hf : P f
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↑↑X.toPresheafedSpace
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↑↑X.toPresheafedSpace), IsAffine X ∧ IsAffine Y → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

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

Result:
case inr.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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↑↑X.toPresheafedSpace
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↑↑X.toPresheafedSpace), IsAffine X ∧ IsAffine Y → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hfx : (ConcreteCategory.hom f.base) x ∈ U
right✝ : U ≤ ⊤
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f 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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↑↑(Spec S).toPresheafedSpace
hX : IsAffine (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))

Tactic:
rw [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)]

Result:
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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↑↑(Spec S).toPresheafedSpace
hX : IsAffine (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom φ)) x).asIdeal x.asIdeal
          (CommRingCat.Hom.hom φ) ⋯)))