-- 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:
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
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↑↑X.toPresheafedSpace),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ Q
    (CommRingCat.Hom.hom
      (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) ((ConcreteCategory.hom X.isoSpec.hom.base) x)))

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

Result:
case refine_1
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
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↑↑X.toPresheafedSpace),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)

case refine_2
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
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↑↑X.toPresheafedSpace),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ ∃ R S, Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S

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
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↑↑X.toPresheafedSpace),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
this :
  Q
    (CommRingCat.Hom.hom
      (Scheme.Hom.stalkMap f ((ConcreteCategory.hom X.isoSpec.inv.base) ((ConcreteCategory.hom X.isoSpec.hom.base) x))))
⊢ (ConcreteCategory.hom X.isoSpec.inv.base) ((ConcreteCategory.hom X.isoSpec.hom.base) x) = x

Tactic:
simp

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
h : IsAffine X ∧ IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨hX, hY⟩ := h

Result:
case 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
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↑↑X.toPresheafedSpace
hX : IsAffine X
hY : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Proof state:
case 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
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↑↑X.toPresheafedSpace
hX : IsAffine X
hY : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y

Result:
case intro.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 ⋯)
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
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↑↑X.toPresheafedSpace),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

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))