-- 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
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)) ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (((f : (a : M × R) → M × R →ₗ[R] CliffordAlgebra Q) x : M × R →ₗ[R] CliffordAlgebra Q) :
          (a : M × R) → CliffordAlgebra Q)
        y =
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) x.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) x.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) y.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) y.2 : CliffordAlgebra Q)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) x
hm :
  ∀ (m : M × R),
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m.1 : CliffordAlgebra Q) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m.2 : CliffordAlgebra Q) =
      (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)
m₁ m₂ m₃ : M × R
refine_2 :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
      (HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q)) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
      HSMul.hSMul (α := R) ((Q' Q : (a : M × R) → R) m₂ : R)
        (HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q))
refine_2₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
          HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
        HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
      HSMul.hSMul (α := R) ((Q' Q : (a : M × R) → R) m₂ : R)
        (HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q))
refine_2₂ :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
        (HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
          HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q)) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
      HSMul.hSMul (α := R) ((Q' Q : (a : M × R) → R) m₂ : R)
        (HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q))
refine_2₃ :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q) -
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q)) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
      HSMul.hSMul (α := R) ((Q' Q : (a : M × R) → R) m₂ : R)
        (HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q))
⊢ HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
      (HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q)) =
    HSMul.hSMul (α := R) ((Q' Q : (a : M × R) → R) m₂ : R)
      (HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
        HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q))
have refine_2₄ : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂.1 : CliffordAlgebra Q) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₂.2 : CliffordAlgebra Q)) *
    HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q) =
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁.1 : CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₁.2 : CliffordAlgebra Q) *
    HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m₂) :
        CliffordAlgebra Q)
      (HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₃.1 : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) m₃.2 : CliffordAlgebra Q))
Tactic: rw [← mul_smul_comm, ← mul_assoc, mul_assoc (_ + _), ← (hc _ _).symm.mul_self_sub_mul_self_eq',
      Algebra.smul_def, ← mul_assoc, hm]