-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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 : α
⊢ 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)
have 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')
Tactic: apply e.injective