-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_comm (x : CliffordAlgebra Q) : d⌋(d'⌋x) = -(d'⌋(d⌋x))

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractLeft d) ((contractLeft d') x) = -(contractLeft d') ((contractLeft d) x)

Tactic:
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [contractLeft_algebraMap, map_zero, neg_zero]
| add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy, neg_add]
| ι_mul _ _ hx =>
  simp only [contractLeft_ι_mul, map_sub, LinearMap.map_smul]
  rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]

Result:
no goals

Proof state:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
⊢ (contractLeft d) ((contractLeft d') ((ι Q) m✝ * x✝)) = -(contractLeft d') ((contractLeft d) ((ι Q) m✝ * x✝))

Tactic:
simp only [contractLeft_ι_mul, map_sub, LinearMap.map_smul]

Result:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
⊢ d' m✝ • (contractLeft d) x✝ - (d m✝ • (contractLeft d') x✝ - (ι Q) m✝ * (contractLeft d) ((contractLeft d') x✝)) =
    -(d m✝ • (contractLeft d') x✝ - (d' m✝ • (contractLeft d) x✝ - (ι Q) m✝ * (contractLeft d') ((contractLeft d) x✝)))

Proof state:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') (x✝ + y✝)) = -(contractLeft d') ((contractLeft d) (x✝ + y✝))

Tactic:
rw [map_add, map_add, map_add, map_add, hx, hy, neg_add]

Result:
no goals

Proof state:
case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r✝ : R
⊢ (contractLeft d) ((contractLeft d') ((algebraMap R (CliffordAlgebra Q)) r✝)) =
    -(contractLeft d') ((contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r✝))

Tactic:
simp_rw [contractLeft_algebraMap, map_zero, neg_zero]

Result:
no goals

Proof state:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
⊢ d' m✝ • (contractLeft d) x✝ - (d m✝ • (contractLeft d') x✝ - (ι Q) m✝ * (contractLeft d) ((contractLeft d') x✝)) =
    -(d m✝ • (contractLeft d') x✝ - (d' m✝ • (contractLeft d) x✝ - (ι Q) m✝ * (contractLeft d') ((contractLeft d) x✝)))

Tactic:
rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]

Result:
no goals