-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
a : α
m : M
b : α
h :
  Eq.{u_4 + 1} (α := M')
    ((e : (a : Localization S ⊗[R] M) → M')
        (((((finsuppRight R R (Localization (M := R) S) M α :
                      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
                    (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
                  ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
                        Finsupp.lsingle a :
                      (a : M) → Localization S ⊗[R] (α →₀ M))
                    m) :
                α →₀ Localization (M := R) S ⊗[R] M) :
              (a : α) → Localization S ⊗[R] M)
            b :
          Localization (M := R) S ⊗[R] M) :
      M')
    ((e : (a : Localization S ⊗[R] M) → M')
        (((((finsuppRight R R (Localization (M := R) S) M α :
                      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
                    (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
                  (((mk R (Localization (M := R) S) (α →₀ M) :
                            (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
                          1 ∘ₗ
                        Finsupp.lsingle a :
                      (a : M) → Localization S ⊗[R] (α →₀ M))
                    m) :
                α →₀ Localization (M := R) S ⊗[R] M) :
              (a : α) → Localization S ⊗[R] M)
            b :
          Localization (M := R) S ⊗[R] M) :
      M')
⊢ Eq (α := Localization (M := R) S ⊗[R] M)
    (((((finsuppRight R R (Localization (M := R) S) M α :
                  Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
                (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
              ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
                    Finsupp.lsingle a :
                  (a : M) → Localization S ⊗[R] (α →₀ M))
                m) :
            α →₀ Localization (M := R) S ⊗[R] M) :
          (a : α) → Localization S ⊗[R] M)
        b :
      Localization (M := R) S ⊗[R] M)
    (((((finsuppRight R R (Localization (M := R) S) M α :
                  Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
                (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
              (((mk R (Localization (M := R) S) (α →₀ M) :
                        (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
                      1 ∘ₗ
                    Finsupp.lsingle a :
                  (a : M) → Localization S ⊗[R] (α →₀ M))
                m) :
            α →₀ Localization (M := R) S ⊗[R] M) :
          (a : α) → Localization S ⊗[R] M)
        b :
      Localization (M := R) S ⊗[R] M)

Tactic:
apply e.injective

Premises used: LinearEquiv.injective