-- 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 Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
simp_rw :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
simp_rw₁ :
  HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
simp_rw₂ :
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q' : (a : M) → R) m₂ : R)
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
simp_rw₃ :
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((-Q : (a : M) → R) m₂ : R)
      (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
⊢ HMul.hMul (α := ↥(even Q')) (β := ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₂ :
        ↥(even Q'))
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₂ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q')) =
    HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
      ((((-(even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
        ↥(even Q'))
have simp_rw₄ : HSMul.hSMul (α := R) (β := ↥(even Q')) (-(Q : (a : M) → R) m₂ : R)
    (((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q')) =
  HSMul.hSMul (α := R) (β := ↥(even Q')) ((Q : (a : M) → R) m₂ : R)
    (-((((even.ι Q').bilin : (a : M) → M →ₗ[R] ↥(even Q')) m₁ : M →ₗ[R] ↥(even Q')) : (a : M) → ↥(even Q')) m₃ :
      ↥(even Q'))
Tactic: simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h,
          QuadraticMap.neg_apply, smul_neg, neg_smul]