-- 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
⊢ 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)
    (((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)
have h : ∀ (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)
Tactic: ext b