-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv (hypothesis)
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
m₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
h2 :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
⊢ HSub.hSub (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
              ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
            HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
              ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) +
          HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ • e0 Q)
            ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) -
        HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)))
      ((algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) :
        CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
            ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
            ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) +
          HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ • e0 Q)
            ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) +
        HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q) +
      r₁ • e0 Q * r₂ • e0 Q
have h3 : -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
  r₁ • e0 Q * r₂ • e0 Q
Tactic: have h3 : -algebraMap R _ (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q := by
                  rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]