import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
import Mathlib.LinearAlgebra.CliffordAlgebra.Grading
import Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
import Mathlib.RingTheory.FiniteType
import Mathlib.Tactic
-- import Mathlib.Util.Superscript
-- import Mathlib.Data.Matrix.Notation

open Module (finrank: (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank finrank_eq_card_basis: ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StrongRankCondition R] {ι : Type w} [inst_4 : Fintype ι], Basis ι R M → finrank R M = Fintype.card ι
finrank_eq_card_basis finrank_directSum: ∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] (M : ι → Type w)
  [inst_3 : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module R (M i)] [inst_5 : ∀ (i : ι), Module.Free R (M i)]
  [inst_6 : ∀ (i : ι), Module.Finite R (M i)], finrank R (DirectSum ι fun i => M i) = ∑ i : ι, finrank R (M i)
finrank_directSum rank_self: ∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R], Module.rank R R = 1
rank_self)

set_option quotPrecheck false

variable {R: Type u_1
R M: Type u_2
M : Type*: Type (u_1 + 1)
Type*} [CommRing: Type u_1 → Type u_1
CommRing R: Type u_1
R] [AddCommGroup: Type u_2 → Type u_2
AddCommGroup M: Type u_2
M] [Module: (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max u_1 u_2)
Module R: Type u_1
R M: Type u_2
M]

variable {Q: QuadraticForm R M
Q : QuadraticForm: (R : Type u_1) →
  (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max u_1 u_2)
QuadraticForm R: Type u_1
R M: Type u_2
M}

variable [Invertible: {α : Type u_1} → [inst : Mul α] → [inst : One α] → α → Type u_1
Invertible (2: R
2 : R: Type u_1
R)]

variable [Invertible: {α : Type (max u_1 u_2)} → [inst : Mul α] → [inst : One α] → α → Type (max u_1 u_2)
Invertible (2: Cl
2 : CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q)]

variable (u: CliffordAlgebra Q
u v: Cl
v w: Cl
w : CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q)

local notation "Cl" => CliffordAlgebra Q

local instance hasCoeCliffordAlgebraRing: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Coe R Cl
hasCoeCliffordAlgebraRing : Coe: semiOutParam (Type u_1) → Type (max u_2 u_1) → Type (max (max 0 u_1) u_2 u_1)
Coe R: Type u_1
R Cl: Type (max u_2 u_1)
Cl := ⟨algebraMap: (R : Type u_1) →
  (A : Type (max u_2 u_1)) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → R →+* A
algebraMap R: Type u_1
R (Cl: Type (max u_2 u_1)
Cl)⟩
local instance hasCoeCliffordAlgebraModule: Coe M Cl
hasCoeCliffordAlgebraModule : Coe: semiOutParam (Type u_2) → Type (max u_2 u_1) → Type (max (max 0 u_2) u_2 u_1)
Coe M: Type u_2
M Cl: Type (max u_2 u_1)
Cl := ⟨CliffordAlgebra.ι: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → M →ₗ[R] Cl
CliffordAlgebra.ι Q: QuadraticForm R M
Q⟩

local notation "G0" => (algebraMap R Cl).range
local notation "G1" => LinearMap.range (CliffordAlgebra.ι Q)

lemma mul_eq_half_add_sub: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} [inst_3 : Invertible 2] [inst_4 : Invertible 2] (u v : Cl),
  u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u)
mul_eq_half_add_sub : u: Cl
u * v: Cl
v = ⅟2: Cl
2 * (u: Cl
u * v: Cl
v + v: Cl
v * u: Cl
u) + ⅟2: Cl
2 * (u: Cl
u * v: Cl
v - v: Cl
v * u: Cl
u) :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false` byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
  calc
    u: Cl
u * v: Cl
v = 1: Cl
1 * (u: Cl
u * v: Cl
v)                                             :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙 rw [Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = 1 * (u * v)one_mul: ∀ {M : Type (max u_1 u_2)} [inst : MulOneClass M] (a : M), 1 * a = a
one_mulWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = u * v]Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
        _: Cl_: Cl
_ = (⅟2: Cl
2 * 2: Cl
2) * (u: Cl
u * v: Cl
v)                                      :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙 rw [Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
1 * (u * v) = ⅟2 * 2 * (u * v)invOf_mul_self': ∀ {α : Type (max u_1 u_2)} [inst : Mul α] [inst_1 : One α] (a : α) {x : Invertible a}, ⅟a * a = 1
invOf_mul_self'Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
1 * (u * v) = 1 * (u * v)]Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
        _: Cl_: Cl
_ = ⅟2: Cl
2 * (2: Cl
2 * (u: Cl
u * v: Cl
v))                                      :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙 rw [Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * 2 * (u * v) = ⅟2 * (2 * (u * v))mul_assoc: ∀ {G : Type ?u.140475} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assocWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (2 * (u * v)) = ⅟2 * (2 * (u * v))]Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
        _: Cl_: Cl
_ = ⅟2: Cl
2 * (u: Cl
u * v: Cl
v + u: Cl
u * v: Cl
v)                                    :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙 rw [Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (2 * (u * v)) = ⅟2 * (u * v + u * v)←two_mul: ∀ {α : Type (max u_1 u_2)} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n
two_mulWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (2 * (u * v)) = ⅟2 * (2 * (u * v))]Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
        _: Cl_: Cl
_ = ⅟2: Cl
2 * ((u: Cl
u * v: Cl
v + v: Cl
v * u: Cl
u) + (u: Cl
u * v: Cl
v - v: Cl
v * u: Cl
u))                :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙 rw [Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (u * v + u * v) = ⅟2 * (u * v + v * u + (u * v - v * u))add_add_sub_cancel: ∀ {G : Type (max u_1 u_2)} [inst : AddCommGroup G] (a b c : G), a + c + (b - c) = a + b
add_add_sub_cancelWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (u * v + u * v) = ⅟2 * (u * v + u * v)]Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
        _: Cl_: Cl
_ = ⅟2: Cl
2 * (u: Cl
u * v: Cl
v + v: Cl
v * u: Cl
u) + ⅟2: Cl
2 * (u: Cl
u * v: Cl
v - v: Cl
v * u: Cl
u)             :=Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) byWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙 rw [Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (u * v + v * u + (u * v - v * u)) = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u)mul_add: ∀ {R : Type (max u_1 u_2)} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
  a * (b + c) = a * b + a * c
mul_addWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v: Cl
⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u)]Warning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
  doneWarning: automatically included section variable(s) unused in theorem 'mul_eq_half_add_sub':
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

#checkmul_eq_half_add_sub.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M]
  {Q : QuadraticForm R M} [Invertible 2] [Invertible 2] (u v : Cl) : u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u) mul_eq_half_add_sub: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} [inst_3 : Invertible 2] [inst_4 : Invertible 2] (u v : Cl),
  u * v = ⅟2 * (u * v + v * u) + ⅟2 * (u * v - v * u)
mul_eq_half_add_sub

Axiom 1. G is a ring with unit. The additive identity is called 0 and the multiplicative identity is called 1.

#checkCliffordAlgebra.instRing.{u_1, u_2} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M) : Ring Cl CliffordAlgebra.instRing: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Ring Cl
CliffordAlgebra.instRing
example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (u : Cl), 0 + u = u
example : 0: Cl
0 + u: Cl
u = u: Cl
u := byGoals accomplished! 🐙 rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
0 + u = uzero_add: ∀ {M : Type (max u_1 u_2)} [inst : AddZeroClass M] (a : M), 0 + a = a
zero_addR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
u = u]Goals accomplished! 🐙
example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (u : Cl), u + 0 = u
example : u: Cl
u + 0: Cl
0 = u: Cl
u := byGoals accomplished! 🐙 rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
u + 0 = uadd_zero: ∀ {M : Type ?u.177426} [inst : AddZeroClass M] (a : M), a + 0 = a
add_zeroR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
u = u]Goals accomplished! 🐙
example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (u : Cl), 1 * u = u
example : 1: Cl
1 * u: Cl
u = u: Cl
u := byGoals accomplished! 🐙 rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
1 * u = uone_mul: ∀ {M : Type ?u.186051} [inst : MulOneClass M] (a : M), 1 * a = a
one_mulR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
u = u]Goals accomplished! 🐙
example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (u : Cl), u * 1 = u
example : u: Cl
u * 1: Cl
1 = u: Cl
u := byGoals accomplished! 🐙 rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
u * 1 = umul_one: ∀ {M : Type ?u.195736} [inst : MulOneClass M] (a : M), a * 1 = a
mul_oneR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
u = u]Goals accomplished! 🐙

Axiom 2. G contains a ~~field~~ring G0 of characteristic zero which includes 0 and 1.

-- [Field R]
-- [DivisionRing R] [CharZero R]

#check(algebraMap R Cl).range : Subring Cl G0: Subring Cl
G0

local notation "𝟘" => (0 : Cl)
local notation "𝟙" => (1 : Cl)

-- local notation "𝒢" => algebraMap R (CliffordAlgebra Q)
-- #check 𝒢
#check0 : Cl 𝟘: Cl
𝟘
#check1 : Cl 𝟙: Cl
𝟙

Axiom 3. G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.

#checkM : Type u_2 M: Type u_2
M
#checkG1 : Submodule R Cl G1: Submodule R Cl
G1

example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (u : Cl) {r : Cl}, r ∈ (algebraMap R Cl).range ∧ u ∈ G1 → r • u ∈ G1
example : r: Cl
r ∈ G0: Subring Cl
G0 ∧ u: Cl
u ∈ G1: Submodule R Cl
G1 → r: Cl
r • u: Cl
u ∈ G1: Submodule R Cl
G1 := byGoals accomplished! 🐙
  rintro ⟨hr, hu⟩: r ∈ (algebraMap R Cl).range ∧ u ∈ G1
⟨hr: r ∈ (algebraMap R Cl).range
hr⟨hr, hu⟩: r ∈ (algebraMap R Cl).range ∧ u ∈ G1
, hu: u ∈ G1
hu⟨hr, hu⟩: r ∈ (algebraMap R Cl).range ∧ u ∈ G1
⟩R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: r ∈ (algebraMap R Cl).range
hu: u ∈ G1
intror • u ∈ G1
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: r ∈ (algebraMap R Cl).range
hu: u ∈ G1
intror • u ∈ G1LinearMap.mem_range: ∀ {R : Type ?u.321810} {R₂ : Type ?u.321809} {M : Type ?u.321808} {M₂ : Type ?u.321807} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type ?u.321806} [inst_6 : FunLike F M M₂]
  [inst_7 : SemilinearMapClass F τ₁₂ M M₂] [inst_8 : RingHomSurjective τ₁₂] {f : F} {x : M₂},
  x ∈ LinearMap.range f ↔ ∃ y, f y = x
LinearMap.mem_rangeR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: r ∈ (algebraMap R Cl).range
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u]R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: r ∈ (algebraMap R Cl).range
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u at *R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: r ∈ (algebraMap R Cl).range
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: r ∈ (algebraMap R Cl).range
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • uRingHom.mem_range: ∀ {R : Type ?u.341124} {S : Type ?u.341123} [inst : Ring R] [inst_1 : Ring S] {f : R →+* S} {y : S},
  y ∈ f.range ↔ ∃ x, f x = y
RingHom.mem_rangeR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: ∃ x, (algebraMap R Cl) x = r
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u]R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: ∃ x, (algebraMap R Cl) x = r
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u at hr: r ∈ (algebraMap R Cl).range
hrR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: ∃ x, (algebraMap R Cl) x = r
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u
  let ⟨r': R
r', hr': (algebraMap R Cl) r' = r
hr'⟩ := hr: ∃ x, (algebraMap R Cl) x = r
hrR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: ∃ x, (algebraMap R Cl) x = r
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
r': R
hr': (algebraMap R Cl) r' = r
intro∃ y, (CliffordAlgebra.ι Q) y = r • u
  let ⟨u': M
u', hu': (CliffordAlgebra.ι Q) u' = u
hu'⟩ := hu: ∃ y, (CliffordAlgebra.ι Q) y = u
huR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: ∃ x, (algebraMap R Cl) x = r
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
r': R
hr': (algebraMap R Cl) r' = r
u': M
hu': (CliffordAlgebra.ι Q) u' = u
intro∃ y, (CliffordAlgebra.ι Q) y = r • u
  use (r': R
r' • u': M
u')R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w, r: Cl
hr: ∃ x, (algebraMap R Cl) x = r
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
r': R
hr': (algebraMap R Cl) r' = r
u': M
hu': (CliffordAlgebra.ι Q) u' = u
h(CliffordAlgebra.ι Q) (r' • u') = r • u
  simp only [← hr': (algebraMap R Cl) r' = r
hr', ← hu': (CliffordAlgebra.ι Q) u' = u
hu', map_smul: ∀ {F : Type ?u.342963} {M : Type ?u.342962} {X : Type ?u.342961} {Y : Type ?u.342960} [inst : SMul M X]
  [inst_1 : SMul M Y] [inst_2 : FunLike F X Y] [inst_3 : MulActionHomClass F M X Y] (f : F) (c : M) (x : X),
  f (c • x) = c • f x
map_smul, smul_eq_mul: ∀ (α : Type ?u.343001) [inst : Mul α] {a a' : α}, a • a' = a * a'
smul_eq_mul, Algebra.smul_def: ∀ {R : Type ?u.343018} {A : Type ?u.343017} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R)
  (x : A), r • x = (algebraMap R A) r * x
Algebra.smul_def]Goals accomplished! 🐙
  doneWarning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

-- local notation "ι" => CliffordAlgebra.ι Q

-- #check @Mul.mul Cl _

-- local notation "∘" => @Mul.mul Cl _

-- example (r : R) (u : M)  : r ∘ u = u ∘ r := by rw [@Algebra.commutes]

-- local notation "*" => fun x y => (CliffordAlgebra Q).mul ↑x ↑y

-- abbrev 𝒢 := CliffordAlgebra Q
-- abbrev Cl := CliffordAlgebra Q
-- def Cl := CliffordAlgebra Q

/-
Cl.{u_2, u_1} {R : Type u_1} {M : Type u_2} [inst✝ : CommRing R] [inst✝¹ : AddCommGroup M] [inst✝² : Module R M]
  {Q : QuadraticForm R M} : Type (max u_2 u_1)
-/
-- #check Cl

-- local notation "𝐶𝑙" => CliffordAlgebra Q
-- local notation "𝒢" => CliffordAlgebra Q
-- local notation "𝔊" => CliffordAlgebra Q
-- local notation:50 A " =[" T:50 "] " B:50 => @Eq T A B
-- local notation:50 A "=ₐ" B:50 => @Eq 𝐶𝑙 A B


local notation:50 A "=" B:50 ":" T:50 => @Eq T A B

example (u v: M) : ∃ w : M, w = u + v : Cl := byGoals accomplished! 🐙
  use (u: M
u + v: M
v)R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w: Cl
u, v: M
h(CliffordAlgebra.ι Q) (u + v) = (CliffordAlgebra.ι Q) u + (CliffordAlgebra.ι Q) v
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w: Cl
u, v: M
h(CliffordAlgebra.ι Q) (u + v) = (CliffordAlgebra.ι Q) u + (CliffordAlgebra.ι Q) vmap_add: ∀ {M : Type ?u.375019} {N : Type ?u.375018} {F : Type ?u.375017} [inst : Add M] [inst_1 : Add N]
  [inst_2 : FunLike F M N] [inst_3 : AddHomClass F M N] (f : F) (x y : M), f (x + y) = f x + f y
map_addR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w: Cl
u, v: M
h(CliffordAlgebra.ι Q) u + (CliffordAlgebra.ι Q) v = (CliffordAlgebra.ι Q) u + (CliffordAlgebra.ι Q) v]Goals accomplished! 🐙

example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, ∀ u ∈ G1, ∀ v ∈ G1, u + v ∈ G1
example : ∀ u: Cl
u ∈ G1: Submodule R Cl
G1, ∀ v: Cl
v ∈ G1: Submodule R Cl
G1, u: Cl
u + v: Cl
v ∈ G1: Submodule R Cl
G1 := byGoals accomplished! 🐙
  intros u: Cl
u hu: u ∈ G1
hu v: Cl
v hv: v ∈ G1
hvR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u + v ∈ G1
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u + v ∈ G1LinearMap.mem_range: ∀ {R : Type ?u.395814} {R₂ : Type ?u.395813} {M : Type ?u.395812} {M₂ : Type ?u.395811} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type ?u.395810} [inst_6 : FunLike F M M₂]
  [inst_7 : SemilinearMapClass F τ₁₂ M M₂] [inst_8 : RingHomSurjective τ₁₂] {f : F} {x : M₂},
  x ∈ LinearMap.range f ↔ ∃ y, f y = x
LinearMap.mem_rangeR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
∃ y, (CliffordAlgebra.ι Q) y = u + v]R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
∃ y, (CliffordAlgebra.ι Q) y = u + v
  obtain: ∃ u', (CliffordAlgebra.ι Q) u' = u
obtain ⟨u', hu'⟩: ∃ u', (CliffordAlgebra.ι Q) u' = u
⟨u': M
u'⟨u', hu'⟩: ∃ u', (CliffordAlgebra.ι Q) u' = u
, hu': (CliffordAlgebra.ι Q) u' = u
hu'⟨u', hu'⟩: ∃ u', (CliffordAlgebra.ι Q) u' = u
⟩ : ∃ u': M
u' : M: Type u_2
M, u': M
u' = u: Cl
u :=R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
∃ y, (CliffordAlgebra.ι Q) y = u + v byGoals accomplished! 🐙
    rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
∃ u', (CliffordAlgebra.ι Q) u' = uLinearMap.mem_range: ∀ {R R₂ : Type u_1} {M : Type u_2} {M₂ : Type (max u_1 u_2)} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {F : Type (max u_1 u_2)} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
  [inst_8 : RingHomSurjective τ₁₂] {f : F} {x : M₂}, x ∈ LinearMap.range f ↔ ∃ y, f y = x
LinearMap.mem_rangeR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
v: Cl
hv: v ∈ G1
∃ u', (CliffordAlgebra.ι Q) u' = u]R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
v: Cl
hv: v ∈ G1
∃ u', (CliffordAlgebra.ι Q) u' = u at hu: u ∈ G1
huR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: ∃ y, (CliffordAlgebra.ι Q) y = u
v: Cl
hv: v ∈ G1
∃ u', (CliffordAlgebra.ι Q) u' = u
    exact hu: ∃ y, (CliffordAlgebra.ι Q) y = u
huGoals accomplished! 🐙
  obtain: ∃ v', (CliffordAlgebra.ι Q) v' = v
obtain ⟨v', hv'⟩: ∃ v', (CliffordAlgebra.ι Q) v' = v
⟨v': M
v'⟨v', hv'⟩: ∃ v', (CliffordAlgebra.ι Q) v' = v
, hv': (CliffordAlgebra.ι Q) v' = v
hv'⟨v', hv'⟩: ∃ v', (CliffordAlgebra.ι Q) v' = v
⟩ : ∃ v': M
v' : M: Type u_2
M, v': M
v' = v: Cl
v :=R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
intro∃ y, (CliffordAlgebra.ι Q) y = u + v byGoals accomplished! 🐙
    rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
∃ v', (CliffordAlgebra.ι Q) v' = vLinearMap.mem_range: ∀ {R R₂ : Type u_1} {M : Type u_2} {M₂ : Type (max u_1 u_2)} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {F : Type (max u_1 u_2)} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
  [inst_8 : RingHomSurjective τ₁₂] {f : F} {x : M₂}, x ∈ LinearMap.range f ↔ ∃ y, f y = x
LinearMap.mem_rangeR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: ∃ y, (CliffordAlgebra.ι Q) y = v
u': M
hu': (CliffordAlgebra.ι Q) u' = u
∃ v', (CliffordAlgebra.ι Q) v' = v]R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: ∃ y, (CliffordAlgebra.ι Q) y = v
u': M
hu': (CliffordAlgebra.ι Q) u' = u
∃ v', (CliffordAlgebra.ι Q) v' = v at hv: v ∈ G1
hvR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: ∃ y, (CliffordAlgebra.ι Q) y = v
u': M
hu': (CliffordAlgebra.ι Q) u' = u
∃ v', (CliffordAlgebra.ι Q) v' = v
    exact hv: ∃ y, (CliffordAlgebra.ι Q) y = v
hvGoals accomplished! 🐙
  use (u': M
u' + v': M
v')R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
h(CliffordAlgebra.ι Q) (u' + v') = u + v
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
h(CliffordAlgebra.ι Q) (u' + v') = u + vmap_add: ∀ {M : Type u_2} {N F : Type (max u_1 u_2)} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F) (x y : M), f (x + y) = f x + f y
map_addR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
h(CliffordAlgebra.ι Q) u' + (CliffordAlgebra.ι Q) v' = u + v]R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
h(CliffordAlgebra.ι Q) u' + (CliffordAlgebra.ι Q) v' = u + v
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
h(CliffordAlgebra.ι Q) u' + (CliffordAlgebra.ι Q) v' = u + vhu': (CliffordAlgebra.ι Q) u' = u
hu',R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
hu + (CliffordAlgebra.ι Q) v' = u + v hv': (CliffordAlgebra.ι Q) v' = v
hv'R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v✝, w, u: Cl
hu: u ∈ G1
v: Cl
hv: v ∈ G1
u': M
hu': (CliffordAlgebra.ι Q) u' = u
v': M
hv': (CliffordAlgebra.ι Q) v' = v
hu + v = u + v]Goals accomplished! 🐙
  doneWarning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (r : R) (u : M),
  (algebraMap R Cl) r * (CliffordAlgebra.ι Q) u = (CliffordAlgebra.ι Q) u * (algebraMap R Cl) r
example (r: R
r : R: Type u_1
R) (u: M
u : M: Type u_2
M) : r: R
r * u: M
u = u: M
u * r: R
r : Cl: Type (max u_2 u_1)
Cl := byGoals accomplished! 🐙 rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
(algebraMap R Cl) r * (CliffordAlgebra.ι Q) u = (CliffordAlgebra.ι Q) u * (algebraMap R Cl) r@Algebra.commutes: ∀ {R : Type u_1} {A : Type (max u_1 u_2)} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R)
  (x : A), (algebraMap R A) r * x = x * (algebraMap R A) r
Algebra.commutesR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
(CliffordAlgebra.ι Q) u * (algebraMap R Cl) r = (CliffordAlgebra.ι Q) u * (algebraMap R Cl) r]Goals accomplished! 🐙

example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (r : R) (u : M), ∃ w, (CliffordAlgebra.ι Q) w = (algebraMap R Cl) r * (CliffordAlgebra.ι Q) u
example (r: R
r : R: Type u_1
R) (u: M
u : M: Type u_2
M) : ∃ w: M
w : M: Type u_2
M, w: M
w = r: R
r * u: M
u : Cl: Type (max u_2 u_1)
Cl := byGoals accomplished! 🐙
  use (r: R
r • u: M
u)R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
h(CliffordAlgebra.ι Q) (r • u) = (algebraMap R Cl) r * (CliffordAlgebra.ι Q) u
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
h(CliffordAlgebra.ι Q) (r • u) = (algebraMap R Cl) r * (CliffordAlgebra.ι Q) umap_smul: ∀ {F : Type (max u_1 u_2)} {M : Type u_1} {X : Type u_2} {Y : Type (max u_1 u_2)} [inst : SMul M X] [inst_1 : SMul M Y]
  [inst_2 : FunLike F X Y] [inst_3 : MulActionHomClass F M X Y] (f : F) (c : M) (x : X), f (c • x) = c • f x
map_smul,R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
hr • (CliffordAlgebra.ι Q) u = (algebraMap R Cl) r * (CliffordAlgebra.ι Q) u Algebra.smul_def: ∀ {R : Type ?u.430421} {A : Type ?u.430420} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R)
  (x : A), r • x = (algebraMap R A) r * x
Algebra.smul_def,R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
h(algebraMap R Cl) r * (CliffordAlgebra.ι Q) u = (algebraMap R Cl) r * (CliffordAlgebra.ι Q) u Algebra.commutes: ∀ {R : Type ?u.432220} {A : Type ?u.432219} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R)
  (x : A), (algebraMap R A) r * x = x * (algebraMap R A) r
Algebra.commutesR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u✝, v, w: Cl
r: R
u: M
h(CliffordAlgebra.ι Q) u * (algebraMap R Cl) r = (CliffordAlgebra.ι Q) u * (algebraMap R Cl) r]Goals accomplished! 🐙

Axiom 4. The square of every vector is a scalar.

#checkCliffordAlgebra.ι_sq_scalar.{u_1, u_2} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M) (m : M) : (CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R Cl) (Q m) CliffordAlgebra.ι_sq_scalar: ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M), (CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R Cl) (Q m)
CliffordAlgebra.ι_sq_scalar

-- def square {Gn G: Type*} (m : Gn) : G
-- | M.mk m => (ι m)^2


local notation x: Lean.TSyntax `term
x "²" => (x: Lean.TSyntax `term
x : Cl)^2

theorem ι_sq_scalar: ∀ (m : M), (CliffordAlgebra.ι Q) m ^ 2 = (algebraMap R Cl) (Q m)
ι_sq_scalar (m: M
m : M: Type u_2
M) : m: M
m² = Q: QuadraticForm R M
Q m: M
m : Cl: Type (max u_2 u_1)
Cl :=Warning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false` byWarning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
  rw [Warning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
m: M
(CliffordAlgebra.ι Q) m ^ 2 = (algebraMap R Cl) (Q m)pow_two: ∀ {M : Type (max u_1 u_2)} [inst : Monoid M] (a : M), a ^ 2 = a * a
pow_two,Warning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
m: M
(CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R Cl) (Q m) CliffordAlgebra.ι_sq_scalar: ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M), (CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R Cl) (Q m)
CliffordAlgebra.ι_sq_scalarWarning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
m: M
(algebraMap R Cl) (Q m) = (algebraMap R Cl) (Q m)]Warning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
  doneWarning: automatically included section variable(s) unused in theorem 'ι_sq_scalar':
  [Invertible 2]
  [Invertible 2]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Invertible 2] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

/-！
  Axiom 5. The inner product is nondegenerate.

TODO: Wait to see if this is necessary and what's the weaker condition.
-/

Axiom 6. If G0 = G1, then G = G0. TODO: Wait to see if this is necessary and what's the weaker condition.

Otherwise, G is the direct sum of all the Gr.

#checkCliffordAlgebra.GradedAlgebra.ι.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M) : M →ₗ[R] DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i) CliffordAlgebra.GradedAlgebra.ι: {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] DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i)
CliffordAlgebra.GradedAlgebra.ι
#checkCliffordAlgebra.GradedAlgebra.ι_apply.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M]
  [Module R M] (Q : QuadraticForm R M) (m : M) :
  (CliffordAlgebra.GradedAlgebra.ι Q) m =
    (DirectSum.of (fun i => ↥(CliffordAlgebra.evenOdd Q i)) 1) ⟨(CliffordAlgebra.ι Q) m, ⋯⟩ CliffordAlgebra.GradedAlgebra.ι_apply: ∀ {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),
  (CliffordAlgebra.GradedAlgebra.ι Q) m =
    (DirectSum.of (fun i => ↥(CliffordAlgebra.evenOdd Q i)) 1) ⟨(CliffordAlgebra.ι Q) m, ⋯⟩
CliffordAlgebra.GradedAlgebra.ι_apply

-- def 𝒢ᵣ (v : M) (i : ℕ) := CliffordAlgebra.GradedAlgebra.ι Q v i

#checkGradedAlgebra.proj.{u_1, u_2, u_3} {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι]
  [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (i : ι) : A →ₗ[R] A GradedAlgebra.proj: {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → (𝒜 : ι → Submodule R A) → [inst : GradedAlgebra 𝒜] → ι → A →ₗ[R] A
GradedAlgebra.proj
-- #check CliffordAlgebra.proj

-- invalid occurrence of universe level 'u_3' at '𝒢ᵣ', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
--   sorryAx.{u_3} (?m.443921 _uniq.442570 _uniq.443000 _uniq.443430 mv i)
-- at declaration body
--   fun {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M}
--       (mv : CliffordAlgebra Q) (i : ℕ) =>
--     sorryAx (?m.443921 _uniq.442570 _uniq.443000 _uniq.443430 mv i)
-- def 𝒢ᵣ (mv : CliffordAlgebra Q) (i : ℕ) := sorry

-- variable {ι : Type _} [DecidableEq ι] [AddMonoid ι]
-- variable (𝒜 : ι → Submodule R (CliffordAlgebra Q))
variable (𝒜: ℕ → Submodule R Cl
𝒜 : ℕ: Type
ℕ → Submodule: (R : Type u_1) →
  (M : Type (max u_2 u_1)) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max u_2 u_1)
Submodule R: Type u_1
R (CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q))

def 𝒢ᵣ: Cl → ℕ → Cl
𝒢ᵣ (mv: Cl
mv : CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q) (i: ℕ
i : ℕ: Type
ℕ) : CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q := GradedAlgebra.proj: {ι : Type} →
  {R : Type u_1} →
    {A : Type (max u_1 u_2)} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → (𝒜 : ι → Submodule R A) → [inst : GradedAlgebra 𝒜] → ι → A →ₗ[R] A
GradedAlgebra.proj (CliffordAlgebra.evenOdd: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R Cl
CliffordAlgebra.evenOdd Q: QuadraticForm R M
Q) i: ℕ
i mv: Cl
mv

#checkList.{u} (α : Type u) : Type u List: Type u → Type u
List

-- (fun xs i => true)
--  (CliffordAlgebra Q → ℕ → Prop)
instance instGetElemByGradeCliffordAlgebra: GetElem Cl ℕ Cl fun _mv i => ↑i < Module.rank R Cl
instGetElemByGradeCliffordAlgebra : GetElem: (coll : Type (max u_2 u_1)) →
  (idx : Type) → outParam (Type (max u_2 u_1)) → outParam (coll → idx → Prop) → Type (max (max u_2 u_1) 0)
GetElem (CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q) ℕ: Type
ℕ (CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q) (fun _mv: Cl
_mv i: ℕ
i => i: ℕ
i < Module.rank: (R : Type u_1) →
  (M : Type (max u_2 u_1)) →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{max u_2 u_1}
Module.rank R: Type u_1
R (CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q)) := {
  getElem := fun mv: Cl
mv i: ℕ
i _h: ↑i < Module.rank R Cl
_h => 𝒢ᵣ: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Cl → ℕ → Cl
𝒢ᵣ mv: Cl
mv i: ℕ
i
}

example: ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (mv : Cl) (i : ℕ) (h : ↑i < Module.rank R Cl), mv[i] = mv[i]
example (mv: Cl
mv : CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q) (i: ℕ
i : ℕ: Type
ℕ) (h: ↑i < Module.rank R Cl
h : i: ℕ
i < Module.rank: (R : Type u_1) →
  (M : Type (max u_2 u_1)) →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{max u_2 u_1}
Module.rank R: Type u_1
R (CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q)) : mv: Cl
mv[i: ℕ
i] = mv: Cl
mv[i: ℕ
i] := rfl: ∀ {α : Type (max u_1 u_2)} {a : α}, a = a
rfl

#checkCoeFun.{u, v} (α : Sort u) (γ : outParam (α → Sort v)) : Sort (max (max 1 u) v) CoeFun: (α : Sort u) → outParam (α → Sort v) → Sort (max (max 1 u) v)
CoeFun

#checkModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Prop Module.Finite: (R : Type u_1) → (M : Type u_4) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Finite

#checkSubmodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
  Submodule R M Submodule.span: (R : Type u_1) →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Set M → Submodule R M
Submodule.span

#checkModule.rank R M : Cardinal.{u_2} Module.rank: (R : Type u_1) →
  (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{u_2}
Module.rank R: Type u_1
R M: Type u_2
M

#checkModule.rank R Cl : Cardinal.{max u_2 u_1} Module.rank: (R : Type u_1) →
  (M : Type (max u_2 u_1)) →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{max u_2 u_1}
Module.rank R: Type u_1
R (CliffordAlgebra: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_2 u_1)
CliffordAlgebra Q: QuadraticForm R M
Q)

#checkAlgebra.adjoin.{u, v} (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : Subalgebra R A Algebra.adjoin: (R : Type u) →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Set A → Subalgebra R A
Algebra.adjoin

#checkSubsemiring.closure.{u} {R : Type u} [NonAssocSemiring R] (s : Set R) : Subsemiring R Subsemiring.closure: {R : Type u} → [inst : NonAssocSemiring R] → Set R → Subsemiring R
Subsemiring.closure

#checkAlgebra.adjoin_eq.{uR, uA} {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A]
  (S : Subalgebra R A) : Algebra.adjoin R ↑S = S Algebra.adjoin_eq: ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  Algebra.adjoin R ↑S = S
Algebra.adjoin_eq

#checkAlgebra.adjoin_eq_range_freeAlgebra_lift.{u_1, u_3} (R : Type u_1) [CommSemiring R] {A : Type u_3} [Semiring A]
  [Algebra R A] (s : Set A) : Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range Algebra.adjoin_eq_range_freeAlgebra_lift: ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range
Algebra.adjoin_eq_range_freeAlgebra_lift

example: ∀ (c : ℂ), c = c
example (c: ℂ
c : ℂ: Type
ℂ) : c: ℂ
c = c: ℂ
c := rfl: ∀ {α : Type} {a : α}, a = a
rfl

#checkCliffordAlgebraComplex.ofComplex : ℂ →ₐ[ℝ] CliffordAlgebra CliffordAlgebraComplex.Q CliffordAlgebraComplex.ofComplex: ℂ →ₐ[ℝ] CliffordAlgebra CliffordAlgebraComplex.Q
CliffordAlgebraComplex.ofComplex

#checkModule.rank ℝ (CliffordAlgebra CliffordAlgebraComplex.Q) : Cardinal.{0} Module.rank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{0}
Module.rank ℝ: Type
ℝ (CliffordAlgebra: {R : Type} →
  [inst : CommRing R] → {M : Type} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type
CliffordAlgebra CliffordAlgebraComplex.Q: QuadraticForm ℝ ℝ
CliffordAlgebraComplex.Q)

example: Cardinal.mk ℝ = Cardinal.continuum
example : Cardinal.mk: Type → Cardinal.{0}
Cardinal.mk ℝ: Type
ℝ = Cardinal.continuum: Cardinal.{0}
Cardinal.continuum := byGoals accomplished! 🐙
  simp only [Cardinal.mk_real: Cardinal.mk ℝ = Cardinal.continuum
Cardinal.mk_real]Goals accomplished! 🐙

example: Module.rank ℝ ℝ = 1
example : Module.rank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{0}
Module.rank ℝ: Type
ℝ ℝ: Type
ℝ = 1: Cardinal.{0}
1 := byGoals accomplished! 🐙
  simp only [rank_self: ∀ (R : Type ?u.687052) [inst : Ring R] [inst_1 : StrongRankCondition R], Module.rank R R = 1
rank_self]Goals accomplished! 🐙

example: Module.rank ℝ ℂ = 2
example : Module.rank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{0}
Module.rank ℝ: Type
ℝ ℂ: Type
ℂ = 2: Cardinal.{0}
2 := byGoals accomplished! 🐙
  simp only [Complex.rank_real_complex: Module.rank ℝ ℂ = 2
Complex.rank_real_complex]Goals accomplished! 🐙

#checkRingHom.Finite.{u_1, u_2} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) : Prop RingHom.Finite: {A : Type u_1} → {B : Type u_2} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → Prop
RingHom.Finite

-- local instance : Module.Finite ℝ ℂ := by
--   apply Complex.finite_real_complex

-- instance instFiniteCliffordAlgebraComplex : Module.Finite ℝ (CliffordAlgebra CliffordAlgebraComplex.Q) := sorry

noncomputable def basisOneI: Basis (Fin 2) ℝ (CliffordAlgebra CliffordAlgebraComplex.Q)
basisOneI : Basis: Type → (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type
Basis (Fin: ℕ → Type
Fin 2: ℕ
2) ℝ: Type
ℝ (CliffordAlgebra: {R : Type} →
  [inst : CommRing R] → {M : Type} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type
CliffordAlgebra CliffordAlgebraComplex.Q: QuadraticForm ℝ ℝ
CliffordAlgebraComplex.Q) :=
  Basis.ofEquivFun: {ι R M : Type} →
  [inst : Semiring R] →
    [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : Finite ι] → (M ≃ₗ[R] ι → R) → Basis ι R M
Basis.ofEquivFun
    { toFun := fun mv: CliffordAlgebra CliffordAlgebraComplex.Q
mv =>
      let z: ℂ
z := CliffordAlgebraComplex.toComplex: CliffordAlgebra CliffordAlgebraComplex.Q →ₐ[ℝ] ℂ
CliffordAlgebraComplex.toComplex mv: CliffordAlgebra CliffordAlgebraComplex.Q
mv
      ![z: ℂ
z.re: ℂ → ℝ
re, z: ℂ
z.im: ℂ → ℝ
im]
      invFun := fun c: Fin 2 → ℝ
c => CliffordAlgebraComplex.ofComplex: ℂ →ₐ[ℝ] CliffordAlgebra CliffordAlgebraComplex.Q
CliffordAlgebraComplex.ofComplex (c: Fin 2 → ℝ
c 0: Fin 2
0 + c: Fin 2 → ℝ
c 1: Fin 2
1 • Complex.I: ℂ
Complex.I)
      left_inv := fun z: CliffordAlgebra CliffordAlgebraComplex.Q
z => byGoals accomplished! 🐙 simpGoals accomplished! 🐙
      right_inv := fun c: Fin 2 → ℝ
c => byGoals accomplished! 🐙
        ext i: Fin 2
iR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
c: Fin 2 → ℝ
i: Fin 2
h{
        toFun := fun mv =>
          let z := CliffordAlgebraComplex.toComplex mv;
          ![z.re, z.im],
        map_add' := ⋯, map_smul' := ⋯ }.toFun
    ((fun c => CliffordAlgebraComplex.ofComplex (↑(c 0) + c 1 • Complex.I)) c) i =
  c i
        fin_cases i: Fin 2
iR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
c: Fin 2 → ℝ
h.head{
        toFun := fun mv =>
          let z := CliffordAlgebraComplex.toComplex mv;
          ![z.re, z.im],
        map_add' := ⋯, map_smul' := ⋯ }.toFun
    ((fun c => CliffordAlgebraComplex.ofComplex (↑(c 0) + c 1 • Complex.I)) c) ⟨0, ⋯⟩ =
  c ⟨0, ⋯⟩
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
c: Fin 2 → ℝ
h.tail.head{
        toFun := fun mv =>
          let z := CliffordAlgebraComplex.toComplex mv;
          ![z.re, z.im],
        map_add' := ⋯, map_smul' := ⋯ }.toFun
    ((fun c => CliffordAlgebraComplex.ofComplex (↑(c 0) + c 1 • Complex.I)) c) ⟨1, ⋯⟩ =
  c ⟨1, ⋯⟩ <;>R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
c: Fin 2 → ℝ
h.head{
        toFun := fun mv =>
          let z := CliffordAlgebraComplex.toComplex mv;
          ![z.re, z.im],
        map_add' := ⋯, map_smul' := ⋯ }.toFun
    ((fun c => CliffordAlgebraComplex.ofComplex (↑(c 0) + c 1 • Complex.I)) c) ⟨0, ⋯⟩ =
  c ⟨0, ⋯⟩
R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
c: Fin 2 → ℝ
h.tail.head{
        toFun := fun mv =>
          let z := CliffordAlgebraComplex.toComplex mv;
          ![z.re, z.im],
        map_add' := ⋯, map_smul' := ⋯ }.toFun
    ((fun c => CliffordAlgebraComplex.ofComplex (↑(c 0) + c 1 • Complex.I)) c) ⟨1, ⋯⟩ =
  c ⟨1, ⋯⟩ simpGoals accomplished! 🐙
      map_add' := fun z: CliffordAlgebra CliffordAlgebraComplex.Q
z z': CliffordAlgebra CliffordAlgebraComplex.Q
z' => byGoals accomplished! 🐙 simpGoals accomplished! 🐙
      map_smul' := fun c: ℝ
c z: CliffordAlgebra CliffordAlgebraComplex.Q
z => byGoals accomplished! 🐙 simpGoals accomplished! 🐙 }

example: finrank ℝ (CliffordAlgebra CliffordAlgebraComplex.Q) = 2
example : finrank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank ℝ: Type
ℝ (CliffordAlgebra: {R : Type} →
  [inst : CommRing R] → {M : Type} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type
CliffordAlgebra CliffordAlgebraComplex.Q: QuadraticForm ℝ ℝ
CliffordAlgebraComplex.Q) = 2: ℕ
2 := byGoals accomplished! 🐙
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
finrank ℝ (CliffordAlgebra CliffordAlgebraComplex.Q) = 2finrank_eq_card_basis: ∀ {R M : Type} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : StrongRankCondition R]
  {ι : Type} [inst_4 : Fintype ι], Basis ι R M → finrank R M = Fintype.card ι
finrank_eq_card_basis basisOneI: Basis (Fin 2) ℝ (CliffordAlgebra CliffordAlgebraComplex.Q)
basisOneI,R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
Fintype.card (Fin 2) = 2 Fintype.card_fin: ∀ (n : ℕ), Fintype.card (Fin n) = n
Fintype.card_finR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
2 = 2]Goals accomplished! 🐙
  doneWarning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

#checkCliffordAlgebraComplex.equiv : CliffordAlgebra CliffordAlgebraComplex.Q ≃ₐ[ℝ] ℂ CliffordAlgebraComplex.equiv: CliffordAlgebra CliffordAlgebraComplex.Q ≃ₐ[ℝ] ℂ
CliffordAlgebraComplex.equiv

universe uA

#checkAlgEquiv.toLinearEquiv_refl.{uR, uA₁} {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] :
  AlgEquiv.refl.toLinearEquiv = LinearEquiv.refl R A₁ AlgEquiv.toLinearEquiv_refl: ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  AlgEquiv.refl.toLinearEquiv = LinearEquiv.refl R A₁
AlgEquiv.toLinearEquiv_refl
#checkFiniteDimensional.nonempty_linearEquiv_iff_finrank_eq.{u, v, v'} {R : Type u} {M : Type v} {M' : Type v'} [Ring R]
  [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M']
  [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] : Nonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M' FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq: ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : StrongRankCondition R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : AddCommGroup M'] [inst_6 : Module R M']
  [inst_7 : Module.Free R M'] [inst_8 : Module.Finite R M] [inst_9 : Module.Finite R M'],
  Nonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M'
FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq
/-
LinearEquiv.finrank_eq.{u_3, u_2, u_1} {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst✝ : Ring R]
  [inst✝¹ : AddCommGroup M] [inst✝² : AddCommGroup M₂] [inst✝³ : Module R M] [inst✝⁴ : Module R M₂] (f : M ≃ₗ[R] M₂) :
  finrank R M = finrank R M₂
-/
#checkLinearEquiv.finrank_eq.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M]
  [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M ≃ₗ[R] M₂) : finrank R M = finrank R M₂ LinearEquiv.finrank_eq: ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (M ≃ₗ[R] M₂) → finrank R M = finrank R M₂
LinearEquiv.finrank_eq

#checkCommRing.{u} (α : Type u) : Type u CommRing: Type u → Type u
CommRing

local notation "Clℂ" => CliffordAlgebra CliffordAlgebraComplex.Q

lemma finrank_eq: ∀ (R : Type uR) (A B : Type uA) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B] [inst_3 : Algebra R A]
  [inst_4 : Algebra R B], (A ≃ₐ[R] B) → finrank R A = finrank R B
finrank_eq (R: Type uR
R: Type uR: Type (uR + 1)
Type uR) (A: Type uA
A B: Type uA
B: Type uA: Type (uA + 1)
Type uA) [CommRing: Type uR → Type uR
CommRing R: Type uR
R] [Ring: Type uA → Type uA
Ring A: Type uA
A] [Ring: Type uA → Type uA
Ring B: Type uA
B] [Algebra: (R : Type uR) → (A : Type uA) → [inst : CommSemiring R] → [inst : Semiring A] → Type (max uR uA)
Algebra R: Type uR
R A: Type uA
A] [Algebra: (R : Type uR) → (A : Type uA) → [inst : CommSemiring R] → [inst : Semiring A] → Type (max uR uA)
Algebra R: Type uR
R B: Type uA
B] :
  (A: Type uA
A ≃ₐ[R: Type uR
R] B: Type uA
B) → finrank: (R : Type uR) → (M : Type uA) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank R: Type uR
R A: Type uA
A = finrank: (R : Type uR) → (M : Type uA) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank R: Type uR
R B: Type uA
B := fun ha: A ≃ₐ[R] B
ha => LinearEquiv.finrank_eq: ∀ {R : Type uR} {M M₂ : Type uA} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (M ≃ₗ[R] M₂) → finrank R M = finrank R M₂
LinearEquiv.finrank_eq ha: A ≃ₐ[R] B
ha.toLinearEquiv: {R : Type uR} →
  {A₁ A₂ : Type uA} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A₁] →
        [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ ≃ₗ[R] A₂
toLinearEquiv
--   done

example: finrank ℝ Clℂ = finrank ℝ ℂ
example : finrank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank ℝ: Type
ℝ Clℂ: Type
Clℂ = finrank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank ℝ: Type
ℝ ℂ: Type
ℂ := byGoals accomplished! 🐙
  rw [R: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
finrank ℝ Clℂ = finrank ℝ ℂfinrank_eq: ∀ (R A B : Type) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  (A ≃ₐ[R] B) → finrank R A = finrank R B
finrank_eq ℝ: Type
ℝ Clℂ: Type
Clℂ ℂ: Type
ℂ CliffordAlgebraComplex.equiv: Clℂ ≃ₐ[ℝ] ℂ
CliffordAlgebraComplex.equivR: Type u_1
M: Type u_2
inst✝⁴: CommRing R
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
inst✝¹: Invertible 2
inst✝: Invertible 2
u, v, w: Cl
𝒜: ℕ → Submodule R Cl
finrank ℝ ℂ = finrank ℝ ℂ]Goals accomplished! 🐙

example: finrank ℝ Clℂ = finrank ℝ ℂ
example : finrank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank ℝ: Type
ℝ Clℂ: Type
Clℂ = finrank: (R M : Type) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank ℝ: Type
ℝ ℂ: Type
ℂ := LinearEquiv.finrank_eq: ∀ {R M M₂ : Type} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M]
  [inst_4 : Module R M₂], (M ≃ₗ[R] M₂) → finrank R M = finrank R M₂
LinearEquiv.finrank_eq CliffordAlgebraComplex.equiv: Clℂ ≃ₐ[ℝ] ℂ
CliffordAlgebraComplex.equiv.toLinearEquiv: {R A₁ A₂ : Type} →
  [inst : CommSemiring R] →
    [inst_1 : Semiring A₁] →
      [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ ≃ₗ[R] A₂
toLinearEquiv

--   done


-- example (n : ℕ) : Cardinal.mk (Vector ℝ n) = n := by
--   simp only [Cardinal.mk_vector]
--   done

-- #check Cardinal.mk_vector

-- example (c : ℂ) : (CliffordAlgebraComplex.ofComplex c)[0] = 1 := rfl

-- example : Module.rank R (CliffordAlgebra Q) = 2^(Module.rank R M) := sorry


#checkDirectSum.GradeZero.module.{u_1, u_2} {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)]
  [AddMonoid ι] [DirectSum.GSemiring A] {i : ι} : Module (A 0) (A i) DirectSum.GradeZero.module: {ι : Type u_1} →
  [inst : DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [inst_2 : AddMonoid ι] → [inst_3 : DirectSum.GSemiring A] → {i : ι} → Module (A 0) (A i)
DirectSum.GradeZero.module

#checkDirectSum.decomposeRingEquiv
  (CliffordAlgebra.evenOdd Q) : Cl ≃+* DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i) DirectSum.decomposeRingEquiv: {ι : Type} →
  {A σ : Type (max u_1 u_2)} →
    [inst : DecidableEq ι] →
      [inst_1 : AddMonoid ι] →
        [inst_2 : Semiring A] →
          [inst_3 : SetLike σ A] →
            [inst_4 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [inst_5 : GradedRing 𝒜] → A ≃+* DirectSum ι fun i => ↥(𝒜 i)
DirectSum.decomposeRingEquiv (CliffordAlgebra.evenOdd: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R Cl
CliffordAlgebra.evenOdd Q: QuadraticForm R M
Q)

#checkDirectSum.decomposeAlgEquiv
  (CliffordAlgebra.evenOdd Q) : Cl ≃ₐ[R] DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i) DirectSum.decomposeAlgEquiv: {ι : Type} →
  {R : Type u_1} →
    {A : Type (max u_1 u_2)} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (𝒜 : ι → Submodule R A) → [inst_5 : GradedAlgebra 𝒜] → A ≃ₐ[R] DirectSum ι fun i => ↥(𝒜 i)
DirectSum.decomposeAlgEquiv (CliffordAlgebra.evenOdd: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R Cl
CliffordAlgebra.evenOdd Q: QuadraticForm R M
Q)

#checkLinearEquiv.ofFinrankEq.{u, v, v'} {R : Type u} (M : Type v) (M' : Type v') [Ring R] [StrongRankCondition R]
  [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] [Module.Finite R M]
  [Module.Finite R M'] (cond : finrank R M = finrank R M') : M ≃ₗ[R] M' LinearEquiv.ofFinrankEq: {R : Type u} →
  (M : Type v) →
    (M' : Type v') →
      [inst : Ring R] →
        [inst_1 : StrongRankCondition R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : Module.Free R M] →
                [inst_5 : AddCommGroup M'] →
                  [inst_6 : Module R M'] →
                    [inst_7 : Module.Free R M'] →
                      [inst_8 : Module.Finite R M] →
                        [inst_9 : Module.Finite R M'] → finrank R M = finrank R M' → M ≃ₗ[R] M'
LinearEquiv.ofFinrankEq

open DirectSum

local notation "Cl₀₁" => CliffordAlgebra.evenOdd Q

-- def Cl₀₁ (i : ZMod 2) : Submodule R Cl := CliffordAlgebra.evenOdd Q i

example: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Cl ≃+* ⨁ (i : ZMod 2), ↥(Cl₀₁ i)
example : Cl: Type (max u_2 u_1)
Cl ≃+* ⨁ (i: ZMod 2
i : ZMod: ℕ → Type
ZMod 2: ℕ
2), Cl₀₁: ZMod 2 → Submodule R Cl
Cl₀₁ i: ZMod 2
i := byGoals accomplished! 🐙
  apply DirectSum.decomposeRingEquiv: {ι : Type} →
  {A σ : Type (max u_1 u_2)} →
    [inst : DecidableEq ι] →
      [inst_1 : AddMonoid ι] →
        [inst_2 : Semiring A] →
          [inst_3 : SetLike σ A] →
            [inst_4 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [inst_5 : GradedRing 𝒜] → A ≃+* ⨁ (i : ι), ↥(𝒜 i)
DirectSum.decomposeRingEquiv (CliffordAlgebra.evenOdd: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R Cl
CliffordAlgebra.evenOdd Q: QuadraticForm R M
Q)Goals accomplished! 🐙
  doneWarning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

example: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Cl ≃ₐ[R] ⨁ (i : ZMod 2), ↥(Cl₀₁ i)
example : Cl: Type (max u_2 u_1)
Cl ≃ₐ[R: Type u_1
R] ⨁ (i: ZMod 2
i : ZMod: ℕ → Type
ZMod 2: ℕ
2), Cl₀₁: ZMod 2 → Submodule R Cl
Cl₀₁ i: ZMod 2
i := byGoals accomplished! 🐙
  apply DirectSum.decomposeAlgEquiv: {ι : Type} →
  {R : Type u_1} →
    {A : Type (max u_1 u_2)} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → (𝒜 : ι → Submodule R A) → [inst_5 : GradedAlgebra 𝒜] → A ≃ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
DirectSum.decomposeAlgEquiv (CliffordAlgebra.evenOdd: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R Cl
CliffordAlgebra.evenOdd Q: QuadraticForm R M
Q)Goals accomplished! 🐙
  doneWarning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙

variable (i: ZMod 2
i : ZMod: ℕ → Type
ZMod 2: ℕ
2)

#checkCl₀₁ i : Submodule R Cl CliffordAlgebra.evenOdd: {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R Cl
CliffordAlgebra.evenOdd Q: QuadraticForm R M
Q i: ZMod 2
i

#checkModule.finrank_directSum.{u, v, w} (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι]
  (M : ι → Type w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)]
  [∀ (i : ι), Module.Finite R (M i)] : finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i) finrank_directSum: ∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] (M : ι → Type w)
  [inst_3 : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module R (M i)] [inst_5 : ∀ (i : ι), Module.Free R (M i)]
  [inst_6 : ∀ (i : ι), Module.Finite R (M i)], finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i)
finrank_directSum

/-
failed to synthesize
  CommRing (⨁ (i : ZMod 2), ↥CliffordAlgebra.evenOdd Q i)
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
-/
-- #check finrank_directSum (⨁ i, CliffordAlgebra.evenOdd Q i)

-- example (i : ZMod 2) : finrank (⨁ i, CliffordAlgebra.evenOdd Q i) =  := by
--   -- rw [finrank_directSum]
--   done

-- example : finrank R (CliffordAlgebra Q) = 2^(finrank R M) := by
--   -- conv_lhs => rw [finrank_directSum]
--   rw [← Nat.sum_range_choose]
--   sorry
--   done