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

Tactic:
apply ((Module.End_isUnit_iff _).mp (IsLocalizedModule.map_units f s)).1

Result:
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
⊢ ((algebraMap R (End R Mₚ)) ↑s) ((↑__spread✝⁻⁰).toFun (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s • x)) =
    ((algebraMap R (End R Mₚ)) ↑s)
      (↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
          (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) •
        (↑__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
⊢ ((algebraMap R (End R Mₚ)) ↑s) ((↑__spread✝⁻⁰).toFun (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s • x)) =
    ((algebraMap R (End R Mₚ)) ↑s)
      (↑(IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
          (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) •
        (↑__spread✝⁻⁰).toFun x)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
  algebraMap_end_apply, AlgEquiv.toRingEquiv_eq_coe,
  AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, IsLocalization.algEquiv_apply,
  IsLocalization.map_id_mk']

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