-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
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))
⊢ (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] ℬ)
have 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] ℬ)
Tactic: rw [← SetLike.coe_gOne ℬ, tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul,
      SetLike.coe_gOne, one_mul]