awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
xi yi : ℕ
x : CliffordAlgebra Q
hx :
  x ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑xi : ZMod 2)) xi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
y : CliffordAlgebra Q
hy :
  y ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑yi : ZMod 2)) yi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
h : x * y ∈ (↑((ι Q).range ^ xi * (ι Q).range ^ yi) : Set (CliffordAlgebra Q))
⊢ x * y ∈
    (↑((ι Q).range ^
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ (↑n : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑xi : ZMod 2) (↑yi : ZMod 2))
                (xi + yi) ⋯) :
            ℕ)) :
      Set (CliffordAlgebra Q))

Tactic:
simp only [pow_add]

Premises used: pow_add
-- 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
xi yi : ℕ
x : CliffordAlgebra Q
hx :
  x ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑xi : ZMod 2)) xi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
y : CliffordAlgebra Q
hy :
  y ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑yi : ZMod 2)) yi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
⊢ x * y ∈ (↑((ι Q).range ^ xi * (ι Q).range ^ yi) : Set (CliffordAlgebra Q))

Tactic:
Submodule.mul_mem_mul hx hy

Premises used: Submodule.mul_mem_mul, Set.Mem
-- 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
xi yi : ℕ
x : CliffordAlgebra Q
hx :
  x ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑xi : ZMod 2)) xi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
y : CliffordAlgebra Q
hy :
  y ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑yi : ZMod 2)) yi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
⊢ x * y ∈ (↑((ι Q).range ^ xi * (ι Q).range ^ yi) : Set (CliffordAlgebra Q))

Tactic:
exact Submodule.mul_mem_mul hx hy

Premises used: Submodule.mul_mem_mul
-- 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
⊢ Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((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) ⋯) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
rfl

Premises used: Set.Mem, DFinsupp.single, rfl
-- 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
rw :
  Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) (HAdd.hAdd (α := ZMod 2) 1 1) :
            ↥(evenOdd Q (HAdd.hAdd (α := ZMod 2) 1 1)) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q (1 + 1))) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (@GradedMonoid.GMul.mul _ (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) Distrib.toAdd _ 1 1
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 0 : ↥(evenOdd Q 0) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q 0)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (((@DirectSum.GAlgebra.toFun _ R (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) CommRing.toCommSemiring
                (fun (i : ZMod 2) ↦ (evenOdd Q i).addCommMonoid) (fun (i : ZMod 2) ↦ (evenOdd Q i).module)
                AddMonoidWithOne.toAddMonoid (SetLike.gsemiring (evenOdd Q)) _ :
              R →+ ↥(evenOdd Q 0)) :
            (a : R) → ↥(evenOdd Q 0))
          ((Q : (a : M) → R) m)) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
⊢ HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((GradedAlgebra.ι Q : (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)

Tactic:
rw [GradedAlgebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply]

Premises used: DirectSum.of_mul_of, DirectSum.algebraMap_apply, CliffordAlgebra.GradedAlgebra.ι_apply
-- 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
⊢ Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) (HAdd.hAdd (α := ZMod 2) 1 1) :
            ↥(evenOdd Q (HAdd.hAdd (α := ZMod 2) 1 1)) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q (1 + 1))) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (@GradedMonoid.GMul.mul _ (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) Distrib.toAdd _ 1 1
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 0 : ↥(evenOdd Q 0) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q 0)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (((@DirectSum.GAlgebra.toFun _ R (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) CommRing.toCommSemiring
                (fun (i : ZMod 2) ↦ (evenOdd Q i).addCommMonoid) (fun (i : ZMod 2) ↦ (evenOdd Q i).module)
                AddMonoidWithOne.toAddMonoid (SetLike.gsemiring (evenOdd Q)) _ :
              R →+ ↥(evenOdd Q 0)) :
            (a : R) → ↥(evenOdd Q 0))
          ((Q : (a : M) → R) m)) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _)

Premises used: Sigma.subtype_ext, CliffordAlgebra.ι_sq_scalar, DirectSum.of_eq_of_gradedMonoid_eq, rfl
-- 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
⊢ Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) (HAdd.hAdd (α := ZMod 2) 1 1) :
            ↥(evenOdd Q (HAdd.hAdd (α := ZMod 2) 1 1)) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q (1 + 1))) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (@GradedMonoid.GMul.mul _ (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) Distrib.toAdd _ 1 1
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 0 : ↥(evenOdd Q 0) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q 0)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (((@DirectSum.GAlgebra.toFun _ R (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) CommRing.toCommSemiring
                (fun (i : ZMod 2) ↦ (evenOdd Q i).addCommMonoid) (fun (i : ZMod 2) ↦ (evenOdd Q i).module)
                AddMonoidWithOne.toAddMonoid (SetLike.gsemiring (evenOdd Q)) _ :
              R →+ ↥(evenOdd Q 0)) :
            (a : R) → ↥(evenOdd Q 0))
          ((Q : (a : M) → R) m)) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _)
-- 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
i : { n : ℕ // (↑n : ZMod 2) = i' }
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ (↑i : ℕ)
mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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))

Tactic:
obtain ⟨i, rfl⟩ := i

Premises used: rfl
-- 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
x' x : CliffordAlgebra Q
i : ℕ
r : R
mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [AlgHom.commutes, DirectSum.algebraMap_apply]

Premises used: DirectSum.algebraMap_apply, AlgHom.commutes
-- 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
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- 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
x' x_1 : CliffordAlgebra Q
i_1 : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ (ι Q).range ^ i
hy : y ∈ (ι Q).range ^ i
ihx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ihy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [map_add, ihx, ihy, ← map_add]

Premises used: map_add
-- 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
x' x_1 : CliffordAlgebra Q
i_1 : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ (ι Q).range ^ i
hy : y ∈ (ι Q).range ^ i
ihx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ihy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- 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
x' x_1 : CliffordAlgebra Q
i_1 : ℕ
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨_, rfl⟩ := hm

Premises used: rfl
-- 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
x' x_1 : CliffordAlgebra Q
i_1 i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
w : M
mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]

Premises used: CliffordAlgebra.lift_ι_apply, DirectSum.of_mul_of, CliffordAlgebra.GradedAlgebra.ι_apply, map_mul
-- 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
x' x_1 : CliffordAlgebra Q
i_1 i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
w : M
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_)

Premises used: Sigma.subtype_ext, DirectSum.of_eq_of_gradedMonoid_eq
-- 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
x' x_1 : CliffordAlgebra Q
i_1 i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
w : M
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- 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
zero :
  Eq (α := ⨁ (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))
⊢ 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))

Tactic:
rw [map_zero]

Premises used: map_zero
-- 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
zero :
  Eq (α := ⨁ (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))
    (0 : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
⊢ Eq (α := ⨁ (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))

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- 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
zero : Eq (α := ↥(evenOdd Q i')) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 ⋯) 0
⊢ Eq (α := ⨁ (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))
    (0 : ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
apply DFinsupp.single_eq_zero.mpr

Premises used: Iff.mpr, DFinsupp.single_eq_zero
-- 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
⊢ Eq (α := ↥(evenOdd Q i')) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 ⋯) 0

Tactic:
rfl
-- 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 →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)

Tactic:
apply GradedAlgebra.ι Q

Premises used: CliffordAlgebra.GradedAlgebra.ι
-- 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),
    HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        ((GradedAlgebra.ι Q : (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)

Tactic:
apply GradedAlgebra.ι_sq_scalar Q

Premises used: CliffordAlgebra.GradedAlgebra.ι_sq_scalar
-- 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
a :
  ∀ (m : M),
    Eq (α := CliffordAlgebra Q)
      ((AlgHom.toLinearMap
                (AlgHom.comp (DirectSum.coeAlgHom (evenOdd 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) ⋯))) ∘ₗ
              ι Q :
            (a : M) → CliffordAlgebra Q)
          m :
        CliffordAlgebra Q)
      ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) m :
        CliffordAlgebra Q)
⊢ AlgHom.comp (DirectSum.coeAlgHom (evenOdd 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) ⋯)) =
    AlgHom.id R (CliffordAlgebra Q)

Tactic:
ext m