-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget
    [IsLocalAtTarget P] [IsLocalAtSource P] :
    RingHom.PropertyIsLocal fun f ↦ P (Spec.map (CommRingCat.ofHom f))

Proof state:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁶ : IsLocalAtTarget P
inst✝⁵ : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))

Tactic:
rw [Spec.map_comp]

Result:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁶ : IsLocalAtTarget P
inst✝⁵ : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))

Proof state:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝³ : IsLocalAtTarget P
inst✝² : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
⊢ P (Spec.map (CommRingCat.ofHom f))

Tactic:
apply IsLocalAtTarget.of_iSup_eq_top _ (PrimeSpectrum.iSup_basicOpen_eq_top_iff
  (f := fun i : s ↦ (i : R)).mpr (by simpa))

Result:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝³ : IsLocalAtTarget P
inst✝² : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
⊢ ∀ (i : ↑s), P (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen ↑i)

Proof state:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝³ : IsLocalAtTarget P
inst✝² : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
⊢ ∀ (i : ↑s), P (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen ↑i)

Tactic:
intro i

Result:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝³ : IsLocalAtTarget P
inst✝² : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
i : ↑s
⊢ P (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen ↑i)

Proof state:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R S _ _ f r R' S' _ _ _ _ _ _ H

Result:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁹ : IsLocalAtTarget P
inst✝⁸ : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom (IsLocalization.Away.map R' S' f r)))

Proof state:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁹ : IsLocalAtTarget P
inst✝⁸ : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom (Localization.awayMap f r)))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
  (CommRingCat.ofHom f) r)).mp (IsLocalAtTarget.restrict H (basicOpen r))

Result:
no goals

Proof state:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R S _ _  f s hs H

Result:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝³ : IsLocalAtTarget P
inst✝² : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
⊢ P (Spec.map (CommRingCat.ofHom f))

Proof state:
P : MorphismProperty Scheme
inst✝³ : IsLocalAtTarget P
inst✝² : IsLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f)))
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ Ideal.span (Set.range fun i => ↑i) = ⊤

Tactic:
simpa

Result:
no goals