-- 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 ofLocalizationSpanTarget
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.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
intros R S _ _ f s hs H

Result:
case ofLocalizationSpanTarget
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)
⊢ P (Spec.map (CommRingCat.ofHom f))

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 (IsLocalization.Away.map R' S' f r)))

Tactic:
refine (RingHom.RespectsIso.is_localization_away_iff hP ..).mp ?_

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 (Localization.awayMap f r)))

Proof state:
case ofLocalizationSpanTarget
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)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i => ↑i) ⋯).openCover.J
⊢ P ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun i => ↑i) ⋯).openCover.map i ≫ Spec.map (CommRingCat.ofHom f))

Tactic:
simp only [CommRingCat.coe_of, Set.setOf_mem_eq, id_eq, eq_mpr_eq_cast,
  Scheme.AffineOpenCover.openCover_obj, Scheme.affineOpenCoverOfSpanRangeEqTop_obj_carrier,
  Scheme.AffineOpenCover.openCover_map, Scheme.affineOpenCoverOfSpanRangeEqTop_map,
  ← Spec.map_comp]

Result:
case ofLocalizationSpanTarget
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)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i => ↑i) ⋯).openCover.J
⊢ P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away ↑i))))

Proof state:
case ofLocalizationSpanTarget
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)
⊢ P (Spec.map (CommRingCat.ofHom f))

Tactic:
apply IsLocalAtSource.of_openCover (Scheme.affineOpenCoverOfSpanRangeEqTop
  (fun i : s ↦ (i : S)) (by simpa)).openCover

Result:
case ofLocalizationSpanTarget
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)
⊢ ∀ (i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i => ↑i) ⋯).openCover.J),
    P ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun i => ↑i) ⋯).openCover.map i ≫ 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)
i : ↑s
⊢ P (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen ↑i)

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
  (CommRingCat.ofHom f) i.1)).mpr (H i)

Result:
no goals

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))
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
constructor

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))
⊢ RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

case ofLocalizationSpanTarget
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.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

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

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))
⊢ RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] f =>
    P (Spec.map (CommRingCat.ofHom f))