-- 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'
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)
x : M
x_1 : N
h :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') (x, x_1).1 : M')
    (((↑eM.symm : Localization S ⊗[R] M →ₗ[R] M') : (a : Localization S ⊗[R] M) → M')
        ((((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                              ((1,
                                    (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                        (a : N) → M ⊗[R] N)
                                      x_1) :
                                  Localization (M := R) S × M ⊗[R] N).1 :
                            (a : M) → Localization S ⊗[R] M)
                          (x, x_1).1,
                        (x, x_1).2).1,
                    1).1,
                ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N)
                      (((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                      ((1,
                                            (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                                (a : N) → M ⊗[R] N)
                                              x_1) :
                                          Localization (M := R) S × M ⊗[R] N).1 :
                                    (a : M) → Localization S ⊗[R] M)
                                  (x, x_1).1,
                                (x, x_1).2).1,
                            1) :
                          Localization (M := R) S ⊗[R] M × Localization (M := R) S).2 :
                    (a : N) → Localization S ⊗[R] N)
                  ((((↑(LinearEquiv.symm
                                  (AlgebraTensorModule.rid (Localization (M := R) S) (Localization (M := R) S)
                                    (Localization (M := R) S ⊗[R] M))) :
                              LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                                (Localization (M := R) S ⊗[R] M)
                                (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                              (Localization (M := R) S ⊗[R] M)
                              (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                          (a : Localization S ⊗[R] M) → Localization S ⊗[R] M ⊗[Localization S] Localization S)
                        (((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                  ((1,
                                        (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                            (a : N) → M ⊗[R] N)
                                          x_1) :
                                      Localization (M := R) S × M ⊗[R] N).1 :
                                (a : M) → Localization S ⊗[R] M)
                              (x, x_1).1,
                            (x, x_1).2).1,
                      ((↑(LinearEquiv.symm (LinearEquiv.refl R N)) : N →ₗ[R] N) : (a : N) → N)
                        ((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                    ((1,
                                          (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                              (a : N) → M ⊗[R] N)
                                            x_1) :
                                        Localization (M := R) S × M ⊗[R] N).1 :
                                  (a : M) → Localization S ⊗[R] M)
                                (x, x_1).1,
                              (x, x_1).2) :
                            Localization (M := R) S ⊗[R] M × N).2).2).1,
            (((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                              ((1,
                                    (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                        (a : N) → M ⊗[R] N)
                                      x_1) :
                                  Localization (M := R) S × M ⊗[R] N).1 :
                            (a : M) → Localization S ⊗[R] M)
                          (x, x_1).1,
                        (x, x_1).2).1,
                    1).1,
                ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N)
                      (((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                      ((1,
                                            (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                                (a : N) → M ⊗[R] N)
                                              x_1) :
                                          Localization (M := R) S × M ⊗[R] N).1 :
                                    (a : M) → Localization S ⊗[R] M)
                                  (x, x_1).1,
                                (x, x_1).2).1,
                            1) :
                          Localization (M := R) S ⊗[R] M × Localization (M := R) S).2 :
                    (a : N) → Localization S ⊗[R] N)
                  ((((↑(LinearEquiv.symm
                                  (AlgebraTensorModule.rid (Localization (M := R) S) (Localization (M := R) S)
                                    (Localization (M := R) S ⊗[R] M))) :
                              LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                                (Localization (M := R) S ⊗[R] M)
                                (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                              (Localization (M := R) S ⊗[R] M)
                              (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                          (a : Localization S ⊗[R] M) → Localization S ⊗[R] M ⊗[Localization S] Localization S)
                        (((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                  ((1,
                                        (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                            (a : N) → M ⊗[R] N)
                                          x_1) :
                                      Localization (M := R) S × M ⊗[R] N).1 :
                                (a : M) → Localization S ⊗[R] M)
                              (x, x_1).1,
                            (x, x_1).2).1,
                      ((↑(LinearEquiv.symm (LinearEquiv.refl R N)) : N →ₗ[R] N) : (a : N) → N)
                        ((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                    ((1,
                                          (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                              (a : N) → M ⊗[R] N)
                                            x_1) :
                                        Localization (M := R) S × M ⊗[R] N).1 :
                                  (a : M) → Localization S ⊗[R] M)
                                (x, x_1).1,
                              (x, x_1).2) :
                            Localization (M := R) S ⊗[R] M × N).2).2).2).1 :
      M')
h₁ :
  Eq.{u_6 + 1} (α := N') ((g : (a : N) → N') (x, x_1).2 : N')
    (((↑eN.symm : Localization S ⊗[R] N →ₗ[R] N') : (a : Localization S ⊗[R] N) → N')
        ((((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                              ((1,
                                    (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                        (a : N) → M ⊗[R] N)
                                      x_1) :
                                  Localization (M := R) S × M ⊗[R] N).1 :
                            (a : M) → Localization S ⊗[R] M)
                          (x, x_1).1,
                        (x, x_1).2).1,
                    1).1,
                ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N)
                      (((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                      ((1,
                                            (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                                (a : N) → M ⊗[R] N)
                                              x_1) :
                                          Localization (M := R) S × M ⊗[R] N).1 :
                                    (a : M) → Localization S ⊗[R] M)
                                  (x, x_1).1,
                                (x, x_1).2).1,
                            1) :
                          Localization (M := R) S ⊗[R] M × Localization (M := R) S).2 :
                    (a : N) → Localization S ⊗[R] N)
                  ((((↑(LinearEquiv.symm
                                  (AlgebraTensorModule.rid (Localization (M := R) S) (Localization (M := R) S)
                                    (Localization (M := R) S ⊗[R] M))) :
                              LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                                (Localization (M := R) S ⊗[R] M)
                                (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                              (Localization (M := R) S ⊗[R] M)
                              (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                          (a : Localization S ⊗[R] M) → Localization S ⊗[R] M ⊗[Localization S] Localization S)
                        (((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                  ((1,
                                        (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                            (a : N) → M ⊗[R] N)
                                          x_1) :
                                      Localization (M := R) S × M ⊗[R] N).1 :
                                (a : M) → Localization S ⊗[R] M)
                              (x, x_1).1,
                            (x, x_1).2).1,
                      ((↑(LinearEquiv.symm (LinearEquiv.refl R N)) : N →ₗ[R] N) : (a : N) → N)
                        ((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                    ((1,
                                          (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                              (a : N) → M ⊗[R] N)
                                            x_1) :
                                        Localization (M := R) S × M ⊗[R] N).1 :
                                  (a : M) → Localization S ⊗[R] M)
                                (x, x_1).1,
                              (x, x_1).2) :
                            Localization (M := R) S ⊗[R] M × N).2).2).1,
            (((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                              ((1,
                                    (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                        (a : N) → M ⊗[R] N)
                                      x_1) :
                                  Localization (M := R) S × M ⊗[R] N).1 :
                            (a : M) → Localization S ⊗[R] M)
                          (x, x_1).1,
                        (x, x_1).2).1,
                    1).1,
                ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N)
                      (((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                      ((1,
                                            (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                                (a : N) → M ⊗[R] N)
                                              x_1) :
                                          Localization (M := R) S × M ⊗[R] N).1 :
                                    (a : M) → Localization S ⊗[R] M)
                                  (x, x_1).1,
                                (x, x_1).2).1,
                            1) :
                          Localization (M := R) S ⊗[R] M × Localization (M := R) S).2 :
                    (a : N) → Localization S ⊗[R] N)
                  ((((↑(LinearEquiv.symm
                                  (AlgebraTensorModule.rid (Localization (M := R) S) (Localization (M := R) S)
                                    (Localization (M := R) S ⊗[R] M))) :
                              LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                                (Localization (M := R) S ⊗[R] M)
                                (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S))
                              (Localization (M := R) S ⊗[R] M)
                              (Localization (M := R) S ⊗[R] M ⊗[Localization (M := R) S] Localization (M := R) S)) :
                          (a : Localization S ⊗[R] M) → Localization S ⊗[R] M ⊗[Localization S] Localization S)
                        (((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                  ((1,
                                        (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                            (a : N) → M ⊗[R] N)
                                          x_1) :
                                      Localization (M := R) S × M ⊗[R] N).1 :
                                (a : M) → Localization S ⊗[R] M)
                              (x, x_1).1,
                            (x, x_1).2).1,
                      ((↑(LinearEquiv.symm (LinearEquiv.refl R N)) : N →ₗ[R] N) : (a : N) → N)
                        ((((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M)
                                    ((1,
                                          (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
                                              (a : N) → M ⊗[R] N)
                                            x_1) :
                                        Localization (M := R) S × M ⊗[R] N).1 :
                                  (a : M) → Localization S ⊗[R] M)
                                (x, x_1).1,
                              (x, x_1).2) :
                            Localization (M := R) S ⊗[R] M × N).2).2).2).2 :
      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:
congrm (?_ ⊗ₜ ?_)

Premises used: TensorProduct.tmul