-- 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
m : M
a :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
a₁ :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 1 : ↥(evenOdd Q 1) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : ↥(evenOdd Q 1)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
a₂ :
  Eq (α := CliffordAlgebra Q)
    ((↑(Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯) :
        CliffordAlgebra Q) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
a₃ a₄ :
  Eq (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((((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))
          ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]

Premises used: Subtype.coe_mk, CliffordAlgebra.lift_ι_apply, DirectSum.coeAlgHom_of, CliffordAlgebra.GradedAlgebra.ι_apply