-- 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 : ℕ
x : TensorAlgebra R M
r : R
algebraMap :
  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)) 0 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ 0)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (((@DirectSum.GAlgebra.toFun _ R
                (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) inst
                (fun (i : ℕ) ↦
                  (HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i).addCommMonoid)
                (fun (i : ℕ) ↦ (HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i).module)
                Nat.instAddMonoid
                (SetLike.gsemiring fun (x : ℕ) ↦
                  HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x)
                _ :
              R →+ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0)) :
            (a : R) → ↥((ι R).range ^ 0))
          r) :
      ⨁ (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)) 0 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ 0)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0)
          ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r) ⋯) :
      ⨁ (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))
        ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r) :
      ⨁ (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)) 0 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ 0)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0)
          ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r) ⋯) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))

Tactic:
rw [AlgHom.commutes, DirectSum.algebraMap_apply]

Premises used: DirectSum.algebraMap_apply, AlgHom.commutes