-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i_1 : ℕ
x_1 : TensorAlgebra R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i
ih :
  Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    ((((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
              (GradedAlgebra.ι R M) :
            TensorAlgebra R M →ₐ[R]
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        x :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) i :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ i)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
w : M
mem_mul :
  Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
              (1 + i) :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) (1 + i)) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ (1 + i))) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (@GradedMonoid.GMul.mul _
          (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) instAddNat _ 1 i
          (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
            ((ι R : (a : M) → TensorAlgebra R M) w) ⋯)
          (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx)) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
              i.succ :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i.succ) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ i.succ)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i.succ)
          (HMul.hMul (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) w : TensorAlgebra R M) x) ⋯) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
⊢ Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    ((((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
              (GradedAlgebra.ι R M) :
            TensorAlgebra R M →ₐ[R]
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (HMul.hMul (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) w : TensorAlgebra R M) x) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
              i.succ :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i.succ) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ i.succ)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i.succ)
          (HMul.hMul (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) w : TensorAlgebra R M) x) ⋯) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))

Tactic:
rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]

Premises used: DirectSum.of_mul_of, TensorAlgebra.lift_ι_apply, map_mul, TensorAlgebra.GradedAlgebra.ι_apply