-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)))) :
        CliffordAlgebra (Q' Q))
      ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
          CliffordAlgebra (Q' Q)))
ι :
  ∀ (m : M),
    Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m)))) :
        CliffordAlgebra (Q' Q))
      ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m)) :
          CliffordAlgebra (Q' Q)))
mul :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
          CliffordAlgebra (Q' Q))
        ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
          (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q))))
    (hy :
      Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y))) :
          CliffordAlgebra (Q' Q))
        ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
          (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) y) : CliffordAlgebra (Q' Q)))),
    Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x * y)))) :
        CliffordAlgebra (Q' Q))
      ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) (x * y)) : CliffordAlgebra (Q' Q)))
add :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
          CliffordAlgebra (Q' Q))
        ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
          (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q))))
    (hy :
      Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
              ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y))) :
          CliffordAlgebra (Q' Q))
        ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
          (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) y) : CliffordAlgebra (Q' Q)))),
    Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y)))) :
        CliffordAlgebra (Q' Q))
      ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) (x + y)) : CliffordAlgebra (Q' Q)))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q)))

Tactic:
induction x using CliffordAlgebra.induction with
  | algebraMap r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
  | ι m =>
    simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
      reverse_ι, neg_e0_mul_v, map_neg]
  | mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
  | add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]

Premises used: CliffordAlgebra.ι, Algebra.algebraMap, CliffordAlgebra.EquivEven.reverse_e0, Subalgebra.coe_mul, CliffordAlgebra.EquivEven.neg_e0_mul_v, map_add, Subalgebra.coe_algebraMap, map_neg, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.reverse.commutes, map_mul, Subalgebra.coe_neg, CliffordAlgebra.involute_ι, CliffordAlgebra.toEven_ι, AlgHom.commutes, Subalgebra.coe_add, CliffordAlgebra.EquivEven.reverse_v, CliffordAlgebra.reverse_ι