-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma freeLocus_localization (S : Submonoid R) :
    freeLocus (Localization S) (LocalizedModule S M) =
      comap (algebraMap R _) ⁻¹' freeLocus R M

Proof state:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁴ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝³ : IsScalarTower R (Localization S) Rₚ
this✝² : IsLocalization.AtPrime Rₚ p.asIdeal
this✝¹ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝ : IsScalarTower R (Localization S) Mₚ
this : IsScalarTower (Localization S) Rₚ Mₚ
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ (comap (algebraMap R (Localization S))) p ∈ freeLocus R M

Tactic:
let l := (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
  (LocalizedModule.mkLinearMap p'.primeCompl M)).extendScalarsOfIsLocalization S
  (Localization S)

Result:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁴ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝³ : IsScalarTower R (Localization S) Rₚ
this✝² : IsLocalization.AtPrime Rₚ p.asIdeal
this✝¹ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝ : IsScalarTower R (Localization S) Mₚ
this : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ (comap (algebraMap R (Localization S))) p ∈ freeLocus R M

Proof state:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ (comap (algebraMap R (Localization S))) p ∈ freeLocus R M

Tactic:
let Rₚ := Localization.AtPrime p'

Result:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ (comap (algebraMap R (Localization S))) p ∈ freeLocus R M

Proof state:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ p ∈ ⇑(comap (algebraMap R (Localization S))) ⁻¹' freeLocus R M

Tactic:
simp only [Set.mem_preimage]

Result:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ (comap (algebraMap R (Localization S))) p ∈ freeLocus R M

Proof state:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁴ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝³ : IsScalarTower R (Localization S) Rₚ
this✝² : IsLocalization.AtPrime Rₚ p.asIdeal
this✝¹ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝ : IsScalarTower R (Localization S) Mₚ
this : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
⊢ IsLocalizedModule p.asIdeal.primeCompl l

Tactic:
have : IsLocalizedModule p'.primeCompl (l.restrictScalars R) :=
  inferInstanceAs (IsLocalizedModule p'.primeCompl
    (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
    (LocalizedModule.mkLinearMap p'.primeCompl M)))

Result:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁵ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁴ : IsScalarTower R (Localization S) Rₚ
this✝³ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝² : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝¹ : IsScalarTower R (Localization S) Mₚ
this✝ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p'.primeCompl (↑R l)
⊢ IsLocalizedModule p.asIdeal.primeCompl l