-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
simp_rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (HMul.hMul (α := A) (β := A)
              ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
                  ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i)) :
                A)
              ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
                  (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                        (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                      a₂ :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                A) ⊗ₜ[R]
            HMul.hMul (α := B) (β := B)
              ((Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
                  (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                        (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                      b₁ :
                    ⨁ (i : ι), ↥(ℬ i)) :
                B)
              ((Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
                  ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)) :
                B)) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
simp_rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (HMul.hMul (α := A)
              ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
                  ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i)) :
                A)
              (↑a₂ : A) ⊗ₜ[R]
            HMul.hMul (β := B) (↑b₁ : B)
              ((Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
                  ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)) :
                B)) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
⊢ HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
              (HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i))
                (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                    a₂ :
                  ⨁ (i : ι), ↥(𝒜 i))) ⊗ₜ[R]
            (Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
              (HMul.hMul (α := ⨁ (i : ι), ↥(ℬ i)) (β := ⨁ (i : ι), ↥(ℬ i))
                (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                      (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                    b₁ :
                  ⨁ (i : ι), ↥(ℬ i))
                ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)))) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)

Tactic:
simp_rw [decompose_symm_mul, decompose_symm_of, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, DirectSum.decompose_symm_mul, DirectSum.decompose_symm_of