-- 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
m : M
a :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
a₁ :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 1 : ↥(⋀[R]^1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
a₂ :
  Eq (α := ExteriorAlgebra R M)
    ((↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯) :
        ExteriorAlgebra R M) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
a₃ a₄ :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
⊢ Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((((lift R :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m * (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m = 0 }) →
                    ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
                      0)
                  (GradedAlgebra.ι R M) ⋯) :
              ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : CliffordAlgebra 0) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)

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

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