-- 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:
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))
⊢ P f

Tactic:
have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso

Result:
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
⊢ P f

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

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

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

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

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

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

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

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

Tactic:
apply H

Result:
no goals