-- Mathlib/RingTheory/PiTensorProduct.lean
protected lemma mul_assoc (x y z : ⨂[R] i, A i) : mul (mul x y) z = mul x (mul y z)

Proof state:
case H.H.H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ z✝ : ⨂[R] (i : ι), A i
x y z : (i : ι) → A i
⊢ (tprod R) x * (tprod R) y * (tprod R) z = (tprod R) x * ((tprod R) y * (tprod R) z)

Tactic:
simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z)

Result:
no goals

Proof state:
case H.H.H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ z✝ : ⨂[R] (i : ι), A i
x y z : (i : ι) → A i
⊢ (((((((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                          mul ∘ₗ
                        mul).compMultilinearMap
                    (tprod R))
                  x).compMultilinearMap
              (tprod R))
            y).compMultilinearMap
        (tprod R))
      z =
    ((((((((LinearMap.llcomp R (⨂[R] (i : ι), A i)
                              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                            LinearMap.lflip)
                          ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i)
                                ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                              mul.flip ∘ₗ
                            mul)).flip.compMultilinearMap
                    (tprod R))
                  x).compMultilinearMap
              (tprod R))
            y).compMultilinearMap
        (tprod R))
      z

Tactic:
dsimp [← mul_def]

Result:
case H.H.H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ z✝ : ⨂[R] (i : ι), A i
x y z : (i : ι) → A i
⊢ (tprod R) x * (tprod R) y * (tprod R) z = (tprod R) x * ((tprod R) y * (tprod R) z)

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
⊢ (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:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
⊢ (LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul ∘ₗ
      mul =
    (((LinearMap.llcomp R (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
          LinearMap.lflip)
        ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
            mul.flip ∘ₗ
          mul)).flip

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
⊢ (LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul ∘ₗ
      mul =
    (((LinearMap.llcomp R (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
          LinearMap.lflip)
        ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
            mul.flip ∘ₗ
          mul)).flip

Tactic:
ext x y z

Result:
case H.H.H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ z✝ : ⨂[R] (i : ι), A i
x y z : (i : ι) → A i
⊢ (((((((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                          mul ∘ₗ
                        mul).compMultilinearMap
                    (tprod R))
                  x).compMultilinearMap
              (tprod R))
            y).compMultilinearMap
        (tprod R))
      z =
    ((((((((LinearMap.llcomp R (⨂[R] (i : ι), A i)
                              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                            LinearMap.lflip)
                          ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i)
                                ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                              mul.flip ∘ₗ
                            mul)).flip.compMultilinearMap
                    (tprod R))
                  x).compMultilinearMap
              (tprod R))
            y).compMultilinearMap
        (tprod R))
      z

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
this :
  (LinearMap.llcomp R (⨂[R] (i : ?m.133597), ?m.133599 i) (⨂[R] (i : ?m.133597), ?m.133599 i)
          ((⨂[R] (i : ?m.133597), ?m.133599 i) →ₗ[R] ⨂[R] (i : ?m.133597), ?m.133599 i))
        mul ∘ₗ
      mul =
    (((LinearMap.llcomp R (⨂[R] (i : ?m.133597), ?m.133599 i)
            ((⨂[R] (i : ?m.133597), ?m.133599 i) →ₗ[R]
              (⨂[R] (i : ?m.133597), ?m.133599 i) →ₗ[R] ⨂[R] (i : ?m.133597), ?m.133599 i)
            ((⨂[R] (i : ?m.133597), ?m.133599 i) →ₗ[R]
              (⨂[R] (i : ?m.133597), ?m.133599 i) →ₗ[R] ⨂[R] (i : ?m.133597), ?m.133599 i))
          LinearMap.lflip)
        ((LinearMap.llcomp R (⨂[R] (i : ?m.133597), ?m.133599 i) (⨂[R] (i : ?m.133597), ?m.133599 i)
              ((⨂[R] (i : ?m.133597), ?m.133599 i) →ₗ[R] ⨂[R] (i : ?m.133597), ?m.133599 i))
            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