-- 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)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i_1 : ι × ι
H :
  (((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2))
              (HPow.hPow (α := ℤˣ) (-1) (i.2 * i.1))
              (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) (i.2, i.1) :
                      TensorProduct.{u_1, u_3, u_4} R (𝒜 (i.2, i.1).1) (ℬ (i.2, i.1).2) →ₗ[R]
                        ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
                    (a : 𝒜 (i.2, i.1).1 ⊗[R] ℬ (i.2, i.1).2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
                  (b ⊗ₜ[R] a) :
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2))) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1 =
    ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
              (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (a ⊗ₜ[R] b) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1
H₁ :
  (HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
          (HPow.hPow (α := ℤˣ) (-1) (i.2 * i.1))
          ((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
              (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) (i.2, i.1) :
                    TensorProduct.{u_1, u_3, u_4} R (𝒜 (i.2, i.1).1) (ℬ (i.2, i.1).2) →ₗ[R]
                      ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
                  (a : 𝒜 (i.2, i.1).1 ⊗[R] ℬ (i.2, i.1).2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
                (b ⊗ₜ[R] a)) :
            ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1 =
    ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
              (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (a ⊗ₜ[R] b) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1
H₂ :
  (HPow.hPow (α := ℤˣ) (-1) (i.2 * i.1) •
          HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
            (HPow.hPow (α := ℤˣ) (-1) (i.1 * i.2))
            (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (i.1, i.2) :
                    TensorProduct.{u_1, u_4, u_3} R (ℬ (i.1, i.2).1) (𝒜 (i.1, i.2).2) →ₗ[R]
                      ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
                  (a : ℬ (i.1, i.2).1 ⊗[R] 𝒜 (i.1, i.2).2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
                (a ⊗ₜ[R] b) :
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1 =
    ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
              (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (a ⊗ₜ[R] b) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1
⊢ (((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            ((gradedCommAux R ℬ 𝒜 : (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
              (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                    TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                      ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
                  (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
                (a ⊗ₜ[R] b))) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1 =
    ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
              (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (a ⊗ₜ[R] b) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1
have H₃ : (HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
        (HPow.hPow (α := ℤˣ) (-1) (i.2 * i.1) * HPow.hPow (α := ℤˣ) (-1) (i.1 * i.2))
        (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (i.1, i.2) :
                TensorProduct.{u_1, u_4, u_3} R (ℬ (i.1, i.2).1) (𝒜 (i.1, i.2).2) →ₗ[R]
                  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
              (a : ℬ (i.1, i.2).1 ⊗[R] 𝒜 (i.1, i.2).2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (a ⊗ₜ[R] b) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
      (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
    i_1 =
  ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
              TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
            (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
          (a ⊗ₜ[R] b) :
        ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
      (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
    i_1
Tactic: rw [gradedCommAux_lof_tmul, LinearMap.map_smul_of_tower, gradedCommAux_lof_tmul, smul_smul,
    mul_comm i.2 i.1, Int.units_mul_self, one_smul]