-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma mem_freeLocus_of_isLocalization (p : PrimeSpectrum R)
    (Rₚ Mₚ) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal]
    [AddCommGroup Mₚ] [Module R Mₚ] (f : M →ₗ[R] Mₚ) [IsLocalizedModule p.asIdeal.primeCompl f]
    [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] :
    p ∈ freeLocus R M ↔ Module.Free Rₚ Mₚ

Proof state:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ p ∈ freeLocus R M ↔ Free Rₚ Mₚ

Tactic:
apply Module.Free.iff_of_ringEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl
    (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv

Result:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ LocalizedModule p.asIdeal.primeCompl
      M ≃ₛₗ[↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv]
    Mₚ

Proof state:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ LocalizedModule p.asIdeal.primeCompl
      M ≃ₛₗ[↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv]
    Mₚ

Tactic:
refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }

Result:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ ∀ (m : Localization.AtPrime p.asIdeal) (x : LocalizedModule p.asIdeal.primeCompl M),
    (↑__spread✝⁻⁰).toFun (m • x) =
      ↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv m •
        (↑__spread✝⁻⁰).toFun x

Proof state:
case intro.intro.a
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
x : LocalizedModule p.asIdeal.primeCompl M
r : R
s : ↥p.asIdeal.primeCompl
⊢ ↑s • (IsLocalizedModule.iso p.asIdeal.primeCompl f) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s • x) =
    ↑s • IsLocalization.mk' Rₚ r s • (IsLocalizedModule.iso p.asIdeal.primeCompl f) x

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
  IsLocalization.map_id_mk']

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
r : Localization.AtPrime p.asIdeal
x : LocalizedModule p.asIdeal.primeCompl M
⊢ (↑__spread✝⁻⁰).toFun (r • x) =
    ↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv r •
      (↑__spread✝⁻⁰).toFun x

Tactic:
obtain ⟨r, s, rfl⟩ := IsLocalization.mk'_surjective p.asIdeal.primeCompl r

Result:
case intro.intro
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
x : LocalizedModule p.asIdeal.primeCompl M
r : R
s : ↥p.asIdeal.primeCompl
⊢ (↑__spread✝⁻⁰).toFun (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s • x) =
    ↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
        (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) •
      (↑__spread✝⁻⁰).toFun x

Proof state:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ ∀ (m : Localization.AtPrime p.asIdeal) (x : LocalizedModule p.asIdeal.primeCompl M),
    (↑__spread✝⁻⁰).toFun (m • x) =
      ↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv m •
        (↑__spread✝⁻⁰).toFun x

Tactic:
intro r x

Result:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
r : Localization.AtPrime p.asIdeal
x : LocalizedModule p.asIdeal.primeCompl M
⊢ (↑__spread✝⁻⁰).toFun (r • x) =
    ↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv r •
      (↑__spread✝⁻⁰).toFun x