-- 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' : ↥(evenOdd Q i')
obtain :
  ∀ (x' : CliffordAlgebra Q) (hx' : x' ∈ 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))
          (↑(Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') x' hx') : CliffordAlgebra Q) :
        ⨁ (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))
⊢ 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' : CliffordAlgebra Q) :
      ⨁ (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))
        x' :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
obtain ⟨x', hx'⟩ := x'