-- 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
hx : x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i
algebraMap :
  ∀ (r : R),
    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))
add :
  ∀ (x y : TensorAlgebra R M) (i : ℕ)
    (hx : x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)
    (hy : y ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)
    (ihx :
      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)))
    (ihy :
      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))
            y :
          ⨁ (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) y hy) :
          ⨁ (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))
          (x + y) :
        ⨁ (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 + y) ⋯) :
        ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
mem_mul :
  ∀ (m : TensorAlgebra R M) (hm : Membership.mem (γ := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι 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))),
    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))
          (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) (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))
        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))

Tactic:
induction hx using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
    | add x y i hx hy ihx ihy =>
      rw [map_add, ihx, ihy, ← map_add]
      rfl
    | mem_mul m hm i x hx ih =>
      obtain ⟨_, rfl⟩ := hm
      rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
      exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

Premises used: Algebra.algebraMap, Sigma.subtype_ext, DirectSum.of_mul_of, TensorAlgebra.lift_ι_apply, DirectSum.algebraMap_apply, map_add, add_comm, map_mul, TensorAlgebra.GradedAlgebra.ι_apply, AlgHom.commutes, DirectSum.of_eq_of_gradedMonoid_eq, rfl