-- 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'
M₁ : Type ?u.68522
M₂ : Type ?u.68525
B : Type ?u.70458
C : Type ?u.70581
inst_10 : AddCommMonoid M₁
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₁
inst_13 : Module R M₂
inst_14 : Module A M₁
inst_15 : Module A M₂
inst_16 : IsScalarTower R A M₁
inst_17 : IsScalarTower R A M₂
inst_18 : Semiring B
inst_19 : Algebra R B
inst_20 : Algebra A B
inst_21 : IsScalarTower R A B
inst_22 : Semiring C
inst_23 : Algebra R C
inst_24 : Algebra A C
inst_25 : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst_26 : AddCommMonoid N
inst_27 : Module R N
inst_28 : AddCommMonoid N'
inst_29 : Module R N'
g : N →ₗ[R] N'
inst_30 : IsLocalizedModule S f
inst_31 : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization (M := R) S ⊗[R] M :=
  IsLocalizedModule.linearEquiv S f
    ((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M) 1)
eN : N' ≃ₗ[R] Localization (M := R) S ⊗[R] N :=
  IsLocalizedModule.linearEquiv S g
    ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N) 1)
⊢ TensorProduct.map f g =
    (↑(LinearEquiv.restrictScalars R (AlgebraTensorModule.distribBaseChange R (Localization (M := R) S) M N) ≪≫ₗ
            LinearEquiv.symm
              (TensorProduct.congr eM eN ≪≫ₗ
                TensorProduct.equivOfCompatibleSMul (Localization (M := R) S) R R (Localization (M := R) S ⊗[R] M)
                  (Localization (M := R) S ⊗[R] N))) :
        Localization S ⊗[R] (M ⊗[R] N) →ₗ[R] M' ⊗[R] N') ∘ₗ
      (mk R (Localization (M := R) S) (M ⊗[R] N) : (a : Localization S) → M ⊗[R] N →ₗ[R] Localization S ⊗[R] (M ⊗[R] N))
        1
have h : ∀ (x : M) (x_1 : N),
  Eq (α := M' ⊗[R] N')
    (((((AlgebraTensorModule.curry (TensorProduct.map f g) : M →ₗ[R] N →ₗ[R] M' ⊗[R] N') : (a : M) → N →ₗ[R] M' ⊗[R] N')
              x :
            N →ₗ[R] M' ⊗[R] N') :
          (a : N) → M' ⊗[R] N')
        x_1 :
      M' ⊗[R] N')
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.restrictScalars R
                              (AlgebraTensorModule.distribBaseChange R (Localization (M := R) S) M N) ≪≫ₗ
                            LinearEquiv.symm
                              (TensorProduct.congr eM eN ≪≫ₗ
                                TensorProduct.equivOfCompatibleSMul (Localization (M := R) S) R R
                                  (Localization (M := R) S ⊗[R] M) (Localization (M := R) S ⊗[R] N))) :
                        Localization S ⊗[R] (M ⊗[R] N) →ₗ[R] M' ⊗[R] N') ∘ₗ
                      (mk R (Localization (M := R) S) (M ⊗[R] N) :
                          (a : Localization S) → M ⊗[R] N →ₗ[R] Localization S ⊗[R] (M ⊗[R] N))
                        1) :
                  M →ₗ[R] N →ₗ[R] M' ⊗[R] N') :
                (a : M) → N →ₗ[R] M' ⊗[R] N')
              x :
            N →ₗ[R] M' ⊗[R] N') :
          (a : N) → M' ⊗[R] N')
        x_1 :
      M' ⊗[R] N')
Tactic: ext