awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
y : CliffordAlgebra Q
⊢ HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) y =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
have rw : 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) y) =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
      (x * y) -
    HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
Tactic: rw [mul_assoc, ← mul_assoc _ _ y, ι_mul_ι_comm, sub_mul, mul_sub, Algebra.left_comm, mul_assoc,
    mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
y : CliffordAlgebra Q
rw :
  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) y) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
⊢ HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) y =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
have rw₁ : x *
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      y) =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
      (x * y) -
    HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
Tactic: rw [mul_assoc, ← mul_assoc _ _ y, ι_mul_ι_comm, sub_mul, mul_sub, Algebra.left_comm, mul_assoc,
    mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
y : CliffordAlgebra Q
rw :
  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) y) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
rw₁ :
  x *
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        y) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
⊢ HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) y =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
have rw₂ : x *
    (((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)) *
      y) =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
      (x * y) -
    HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
Tactic: rw [mul_assoc, ← mul_assoc _ _ y, ι_mul_ι_comm, sub_mul, mul_sub, Algebra.left_comm, mul_assoc,
    mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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) =
    0
have rw : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0) 0
Tactic: rw [ι_mul_ι_add_swap, h.polar_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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))
Tactic: rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [← mul_assoc, ι_mul_ι_comm_of_isOrtho h, neg_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← mul_assoc, ι_mul_ι_comm_of_isOrtho h, neg_mul, mul_assoc]