-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q)
h₁ :
  ∀ (x : M),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
        CliffordAlgebra Q)
h₂ :
  ∀ (a b : CliffordAlgebra Q)
    (ha :
      Eq (α := CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
          CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
          CliffordAlgebra Q))
    (hb :
      Eq (α := CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
          CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
          CliffordAlgebra Q)),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b)) :
        CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
have h₃ : ∀ (a b : CliffordAlgebra Q)
  (ha :
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
        CliffordAlgebra Q))
  (hb :
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
        CliffordAlgebra Q)),
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a + b)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a + b)) :
      CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap => simp
  | ι => simp
  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
  | add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]
Cleared hypotheses: x