-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ Eq (α := S ⊗[R] A →ₗ[S] S ⊗[R] A →ₗ[S] B)
    (LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
      (LinearMap.liftBaseChange S
        (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)))
    (LinearMap.compl₁₂ (LinearMap.mul S B)
      (LinearMap.liftBaseChange S
        (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
      (LinearMap.liftBaseChange S
        (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)))
have e_a : ∀ (x x_1 : A),
  Eq.{u_7 + 1} (α := B)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry
                              (LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
                                (LinearMap.liftBaseChange S
                                  (↑f :
                                    [inst : FunLike (A →ₐ[R] B) A B] →
                                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))) :
                            S →ₗ[S] A →ₗ[R] S ⊗[R] A →ₗ[S] B) :
                          (a : S) → A →ₗ[R] S ⊗[R] A →ₗ[S] B)
                        1 :
                      (a : A) → S ⊗[R] A →ₗ[S] B)
                    x) :
                S →ₗ[S] A →ₗ[R] B) :
              (a : S) → A →ₗ[R] B)
            1 :
          (a : A) → B)
        x_1 :
      B)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry
                              (LinearMap.compl₁₂ (LinearMap.mul S B)
                                (LinearMap.liftBaseChange S
                                  (↑f :
                                    [inst : FunLike (A →ₐ[R] B) A B] →
                                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                                (LinearMap.liftBaseChange S
                                  (↑f :
                                    [inst : FunLike (A →ₐ[R] B) A B] →
                                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))) :
                            S →ₗ[S] A →ₗ[R] S ⊗[R] A →ₗ[S] B) :
                          (a : S) → A →ₗ[R] S ⊗[R] A →ₗ[S] B)
                        1 :
                      (a : A) → S ⊗[R] A →ₗ[S] B)
                    x) :
                S →ₗ[S] A →ₗ[R] B) :
              (a : S) → A →ₗ[R] B)
            1 :
          (a : A) → B)
        x_1 :
      B)
Tactic: ext