-- 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ₛ)) ⋯)
      (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

Tactic:
apply b.repr.injective

Result:
case intro.intro.intro.refine_2.a
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))))
⊢ b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1)))) = b.repr (b i)

Proof state:
case intro.intro.intro.refine_2.a
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))))
⊢ b.repr ((LocalizedModule.lift (Submonoid.powers r) f ⋯) (e.symm (e'.symm (Finsupp.single i 1)))) = b.repr (b i)

Tactic:
rw [← he, Basis.repr_self, this, LocalizedModule.lift_mk]

Result:
case intro.intro.intro.refine_2.a
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))))
⊢ ↑⋯.unit⁻¹ ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (Finsupp.single i 1)) = Finsupp.single i 1

Proof state:
case intro.intro.intro.refine_1
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))))
⊢ LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[Localization (Submonoid.powers r)]
    I →₀ Localization (Submonoid.powers r)

Tactic:
exact
{ __ := e',
  toLinearMap := e'.extendScalarsOfIsLocalization (.powers r) (Localization (.powers r)) }

Result:
no goals