-- 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:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
have hP : RingHom.RespectsIso (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
  RingHom.toMorphismProperty_respectsIso_iff.mpr
    (inferInstanceAs (P.inverseImage Scheme.Spec).unop.RespectsIso)

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

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

Tactic:
intro R S T _ _ _ _ r _ f hf

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))
⊢ P (Spec.map (CommRingCat.ofHom ((algebraMap S T).comp 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 (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))

Tactic:
exact IsLocalAtSource.comp hf ..

Result:
no goals

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 ((algebraMap S T).comp f)))

Tactic:
show P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap _ _)))

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 f ≫ CommRingCat.ofHom (algebraMap S T)))

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))
⊢ P (Spec.map (CommRingCat.ofHom ((algebraMap S T).comp f)))

Tactic:
have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := T) r

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

Tactic:
exact H i

Result:
no goals

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:
intro i

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:
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)
⊢ Ideal.span (Set.range fun i => ↑i) = ⊤

Tactic:
simpa

Result:
no goals