-- 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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q'')
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'')
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q'')
add :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Eq (α := CliffordAlgebra Q'')
        ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
          CliffordAlgebra Q'')
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q''))
    (hy :
      Eq (α := CliffordAlgebra Q'')
        ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
          CliffordAlgebra Q'')
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') y : CliffordAlgebra Q'')),
    Eq (α := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
        CliffordAlgebra Q'')
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M)
    (hx :
      Eq (α := CliffordAlgebra Q'')
        ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
          CliffordAlgebra Q'')
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')),
    Eq (α := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
            (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)) :
        CliffordAlgebra Q'')
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'')
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
        CliffordAlgebra Q'')
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')

Tactic:
induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
      LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
      add_comm (_ : CliffordAlgebra Q'')]

Premises used: map_sub, Algebra.algebraMap, LinearMap.add_apply, CliffordAlgebra.changeForm_ι_mul, map_add, add_comm, sub_sub, CliffordAlgebra.changeForm_contractLeft, CliffordAlgebra.changeForm_algebraMap