Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((AlgebraTensorModule.curry
              (((AlgebraTensorModule.curry
                        (((AlgebraTensorModule.curry
                                  ((LinearMap.llcomp R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                        (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                        (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ))
                                      mA ∘ₗ
                                    mA) ∘ₗ
                                lof R ι 𝒜 ixa)
                              xa ∘ₗ
                            lof R ι ℬ ixb)
                          xb) ∘ₗ
                      lof R ι 𝒜 iya)
                    ya ∘ₗ
                  lof R ι ℬ iyb)
                yb) ∘ₗ
            lof R ι 𝒜 iza)
          za ∘ₗ
        lof R ι ℬ izb)
      zb =
    ((AlgebraTensorModule.curry
              (((AlgebraTensorModule.curry
                        (((AlgebraTensorModule.curry
                                  (((LinearMap.llcomp R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                          (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                          (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R]
                                            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ))
                                        ↑LinearMap.lflip)
                                      ((LinearMap.llcomp R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                            (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                                            (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ))
                                          mA.flip ∘ₗ
                                        mA)).flip ∘ₗ
                                lof R ι 𝒜 ixa)
                              xa ∘ₗ
                            lof R ι ℬ ixb)
                          xb) ∘ₗ
                      lof R ι 𝒜 iya)
                    ya ∘ₗ
                  lof R ι ℬ iyb)
                yb) ∘ₗ
            lof R ι 𝒜 iza)
          za ∘ₗ
        lof R ι ℬ izb)
      zb

Tactic:
dsimp [mA]

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((gradedMul R 𝒜 ℬ)
        (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
          ((lof R ι 𝒜 iya) ya ⊗ₜ[R] (lof R ι ℬ iyb) yb)))
      ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb) =
    ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
      (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 iya) ya ⊗ₜ[R] (lof R ι ℬ iyb) yb)) ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb))