-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
s : S
m : M
⊢ Eq (α := N)
    ((IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) : (a : N) → N)
        (((((↑R :
                        {S M : Type v₃} →
                          {M₂ : Type (max v₁ v₂)} →
                            [inst : Semiring R] →
                              [inst_9 : Semiring S] →
                                [inst_10 : AddCommMonoid M] →
                                  [inst_11 : AddCommMonoid M₂] →
                                    [inst_12 : Module R M] →
                                      [inst_13 : Module R M₂] →
                                        [inst_14 : Module S M] →
                                          [inst_15 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (S := S)
                      (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) :
                            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                        f) :
                    (a : S) → M →ₗ[R] N)
                  s :
                M →ₗ[R] N) :
              (a : M) → N)
            m :
          N) :
      N)
    (((↑R :
              {S : Type v₃} →
                {M M₂ : Type v₂} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
          (a : N) → N)
        (((((↑R :
                        {S M : Type v₃} →
                          {M₂ : Type (max v₁ v₂)} →
                            [inst : Semiring R] →
                              [inst_9 : Semiring S] →
                                [inst_10 : AddCommMonoid M] →
                                  [inst_11 : AddCommMonoid M₂] →
                                    [inst_12 : Module R M] →
                                      [inst_13 : Module R M₂] →
                                        [inst_14 : Module S M] →
                                          [inst_15 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (S := S)
                      (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) :
                            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                        f) :
                    (a : S) → M →ₗ[R] N)
                  s :
                M →ₗ[R] N) :
              (a : M) → N)
            m :
          N) :
      N)
have h : Eq (α := N)
  (((((↑R :
                  {S M : Type v₃} →
                    {M₂ : Type (max v₁ v₂)} →
                      [inst : Semiring R] →
                        [inst_9 : Semiring S] →
                          [inst_10 : AddCommMonoid M] →
                            [inst_11 : AddCommMonoid M₂] →
                              [inst_12 : Module R M] →
                                [inst_13 : Module R M₂] →
                                  [inst_14 : Module S M] →
                                    [inst_15 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (S := S)
                (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) :
                      (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                    (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                  f) :
              (a : S) → M →ₗ[R] N)
            ((LinearMap.id : (a : S) → S) s) :
          M →ₗ[R] N) :
        (a : M) → N)
      ((((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x : M →ₗ[R] M) : (a : M) → M) m : M) :
    N)
  (((↑R :
            {S : Type v₃} →
              {M M₂ : Type v₂} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
        (a : N) → N)
      (((((↑R :
                      {S M : Type v₃} →
                        {M₂ : Type (max v₁ v₂)} →
                          [inst : Semiring R] →
                            [inst_9 : Semiring S] →
                              [inst_10 : AddCommMonoid M] →
                                [inst_11 : AddCommMonoid M₂] →
                                  [inst_12 : Module R M] →
                                    [inst_13 : Module R M₂] →
                                      [inst_14 : Module S M] →
                                        [inst_15 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (S := S)
                    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] N))) :
                          (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                        (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                      f) :
                  (a : S) → M →ₗ[R] N)
                s :
              M →ₗ[R] N) :
            (a : M) → N)
          m :
        N) :
    N)
Tactic: rw [hf.map_eq hf]