-- 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 ℤˣ)
a₁ a₂ : A
i : ι
e_f :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (a₁ ⊗ₜ[R] (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
        𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
        𝒜 ᵍ⊗[R] ℬ)
e_f₁ :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i))
      ((a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
e_f₂ :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
e_f₃ :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) =
    HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1
      ((a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
e_f₄ :
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)) :
      𝒜 ᵍ⊗[R] ℬ)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        HMul.hMul (α := B) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B)
          (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(ℬ i)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) :
      𝒜 ᵍ⊗[R] ℬ)
e_f₅ :
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
          1) :
      𝒜 ᵍ⊗[R] ℬ)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        HMul.hMul (α := B) 1 1 :
      𝒜 ᵍ⊗[R] ℬ)
e_f₆ e_f₇ :
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
          1) :
      𝒜 ᵍ⊗[R] ℬ)
    ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1 :
      𝒜 ᵍ⊗[R] ℬ)
⊢ (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      ((a₁ * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
        1) =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)

Tactic:
rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]

Premises used: uzpow_zero, GradedTensorProduct.tmul_coe_mul_coe_tmul, MulZeroClass.zero_mul, one_smul, SetLike.coe_gOne, one_mul