-- import Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
import Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
import Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
import Mathlib.LinearAlgebra.TensorAlgebra.Basis
import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
import Mathlib.Tactic

open QuadraticForm BilinForm ExteriorAlgebra FiniteDimensional QuadraticMap

#check
QuadraticMap.polar_self.{u_3, u_4, u_5} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M]
  [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (x : M) : polar (⇑Q) x x = 2 • Q x 
polar_self: ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x : M), polar (⇑Q) x x = 2 • Q x
polar_self

universe uκ uR uM uι

variable {
κ: Type uκ
κ : 
Type uκ: Type (uκ + 1)
Type uκ}
variable {
R: Type uR
R : 
Type uR: Type (uR + 1)
Type uR} [
CommRing: Type uR → Type uR
CommRing 
R: Type uR
R] [
Invertible: {α : Type uR} → [inst : Mul α] → [inst : One α] → α → Type uR
Invertible (
2: R
2 : 
R: Type uR
R)] [
Nontrivial: Type uR → Prop
Nontrivial 
R: Type uR
R]
variable {
M: Type uM
M : 
Type uM: Type (uM + 1)
Type uM} [
AddCommGroup: Type uM → Type uM
AddCommGroup 
M: Type uM
M] [
Module: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max uR uM)
Module 
R: Type uR
R 
M: Type uM
M]
-- variable {B : BilinForm R M}
variable (
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type uR) →
  (M : Type uM) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max uR uM)
QuadraticForm 
R: Type uR
R 
M: Type uM
M) {
Cl: CliffordAlgebra Q
Cl : 
CliffordAlgebra: {R : Type uR} →
  [inst : CommRing R] →
    {M : Type uM} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max uM uR)
CliffordAlgebra 
Q: QuadraticForm R M
Q} {
Ex: ExteriorAlgebra R M
Ex : 
ExteriorAlgebra: (R : Type uR) → [inst : CommRing R] → (M : Type uM) → [inst_1 : AddCommGroup M] → [inst : Module R M] → Type (max uM uR)
ExteriorAlgebra 
R: Type uR
R 
M: Type uM
M}
variable [
Module.Finite: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Finite 
R: Type uR
R 
M: Type uM
M] [
Module.Free: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Free 
R: Type uR
R 
M: Type uM
M]

variable {
ι: Type uι
ι : 
Type uι: Type (uι + 1)
Type uι}
variable [
DecidableEq: Type uι → Type (max 0 uι)
DecidableEq 
ι: Type uι
ι] [
AddMonoid: Type uι → Type uι
AddMonoid 
ι: Type uι
ι]
variable (
𝒜: ι → Submodule R (ExteriorAlgebra R M)
𝒜 : 
ι: Type uι
ι → 
Submodule: (R : Type uR) →
  (M : Type (max uM uR)) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max uM uR)
Submodule 
R: Type uR
R (
ExteriorAlgebra: (R : Type uR) → [inst : CommRing R] → (M : Type uM) → [inst_1 : AddCommGroup M] → [inst : Module R M] → Type (max uM uR)
ExteriorAlgebra 
R: Type uR
R 
M: Type uM
M))

noncomputable def 
QuadraticForm.B: {R : Type uR} →
  [inst : CommRing R] →
    {M : Type uM} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → LinearMap.BilinMap R M R
QuadraticForm.B := 
Classical.choose: {α : Type (max uM uR)} → {p : α → Prop} → (∃ x, p x) → α
Classical.choose 
Q: QuadraticForm R M
Q.
exists_companion: ∀ {R : Type uR} {M : Type uM} {N : Type uR} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N),
  ∃ B, ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
exists_companion

#check
Nat.sum_range_choose (n : ℕ) : ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n 
Nat.sum_range_choose: ∀ (n : ℕ), ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n
Nat.sum_range_choose

#check
Module.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)] : Module.finrank R (DirectSum ι fun i => M i) = ∑ i : ι, Module.finrank R (M i) 
Module.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)],
  Module.finrank R (DirectSum ι fun i => M i) = ∑ i : ι, Module.finrank R (M i)
Module.finrank_directSum

#check
rank_directSum.{u, v, w} (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} (M : ι → Type w)
  [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] :
  Module.rank R (DirectSum ι fun i => M i) = Cardinal.sum fun i => Module.rank R (M i) 
rank_directSum: ∀ (R : Type u) [inst : Ring R] [inst_1 : StrongRankCondition R] {ι : Type v} (M : ι → Type w)
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module R (M i)] [inst_4 : ∀ (i : ι), Module.Free R (M i)],
  Module.rank R (DirectSum ι fun i => M i) = Cardinal.sum fun i => Module.rank R (M i)
rank_directSum

#check
DirectSum.decomposeAlgEquiv.{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 𝒜] :
  A ≃ₐ[R] DirectSum ι fun i => ↥(𝒜 i) 
DirectSum.decomposeAlgEquiv: {ι : 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_5 : GradedAlgebra 𝒜] → A ≃ₐ[R] DirectSum ι fun i => ↥(𝒜 i)
DirectSum.decomposeAlgEquiv

#check
ExteriorAlgebra.liftAlternatingEquiv.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R]
  [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :
  ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N 
ExteriorAlgebra.liftAlternatingEquiv: {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
ExteriorAlgebra.liftAlternatingEquiv

#check
Module.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop 
Module.Free: (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Free

#check
Module.Free.directSum.{u, u_2, u_3} (R : Type u) [Semiring R] {ι : Type u_2} (M : ι → Type u_3)
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] :
  Module.Free R (DirectSum ι fun i => M i) 
Module.Free.directSum: ∀ (R : Type u) [inst : Semiring R] {ι : Type u_2} (M : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : ∀ (i : ι), Module.Free R (M i)],
  Module.Free R (DirectSum ι fun i => M i)
Module.Free.directSum

#check
Module.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module 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

#check
Q.B : LinearMap.BilinMap R M R 
Q: QuadraticForm R M
Q.
B: {R : Type uR} →
  [inst : CommRing R] →
    {M : Type uM} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → LinearMap.BilinMap R M R
B

#check
CliffordAlgebra.equivExterior Q : CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M 
CliffordAlgebra.equivExterior: {R : Type uR} →
  [inst : CommRing R] →
    {M : Type uM} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → [inst_3 : Invertible 2] → CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
CliffordAlgebra.equivExterior 
Q: QuadraticForm R M
Q

#check
Module.Free.multilinearMap.{u_1, u_2, u_3, u_4} {ι : Type u_1} {R : Type u_2} {M₂ : Type u_3} {M₁ : ι → Type u_4}
  [Finite ι] [CommRing R] [AddCommGroup M₂] [Module R M₂] [Module.Finite R M₂] [Module.Free R M₂]
  [(i : ι) → AddCommGroup (M₁ i)] [(i : ι) → Module R (M₁ i)] [∀ (i : ι), Module.Finite R (M₁ i)]
  [∀ (i : ι), Module.Free R (M₁ i)] : Module.Free R (MultilinearMap R M₁ M₂) 
Module.Free.multilinearMap: ∀ {ι : Type u_1} {R : Type u_2} {M₂ : Type u_3} {M₁ : ι → Type u_4} [inst : Finite ι] [inst : CommRing R]
  [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂] [inst_3 : Module.Finite R M₂] [inst_4 : Module.Free R M₂]
  [inst_5 : (i : ι) → AddCommGroup (M₁ i)] [inst_6 : (i : ι) → Module R (M₁ i)]
  [inst_7 : ∀ (i : ι), Module.Finite R (M₁ i)] [inst_8 : ∀ (i : ι), Module.Free R (M₁ i)],
  Module.Free R (MultilinearMap R M₁ M₂)
Module.Free.multilinearMap

#check
CliffordAlgebra.equivBaseChange.{u_1, u_2, u_3} {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A]
  [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) :
  CliffordAlgebra (QuadraticForm.baseChange A Q) ≃ₐ[A] TensorProduct R A (CliffordAlgebra Q) 
CliffordAlgebra.equivBaseChange: {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) →
                    CliffordAlgebra (QuadraticForm.baseChange A Q) ≃ₐ[A] TensorProduct R A (CliffordAlgebra Q)
CliffordAlgebra.equivBaseChange

#check
TensorAlgebra.rank_eq.{uR, uM} {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial R]
  [Module.Free R M] :
  Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n) 
TensorAlgebra.rank_eq: ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Nontrivial R] [inst_4 : Module.Free R M],
  Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)
TensorAlgebra.rank_eq

#check
TensorAlgebra.equivFreeAlgebra.{uκ, uR, uM} {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M]
  [Module R M] (b : Basis κ R M) : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ 
TensorAlgebra.equivFreeAlgebra: {κ : Type uκ} →
  {R : Type uR} →
    {M : Type uM} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Basis κ R M → TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ
TensorAlgebra.equivFreeAlgebra

#check
TensorAlgebra.toExterior.{u1, u2} {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :
  TensorAlgebra R M →ₐ[R] ExteriorAlgebra R M 
TensorAlgebra.toExterior: {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → TensorAlgebra R M →ₐ[R] ExteriorAlgebra R M
TensorAlgebra.toExterior

#check
ExteriorAlgebra.gradedAlgebra.{u_1, u_2} (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
  GradedAlgebra fun i => ⋀[R]^i M 
ExteriorAlgebra.gradedAlgebra: (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → GradedAlgebra fun i => ⋀[R]^i M
ExteriorAlgebra.gradedAlgebra

#check
gradedAlgebra R M : GradedAlgebra fun i => ⋀[R]^i M 
ExteriorAlgebra.gradedAlgebra: (R : Type uR) →
  (M : Type uM) →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → GradedAlgebra fun i => ⋀[R]^i M
ExteriorAlgebra.gradedAlgebra 
R: Type uR
R 
M: Type uM
M

-- example : Module.Free R (ExteriorAlgebra R M) := by

--   done

-- example : (∀ i, M [Λ^Fin i]→ₗ[R] M) = (∀ i, AlternatingMap R M M i) := by
--   done

example: ∀ {R : Type uR} [inst : CommRing R] [inst_1 : Nontrivial R] {M : Type uM} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module.Finite R M], Module.rank R M = ↑(Module.finrank R M)
example : 
Module.rank: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{uM}
Module.rank 
R: Type uR
R 
M: Type uM
M = 
Module.finrank: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
Module.finrank 
R: Type uR
R 
M: Type uM
M := by
Goals accomplished! 🐙
  exact (
Module.finrank_eq_rank: ∀ (R : Type uR) (M : Type uM) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M], ↑(Module.finrank R M) = Module.rank R M
Module.finrank_eq_rank 
R: Type uR
R 
M: Type uM
M).
symm: ∀ {α : Type (uM + 1)} {a b : α}, a = b → b = a
symm
Goals accomplished! 🐙

-- example : finrank R (TensorAlgebra R M) = 2^(finrank R M) := by

--   done

-- example : finrank R (CliffordAlgebra Q) = 2^(finrank R M) := by
--   -- let em := CliffordAlgebra.equivExterior Q
--   -- let Ex := em Cl
--   have h1 : finrank R (CliffordAlgebra Q) = finrank R (ExteriorAlgebra R M) := by
--     apply LinearEquiv.finrank_eq
--     exact CliffordAlgebra.equivExterior Q
--   have h2 : finrank R (ExteriorAlgebra R M) = finrank R (∀ i, M [Λ^Fin i]→ₗ[R] M) := by
--     apply LinearEquiv.finrank_eq
--     exact ExteriorAlgebra.liftAlternatingEquiv R M
--   have h3 : finrank R (ExteriorAlgebra R M) = 2^(finrank R M) := by

--     done
--   done

-- noncomputable def ExteriorAlgebra.equivFreeAlgebra (b : Basis κ R M) :
--     ExteriorAlgebra R M ≃ₐ[R] FreeAlgebra R κ := by
--   apply AlgEquiv.ofAlgHom
--   . apply ExteriorAlgebra.lift

--   done

--     -- (ExteriorAlgebra.lift _ (Finsupp.total _ _ _ (FreeAlgebra.ι _) ∘ₗ b.repr.toLinearMap))
--     -- (FreeAlgebra.lift _ (ι R ∘ b))
--     -- (by ext; simp)
--     -- (hom_ext <| b.ext <| fun i => by simp)

lemma 
rank_eq: Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)
rank_eq :
    
Module.rank: (R : Type uR) →
  (M : Type (max uM uR)) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{max uM uR}
Module.rank 
R: Type uR
R (
TensorAlgebra: (R : Type uR) →
  [inst : CommSemiring R] → (M : Type uM) → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max uR uM)
TensorAlgebra 
R: Type uR
R 
M: Type uM
M) = 
Cardinal.lift: Cardinal.{uM} → Cardinal.{max uM uR}
Cardinal.lift.{uR} (
Cardinal.sum: {ι : Type} → (ι → Cardinal.{uM}) → Cardinal.{uM}
Cardinal.sum fun 
n: ℕ
n ↦ 
Module.rank: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{uM}
Module.rank 
R: Type uR
R 
M: Type uM
M ^ 
n: ℕ
n) :=
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false` by
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙
  let ⟨⟨
κ: Type uM
κ, 
b: Basis κ R M
b⟩⟩ := 
Module.Free.exists_basis: ∀ {R : Type uR} {M : Type uM} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.Free R M], Nonempty ((I : Type uM) × Basis I R M)
Module.Free.exists_basis (R := 
R: Type uR
R) (M := 
M: Type uM
M)
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
κ: Type uM
b: Basis κ R M
Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)
  rw [
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
κ: Type uM
b: Basis κ R M
Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)(
TensorAlgebra.equivFreeAlgebra: {κ : Type uM} →
  {R : Type uR} →
    {M : Type uM} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Basis κ R M → TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ
TensorAlgebra.equivFreeAlgebra 
b: Basis κ R M
b).
toLinearEquiv: {R : Type uR} →
  {A₁ A₂ : Type (max uM uR)} →
    [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.
rank_eq: ∀ {R : Type uR} {M M₁ : Type (max uM uR)} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁], (M ≃ₗ[R] M₁) → Module.rank R M = Module.rank R M₁
rank_eq,
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
κ: Type uM
b: Basis κ R M
Module.rank R (FreeAlgebra R κ) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n) 
FreeAlgebra.rank_eq: ∀ (R : Type uR) (X : Type uM) [inst : CommRing R] [inst_1 : Nontrivial R],
  Module.rank R (FreeAlgebra R X) = Cardinal.lift.{uR, uM} (Cardinal.mk (List X))
FreeAlgebra.rank_eq,
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
κ: Type uM
b: Basis κ R M
Cardinal.lift.{uR, uM} (Cardinal.mk (List κ)) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n) 
Cardinal.mk_list_eq_sum_pow: ∀ (α : Type uM), Cardinal.mk (List α) = Cardinal.sum fun n => Cardinal.mk α ^ n
Cardinal.mk_list_eq_sum_pow,
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
κ: Type uM
b: Basis κ R M
Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Cardinal.mk κ ^ n) =
  Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)
    
Basis.mk_eq_rank'': ∀ {R : Type uR} {M : Type uM} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StrongRankCondition R] {ι : Type uM}, Basis ι R M → Cardinal.mk ι = Module.rank R M
Basis.mk_eq_rank'' 
b: Basis κ R M
b
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
κ: Type uM
b: Basis κ R M
Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n) =
  Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)]
Warning: automatically included section variable(s) unused in theorem 'rank_eq':
  [Invertible 2]
  [Module.Finite R M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Invertible 2] [Module.Finite R M] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
Goals accomplished! 🐙

-- lemma rank_eq' :
--     Module.rank R (ExteriorAlgebra R M) = Cardinal.lift.{uR} (Cardinal.sum fun n ↦ Module.rank R M ^ n) := by
--   let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
--   rw [(ExteriorAlgebra.equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, Cardinal.mk_list_eq_sum_pow,
--     Basis.mk_eq_rank'' b]
--   done

example : Module.rank R M = Module.rank R M := rfl

-- example : Module.rank R (CliffordAlgebra Q) = Module.rank R M := by

--   done

-- example (x y : M) : Q.B x y + Q.B y x = 2 * Q.B x y := by
--   have h1: Q (x + y) = Q x + Q y + Q.B x y := by
--       obtain ⟨b, hb⟩ := Q.exists_companion

--     done
--   have h2 : Q.B x y = Q (x + y) - Q x - Q y := by

--   have h : Q.B x y = Q.B y x := by

--     done
--   done