awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 × 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) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q' Q : (a : M × R) → R) m)
have refine_1 : 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)
Tactic: rw [← (hc _ _).symm.mul_self_sub_mul_self_eq, hm]
-- 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
m₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ 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))
have rw : HMul.hMul (β := 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)) *
      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))
Tactic: rw [← mul_assoc, e0_mul_v_mul_e0]
-- 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
m₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
rw :
  HMul.hMul (β := 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)) *
        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))
⊢ 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))
have rw₁ : 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)) (β := 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))
Tactic: rw [← mul_assoc, e0_mul_v_mul_e0]
-- 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
⊢ 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 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))
Tactic: have h1 : e0 Q * v Q m₁ * (e0 Q * v Q m₂) = v Q m₁ * v Q m₂ := by
                  rw [← mul_assoc, e0_mul_v_mul_e0]
-- 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
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))
⊢ -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)
have rw : -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)) =
  r₂ •
    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)) (e0 Q)
Tactic: rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
-- 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
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))
rw :
  -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)) =
    r₂ •
      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)) (e0 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)
have rw₁ : -(r₂ •
      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))) =
  r₂ •
    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)) (e0 Q)
Tactic: rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
-- 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
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))
rw :
  -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)) =
    r₂ •
      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)) (e0 Q)
rw₁ :
  -(r₂ •
        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))) =
    r₂ •
      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)) (e0 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)
have rw₂ : r₂ •
    -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)) =
  r₂ •
    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)) (e0 Q)
Tactic: rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
-- 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
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))
rw :
  -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)) =
    r₂ •
      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)) (e0 Q)
rw₁ :
  -(r₂ •
        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))) =
    r₂ •
      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)) (e0 Q)
rw₂ :
  r₂ •
      -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)) =
    r₂ •
      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)) (e0 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)
have rw₃ : r₂ •
    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)) (e0 Q) =
  r₂ •
    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)) (e0 Q)
Tactic: rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
-- 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))
⊢ 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 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)
Tactic: have h2 : -(r₂ • e0 Q * v Q m₁) = v Q m₁ * r₂ • e0 Q := by
                  rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
-- 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
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)
⊢ -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
    r₁ • e0 Q * r₂ • e0 Q
have rw : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = r₁ • e0 Q * r₂ • e0 Q
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]