-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem mul_assoc (x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z)

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
⊢ (LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul ∘ₗ mul =
    (((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B))
          LinearMap.lflip)
        ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul.flip ∘ₗ mul)).flip

Tactic:
ext xa xb ya yb za zb

Result:
case a.h.h.a.h.h.a.h.h
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
xa : A
xb : B
ya : A
yb : B
za : A
zb : B
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((AlgebraTensorModule.curry
                      ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul ∘ₗ mul))
                    xa)
                  xb))
              ya)
            yb))
        za)
      zb =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((AlgebraTensorModule.curry
                      (((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B))
                            LinearMap.lflip)
                          ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul.flip ∘ₗ mul)).flip)
                    xa)
                  xb))
              ya)
            yb))
        za)
      zb

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
⊢ (mul ((mul x) y)) z = (mul x) ((mul y) z)

Tactic:
suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
    (LinearMap.llcomp R _ _ _ LinearMap.lflip <| LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
  exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z

Result:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
⊢ (LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul ∘ₗ mul =
    (((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B))
          LinearMap.lflip)
        ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul.flip ∘ₗ mul)).flip

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
this :
  (LinearMap.llcomp R (?m.331774 ⊗[R] ?m.331775) (?m.331774 ⊗[R] ?m.331775)
          (?m.331774 ⊗[R] ?m.331775 →ₗ[R] ?m.331774 ⊗[R] ?m.331775))
        mul ∘ₗ
      mul =
    (((LinearMap.llcomp R (?m.331774 ⊗[R] ?m.331775)
            (?m.331774 ⊗[R] ?m.331775 →ₗ[R] ?m.331774 ⊗[R] ?m.331775 →ₗ[R] ?m.331774 ⊗[R] ?m.331775)
            (?m.331774 ⊗[R] ?m.331775 →ₗ[R] ?m.331774 ⊗[R] ?m.331775 →ₗ[R] ?m.331774 ⊗[R] ?m.331775))
          LinearMap.lflip)
        ((LinearMap.llcomp R (?m.331774 ⊗[R] ?m.331775) (?m.331774 ⊗[R] ?m.331775)
              (?m.331774 ⊗[R] ?m.331775 →ₗ[R] ?m.331774 ⊗[R] ?m.331775))
            mul.flip ∘ₗ
          mul)).flip
⊢ (mul ((mul x) y)) z = (mul x) ((mul y) z)

Tactic:
exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z

Result:
no goals