awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
rw :
  HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A)) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
rw₁ :
  HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
rw₂ rw₃ :
  HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a + b) : A) ((f : (a : M) → A) (a + b) : A) -
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)

Tactic:
rw [hf, hf, hf]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
rw :
  HSub.hSub (α := A) (β := A)
      ((algebraMap R A : (a : R) → A)
          (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R)) :
        A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
    (algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R))
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := A)
    ((algebraMap R A : (a : R) → A)
        (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
          ((Q : (a : M) → R) b : R)) :
      A)
    ((algebraMap R A : (a : R) → A)
        (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
          ((Q : (a : M) → R) b : R)) :
      A)
⊢ HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
    (algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R))

Tactic:
rw [← map_sub, ← map_sub]

Premises used: map_sub
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
simp_rw :
  (∀ (x : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
    ∀ (x x_1 : M),
      Eq.{u_4 + 1} (α := A)
        ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
        ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                      (Algebra.linearMap R A) :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
⊢ (∀ (x : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
    LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f =
      LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
        (Algebra.linearMap R A)

Tactic:
simp_rw [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
⊢ (∀ (x : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
    ∀ (x x_1 : M),
      Eq.{u_4 + 1} (α := A)
        ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
        ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                      (Algebra.linearMap R A) :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)

Tactic:
⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩

Premises used: CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq, Iff.intro
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
refine :
  ∀
    (h :
      ∀ (x x_1 : M),
        Eq.{u_4 + 1} (α := A)
          ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f +
                        LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                      (a : M) → M →ₗ[R] A)
                    x :
                  M →ₗ[R] A) :
                (a : M) → A)
              x_1 :
            A)
          ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                        (Algebra.linearMap R A) :
                      (a : M) → M →ₗ[R] A)
                    x :
                  M →ₗ[R] A) :
                (a : M) → A)
              x_1 :
            A))
    (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
⊢ (∀ (x : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
    ∀ (x x_1 : M),
      Eq.{u_4 + 1} (α := A)
        ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
        ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                      (Algebra.linearMap R A) :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)

Tactic:
refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
h :
  ∀ (x x_1 : M),
    Eq.{u_4 + 1} (α := A)
      ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          x_1 :
        A)
      ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                    (Algebra.linearMap R A) :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          x_1 :
        A)
x : M
⊢ ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)

Tactic:
change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticMap.polar Q x y) at h
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
x : M
h :
  ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
apply :
  2 * HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)

Tactic:
apply h2.mul_left_cancel

Premises used: IsUnit.mul_left_cancel
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
x : M
h :
  ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
rw₂ :
  (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x x) =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
rw₃ :
  (algebraMap R A : (a : R) → A) (HSMul.hSMul (α := ℕ) (β := R) 2 ((Q : (a : M) → R) x : R)) =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
rw₄ :
  (algebraMap R A : (a : R) → A) (HAdd.hAdd (α := R) (β := R) ((Q : (a : M) → R) x : R) ((Q : (a : M) → R) x : R)) =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
rw₅ rw₆ :
  HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A) =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
⊢ 2 * HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)

Tactic:
rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]

Premises used: two_smul, two_mul, QuadraticMap.polar_self, map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
a b : M
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) +
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b)

Tactic:
mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _

Premises used: CliffordAlgebra.ι_sq_scalar, CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
a b : M
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)

Tactic:
eq_sub_of_add_eq (ι_mul_ι_add_swap a b)

Premises used: eq_sub_of_add_eq, CliffordAlgebra.ι_mul_ι_add_swap
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
a b : M
h : QuadraticMap.IsOrtho Q a b
rw : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0) 0
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) +
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    0

Tactic:
rw [ι_mul_ι_add_swap, h.polar_eq_zero]

Premises used: CliffordAlgebra.ι_mul_ι_add_swap, QuadraticMap.IsOrtho.polar_eq_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) =
    -HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)

Tactic:
eq_neg_of_add_eq_zero_left <| ι_mul_ι_add_swap_of_isOrtho h

Premises used: eq_neg_of_add_eq_zero_left, CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
rw :
  x *
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) =
    -HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₁ :
  x *
      -HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    -HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₂ :
  -(x *
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) =
    -HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₃ rw₄ :
  -(x *
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) =
    -(x *
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q))
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) =
    -HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)

Tactic:
rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]

Premises used: mul_assoc, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, mul_neg
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
rw :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      x =
    -HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) x)
rw₁ :
  -HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
      x =
    -HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) x)
rw₂ :
  -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
        x) =
    -HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) x)
rw₃ rw₄ :
  -HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) x) =
    -HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) x)
⊢ HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) x) =
    -HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) x)

Tactic:
rw [← mul_assoc, ι_mul_ι_comm_of_isOrtho h, neg_mul, mul_assoc]

Premises used: mul_assoc, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, neg_mul