-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) =
      HSMul.hSMul (β := CliffordAlgebra Q) c
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
          CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
        HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
    (hy :
      (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
        HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)),
    (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
      HSMul.hSMul (β := CliffordAlgebra Q) c
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M)
    (hx :
      (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
        HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)),
    (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
      HSMul.hSMul (β := CliffordAlgebra Q) c
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
          CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)

Tactic:
induction x using CliffordAlgebra.left_induction with
      | algebraMap => simp_rw [foldr'_algebraMap, smul_zero]
      | add _ _ hx hy => rw [map_add, map_add, smul_add, hx, hy]
      | ι_mul _ _ hx =>
        rw [foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]

Premises used: smul_assoc, Algebra.algebraMap, LinearMap.smul_apply, smul_zero, map_add, CliffordAlgebra.foldr'_ι_mul, CliffordAlgebra.foldr'_algebraMap, smul_sub, mul_smul_comm, CliffordAlgebra.contractLeftAux_apply_apply, smul_add