-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : 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
⊢ HSMul.hSMul (α := R) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (ixb * iya)) : ℤ) : R)
      (HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) ((ixb + iyb) * iza))
        (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) ((lof R ι 𝒜 ixa : (a : 𝒜 ixa) → ⨁ (i : ι), 𝒜 i) xa : ⨁ (i : ι), 𝒜 i)
            (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
              ((lof R ι 𝒜 iya : (a : 𝒜 iya) → ⨁ (i : ι), 𝒜 i) ya : ⨁ (i : ι), 𝒜 i)
              ((lof R ι 𝒜 iza : (a : 𝒜 iza) → ⨁ (i : ι), 𝒜 i) za : ⨁ (i : ι), 𝒜 i)) ⊗ₜ[R]
          HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ ixb : (a : ℬ ixb) → ⨁ (i : ι), ℬ i) xb : ⨁ (i : ι), ℬ i)
            (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ iyb : (a : ℬ iyb) → ⨁ (i : ι), ℬ i) yb : ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ izb : (a : ℬ izb) → ⨁ (i : ι), ℬ i) zb : ⨁ (i : ι), ℬ i)))) =
    HSMul.hSMul (α := R) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (iyb * iza)) : ℤ) : R)
      (HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (ixb * (iya + iza)))
        (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) ((lof R ι 𝒜 ixa : (a : 𝒜 ixa) → ⨁ (i : ι), 𝒜 i) xa : ⨁ (i : ι), 𝒜 i)
            (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
              ((lof R ι 𝒜 iya : (a : 𝒜 iya) → ⨁ (i : ι), 𝒜 i) ya : ⨁ (i : ι), 𝒜 i)
              ((lof R ι 𝒜 iza : (a : 𝒜 iza) → ⨁ (i : ι), 𝒜 i) za : ⨁ (i : ι), 𝒜 i)) ⊗ₜ[R]
          HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ ixb : (a : ℬ ixb) → ⨁ (i : ι), ℬ i) xb : ⨁ (i : ι), ℬ i)
            (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ iyb : (a : ℬ iyb) → ⨁ (i : ι), ℬ i) yb : ⨁ (i : ι), ℬ i)
              ((lof R ι ℬ izb : (a : ℬ izb) → ⨁ (i : ι), ℬ i) zb : ⨁ (i : ι), ℬ i))))
have a : HSMul.hSMul (β := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) (HPow.hPow (α := ℤˣ) (-1) (ixb * iya + (ixb * iza + iyb * iza)))
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) ((lof R ι 𝒜 ixa : (a : 𝒜 ixa) → ⨁ (i : ι), 𝒜 i) xa : ⨁ (i : ι), 𝒜 i)
        (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 iya : (a : 𝒜 iya) → ⨁ (i : ι), 𝒜 i) ya : ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 iza : (a : 𝒜 iza) → ⨁ (i : ι), 𝒜 i) za : ⨁ (i : ι), 𝒜 i)) ⊗ₜ[R]
      HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ ixb : (a : ℬ ixb) → ⨁ (i : ι), ℬ i) xb : ⨁ (i : ι), ℬ i)
        (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ iyb : (a : ℬ iyb) → ⨁ (i : ι), ℬ i) yb : ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ izb : (a : ℬ izb) → ⨁ (i : ι), ℬ i) zb : ⨁ (i : ι), ℬ i))) =
  HSMul.hSMul (α := R) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (iyb * iza)) : ℤ) : R)
    (HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (ixb * iya + ixb * iza))
      (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) ((lof R ι 𝒜 ixa : (a : 𝒜 ixa) → ⨁ (i : ι), 𝒜 i) xa : ⨁ (i : ι), 𝒜 i)
          (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
            ((lof R ι 𝒜 iya : (a : 𝒜 iya) → ⨁ (i : ι), 𝒜 i) ya : ⨁ (i : ι), 𝒜 i)
            ((lof R ι 𝒜 iza : (a : 𝒜 iza) → ⨁ (i : ι), 𝒜 i) za : ⨁ (i : ι), 𝒜 i)) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ ixb : (a : ℬ ixb) → ⨁ (i : ι), ℬ i) xb : ⨁ (i : ι), ℬ i)
          (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
            ((lof R ι ℬ iyb : (a : ℬ iyb) → ⨁ (i : ι), ℬ i) yb : ⨁ (i : ι), ℬ i)
            ((lof R ι ℬ izb : (a : ℬ izb) → ⨁ (i : ι), ℬ i) zb : ⨁ (i : ι), ℬ i))))
Tactic: simp_rw [Int.cast_smul_eq_zsmul R, ← Units.smul_def, smul_smul, ← uzpow_add, add_mul, mul_add]