-- 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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul_ι_mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
ι_mul_ι_mul₁ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁) :
          CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
          CliffordAlgebra Q))
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
ι_mul_ι_mul₂ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (-(ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
          CliffordAlgebra Q))
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
ι_mul_ι_mul₃ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (-(ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        (-(ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q))
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
have ι_mul_ι_mul₄ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      (-(ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      (-(ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
    x =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
    x
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]