-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x
algebraMap :
  ∀ (r : R),
    Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          ((Algebra.algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 0 : ↥(⋀[R]^0 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^0 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^0 M) x)
            ((Algebra.algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) ⋯) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
add :
  ∀ (x y : ExteriorAlgebra R M) (i : ℕ)
    (hx : x ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i)
    (hy : y ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i)
    (ihx :
      Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
        ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x : ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
              (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
            (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
          ⨁ (i : ℕ), ↥(⋀[R]^i M)))
    (ihy :
      Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
        ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) y : ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
              (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
            (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) y hy) :
          ⨁ (i : ℕ), ↥(⋀[R]^i M))),
    Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) (x + y) : ⨁ (i : ℕ), ↥(⋀[R]^i M))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) (x + y) ⋯) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
mem_mul :
  ∀ (m : ExteriorAlgebra R M) (hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) m)
    (i : ℕ) (x : ExteriorAlgebra R M)
    (hx : x ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i)
    (ih :
      Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
        ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x : ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
              (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
            (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
          ⨁ (i : ℕ), ↥(⋀[R]^i M))),
    Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) (m * x) : ⨁ (i : ℕ), ↥(⋀[R]^i M))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i.succ : ↥(⋀[R]^i.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^i.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i.succ M) x) (m * x) ⋯) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
induction hx using Submodule.pow_induction_on_left' with
  | algebraMap => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
  | add _ _ _ _ _ ihx ihy => simp_rw [map_add, ihx, ihy, ← map_add]; rfl
  | mem_mul _ hm _ _ _ ih =>
      obtain ⟨_, rfl⟩ := hm
      simp_rw [map_mul, ih, GradedAlgebra.liftι, 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, ExteriorAlgebra.lift_ι_apply, DirectSum.of_mul_of, DirectSum.algebraMap_apply, map_add, add_comm, map_mul, AlgHom.commutes, DirectSum.of_eq_of_gradedMonoid_eq, ExteriorAlgebra.GradedAlgebra.ι_apply, ExteriorAlgebra.GradedAlgebra.liftι, rfl