-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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'
⊢ 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))
have dsimp : 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) sorry) :
          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: dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]