-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (goal)
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)))
⊢ 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)))
have 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)))
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]
Cleared hypotheses: x