-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_contractLeft (d : Module.Dual R M) (x : CliffordAlgebra Q) :
    -- Porting note: original statement
    --    changeForm h (d⌋x) = d⌋changeForm h x

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

Tactic:
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp only [contractLeft_algebraMap, changeForm_algebraMap, map_zero]
| add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy]
| ι_mul _ _ hx =>
  simp only [contractLeft_ι_mul, changeForm_ι_mul, map_sub, LinearMap.map_smul]
  rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]

Result:
no goals

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

Tactic:
simp only [contractLeft_ι_mul, changeForm_ι_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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
⊢ d m✝ • (changeForm h) x✝ -
      ((ι Q') m✝ * (changeForm h) ((contractLeft d) x✝) -
        (contractLeft (B m✝)) ((changeForm h) ((contractLeft d) x✝))) =
    d m✝ • (changeForm h) x✝ - (ι Q') m✝ * (contractLeft d) ((changeForm h) x✝) -
      (contractLeft d) ((contractLeft (B m✝)) ((changeForm h) x✝))

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

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

Result:
no goals

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

Tactic:
simp only [contractLeft_algebraMap, changeForm_algebraMap, map_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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
⊢ d m✝ • (changeForm h) x✝ -
      ((ι Q') m✝ * (changeForm h) ((contractLeft d) x✝) -
        (contractLeft (B m✝)) ((changeForm h) ((contractLeft d) x✝))) =
    d m✝ • (changeForm h) x✝ - (ι Q') m✝ * (contractLeft d) ((changeForm h) x✝) -
      (contractLeft d) ((contractLeft (B m✝)) ((changeForm h) x✝))

Tactic:
rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]

Result:
no goals