-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : 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
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q')
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q')
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (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')
            ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              x) :
          CliffordAlgebra Q')
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
          CliffordAlgebra Q'))
    (hy :
      Eq (α := CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
            ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              y) :
          CliffordAlgebra Q')
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
          CliffordAlgebra Q')),
    Eq (α := CliffordAlgebra Q')
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            (x + y)) :
        CliffordAlgebra Q')
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
        CliffordAlgebra Q')
⊢ Eq (α := CliffordAlgebra Q')
    ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x) :
      CliffordAlgebra Q')
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (a : CliffordAlgebra Q') → CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q')
have ι_mul : ∀ (x : CliffordAlgebra Q) (m : M)
  (hx :
    Eq (α := CliffordAlgebra Q')
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            x) :
        CliffordAlgebra Q')
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
        CliffordAlgebra Q')),
  Eq (α := CliffordAlgebra Q')
    ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)) :
      CliffordAlgebra Q')
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') d :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (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')
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, map_smul]
    rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]
Cleared hypotheses: x