-- Mathlib/RingTheory/Localization/Free.lean
/--
If `M` is a finitely presented `R`-module,
then any `Rₛ`-basis of `Mₛ` for some `S : Submonoid R` can be lifted to
a `Rᵣ`-basis of `Mᵣ` for some `r ∈ S`.
-/
lemma Module.FinitePresentation.exists_basis_localizedModule_powers
    (Rₛ) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M']
    [IsLocalization S Rₛ] [Module.FinitePresentation R M]
    {I} [Finite I] (b : Basis I Rₛ M') :
    ∃ (r : R) (hr : r ∈ S)
      (b' : Basis I (Localization (.powers r)) (LocalizedModule (.powers r) M)),
      ∀ i, (LocalizedModule.lift (.powers r) f fun s ↦ IsLocalizedModule.map_units f
        ⟨s.1, SetLike.le_def.mp (Submonoid.powers_le.mpr hr) s.2⟩) (b' i) = b i

Proof state:
case intro.intro.intro.refine_2
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✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this✝ : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e :
  LocalizedModule (Submonoid.powers r) M ≃ₗ[Localization (Submonoid.powers r)]
    LocalizedModule (Submonoid.powers r) (I →₀ R)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
he :
  (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e)
      (e.symm (e'.symm (Finsupp.single i 1))) =
    (↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯)
      (e.symm (e'.symm (Finsupp.single i 1)))
⊢ (LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))) = b i

Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe,
  Function.comp_apply, LinearEquiv.apply_symm_apply, LinearEquiv.restrictScalars_apply] at he

Result:
case intro.intro.intro.refine_2
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✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this✝ : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e :
  LocalizedModule (Submonoid.powers r) M ≃ₗ[Localization (Submonoid.powers r)]
    LocalizedModule (Submonoid.powers r) (I →₀ R)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this : e'.symm (Finsupp.single i 1) = LocalizedModule.mk (Finsupp.single i 1) 1
he :
  (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯)
      (e'.symm (Finsupp.single i 1)) =
    b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))))
⊢ (LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1))) = b i

Proof state:
case intro.intro.intro.refine_2
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✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e :
  LocalizedModule (Submonoid.powers r) M ≃ₗ[Localization (Submonoid.powers r)]
    LocalizedModule (Submonoid.powers r) (I →₀ R)
he :
  LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e =
    ↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
⊢ ∀ (i : I),
    (LocalizedModule.lift (Submonoid.powers r) f ⋯)
        ({
            repr :=
              e ≪≫ₗ
                let __spread.0 := e';
                {
                  toLinearMap :=
                    LinearMap.extendScalarsOfIsLocalization (Submonoid.powers r) (Localization (Submonoid.powers r))
                      ↑e',
                  invFun := __spread.0.invFun, left_inv := ⋯, right_inv := ⋯ } }
          i) =
      b i

Tactic:
intro i

Result:
case intro.intro.intro.refine_2
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✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e :
  LocalizedModule (Submonoid.powers r) M ≃ₗ[Localization (Submonoid.powers r)]
    LocalizedModule (Submonoid.powers r) (I →₀ R)
he :
  LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e =
    ↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
⊢ (LocalizedModule.lift (Submonoid.powers r) f ⋯)
      ({
          repr :=
            e ≪≫ₗ
              let __spread.0 := e';
              {
                toLinearMap :=
                  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers r) (Localization (Submonoid.powers r)) ↑e',
                invFun := __spread.0.invFun, left_inv := ⋯, right_inv := ⋯ } }
        i) =
    b i