-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
mem :
  ∀ (i : { n : ℕ // (↑n : ZMod 2) = i' }) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ (↑i : ℕ)),
    Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((((lift Q :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                              (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                            (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                              ((Q : (a : M) → R) m) }) →
                    CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                      (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((Q : (a : M) → R) m))
                  (GradedAlgebra.ι Q) ⋯) :
              CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          x :
        ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i' : ↥(evenOdd Q i') →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : ↥(evenOdd Q i')) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') x ⋯) :
        ⨁ (i : ZMod 2), ↥(evenOdd Q i))
zero :
  Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    ((((lift Q :
                (a :
                    { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                      ∀ (m : M),
                        (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                            (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                          (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                            ((Q : (a : M) → R) m) }) →
                  CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
              (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                ∀ (m : M),
                  HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                      ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                      ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                    (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                      ((Q : (a : M) → R) m))
                (GradedAlgebra.ι Q) ⋯) :
            CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        0 :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i' : ↥(evenOdd Q i') →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q i')) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 ⋯) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
add :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Membership.mem (γ := Submodule R (CliffordAlgebra Q))
        (⨆ (i : { n : ℕ // (↑n : ZMod 2) = i' }), (ι Q).range ^ (↑i : ℕ)) x)
    (hy :
      Membership.mem (γ := Submodule R (CliffordAlgebra Q))
        (⨆ (i : { n : ℕ // (↑n : ZMod 2) = i' }), (ι Q).range ^ (↑i : ℕ)) y)
    (ihx :
      Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        ((((lift Q :
                    (a :
                        { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                          ∀ (m : M),
                            (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                                (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                              (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                                ((Q : (a : M) → R) m) }) →
                      CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                  (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                    ∀ (m : M),
                      HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                          ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                          ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                        (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                          ((Q : (a : M) → R) m))
                    (GradedAlgebra.ι Q) ⋯) :
                CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
              (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
            x :
          ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i' : ↥(evenOdd Q i') →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
              (a : ↥(evenOdd Q i')) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
            (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') x hx) :
          ⨁ (i : ZMod 2), ↥(evenOdd Q i)))
    (ihy :
      Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        ((((lift Q :
                    (a :
                        { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                          ∀ (m : M),
                            (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                                (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                              (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                                ((Q : (a : M) → R) m) }) →
                      CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                  (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                    ∀ (m : M),
                      HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                          ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                          ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                        (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                          ((Q : (a : M) → R) m))
                    (GradedAlgebra.ι Q) ⋯) :
                CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
              (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
            y :
          ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i' : ↥(evenOdd Q i') →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
              (a : ↥(evenOdd Q i')) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
            (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') y hy) :
          ⨁ (i : ZMod 2), ↥(evenOdd Q i))),
    Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((((lift Q :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                              (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                            (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                              ((Q : (a : M) → R) m) }) →
                    CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                      (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((Q : (a : M) → R) m))
                  (GradedAlgebra.ι Q) ⋯) :
              CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (x + y) :
        ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i' : ↥(evenOdd Q i') →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : ↥(evenOdd Q i')) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') (x + y) ⋯) :
        ⨁ (i : ZMod 2), ↥(evenOdd Q i))
⊢ Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    ((((lift Q :
                (a :
                    { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                      ∀ (m : M),
                        (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                            (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                          (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                            ((Q : (a : M) → R) m) }) →
                  CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
              (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                ∀ (m : M),
                  HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                      ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                      ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                    (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                      ((Q : (a : M) → R) m))
                (GradedAlgebra.ι Q) ⋯) :
            CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        x' :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i' : ↥(evenOdd Q i') →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q i')) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') x' hx') :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
induction hx' using Submodule.iSup_induction' with
  | mem i x hx =>
    obtain ⟨i, rfl⟩ := i
    dsimp only [Subtype.coe_mk] at hx
    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 Q, DirectSum.of_mul_of]
      refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_) <;>
        dsimp only [GradedMonoid.mk, Subtype.coe_mk]
      · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
      rfl
  | zero =>
    rw [map_zero]
    apply Eq.symm
    apply DFinsupp.single_eq_zero.mpr; rfl
  | add x y hx hy ihx ihy =>
    rw [map_add, ihx, ihy, ← map_add]; rfl

Premises used: Subtype.coe_mk, Iff.mpr, CliffordAlgebra.lift_ι_apply, Nat.succ_eq_add_one, Algebra.algebraMap, Sigma.subtype_ext, DirectSum.of_mul_of, DirectSum.algebraMap_apply, map_zero, map_add, CliffordAlgebra.GradedAlgebra.ι_apply, add_comm, Nat.cast_add, map_mul, AlgHom.commutes, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, DFinsupp.single_eq_zero, Nat.cast_one, rfl, GradedMonoid.mk