-- Module: Mathlib.RingTheory.TensorProduct.Basic
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
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)
⊢ 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)))

Tactic:
ext