Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝⁷ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝⁶ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝⁵ : IsScalarTower R (Localization.Away f) Rₚ
this✝⁴ : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this✝³ : IsScalarTower R (Localization.Away f) Mₚ
this✝² : IsScalarTower (Localization.Away f) Rₚ Mₚ
l : LocalizedModule (Submonoid.powers f) M →ₗ[Localization.Away f] LocalizedModule p.asIdeal.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers f) (Localization.Away f)
    (IsLocalizedModule.liftOfLE (Submonoid.powers f) p.asIdeal.primeCompl hp'
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M) (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))
this✝¹ : IsLocalization p' Rₚ
this✝ : IsLocalizedModule p.asIdeal.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization.Away f) p.asIdeal.primeCompl) l
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩

Tactic:
have := Module.finrank_of_isLocalizedModule_of_free Rₚ p' l

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝⁸ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝⁷ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝⁶ : IsScalarTower R (Localization.Away f) Rₚ
this✝⁵ : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this✝⁴ : IsScalarTower R (Localization.Away f) Mₚ
this✝³ : IsScalarTower (Localization.Away f) Rₚ Mₚ
l : LocalizedModule (Submonoid.powers f) M →ₗ[Localization.Away f] LocalizedModule p.asIdeal.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers f) (Localization.Away f)
    (IsLocalizedModule.liftOfLE (Submonoid.powers f) p.asIdeal.primeCompl hp'
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M) (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))
this✝² : IsLocalization p' Rₚ
this✝¹ : IsLocalizedModule p.asIdeal.primeCompl (↑R l)
this✝ : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization.Away f) p.asIdeal.primeCompl) l
this :
  finrank Rₚ (LocalizedModule p.asIdeal.primeCompl M) =
    finrank (Localization (Submonoid.powers f)) (LocalizedModule (Submonoid.powers f) M)
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩