-- Mathlib/RingTheory/Localization/Free.lean
/--
If `M` is a finitely presented `R`-module
such that `Mₛ` is free over `Rₛ` for some `S : Submonoid R`,
then `Mᵣ` is already free over `Rᵣ` for some `r ∈ S`.
-/
lemma Module.FinitePresentation.exists_free_localizedModule_powers
    (Rₛ) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M'] [Nontrivial Rₛ]
    [IsLocalization S Rₛ] [Module.FinitePresentation R M] [Module.Free Rₛ M'] :
    ∃ r, r ∈ S ∧
      Module.Free (Localization (.powers r)) (LocalizedModule (.powers r) M) ∧
      Module.finrank (Localization (.powers r)) (LocalizedModule (.powers r) M) =
        Module.finrank Rₛ M'

Proof state:
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) = finrank Rₛ M'

Tactic:
let b : Basis I Rₛ M' := Module.Free.chooseBasis Rₛ M'

Result:
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) = finrank Rₛ M'

Proof state:
case intro.intro.intro
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this✝ : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M)
h✝ : ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
this : Nontrivial (Localization (Submonoid.powers r))
⊢ finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) = finrank Rₛ M'

Tactic:
rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b']

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M)
h✝ : ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) = finrank Rₛ M'

Tactic:
have := (show Localization (.powers r) →+* Rₛ from IsLocalization.map (M := .powers r) (T := S) _
  (RingHom.id _) (Submonoid.powers_le.mpr hr)).domain_nontrivial

Result:
case intro.intro.intro
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this✝ : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M)
h✝ : ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
this : Nontrivial (Localization (Submonoid.powers r))
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) = finrank Rₛ M'