awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) x
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
have add₂ : x + y = x + y
Tactic: rw [map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
have ι_mul_ι_mul : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
    x
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul_ι_mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
have ι_mul_ι_mul₁ : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
        CliffordAlgebra Q))
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
    x
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul_ι_mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
ι_mul_ι_mul₁ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁) :
          CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
          CliffordAlgebra Q))
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
have ι_mul_ι_mul₂ : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      (-(ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
        CliffordAlgebra Q))
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
    x
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
h : x ∈ evenOdd Q 0
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have algebraMap : ∀ (r : R),
  Eq (α := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: induction x, h using even_induction with
  | algebraMap r => exact AlgHom.commutes _ _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
h : x ∈ evenOdd Q 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have add : ∀ (x y : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 0) (_hy : y ∈ evenOdd Q 0)
  (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x)
  (ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y),
  (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
Tactic: induction x, h using even_induction with
  | algebraMap r => exact AlgHom.commutes _ _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
h : x ∈ evenOdd Q 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 0) (_hy : y ∈ evenOdd Q 0)
    (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x)
    (ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 0)
  (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x),
  (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x
Tactic: induction x, h using even_induction with
  | algebraMap r => exact AlgHom.commutes _ _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
have add : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  -(x + y)
Tactic: rw [map_add, ihx, ihy, neg_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
have add₁ : HAdd.hAdd (β := CliffordAlgebra Q) (-x)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  -(x + y)
Tactic: rw [map_add, ihx, ihy, neg_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) (-x)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
have add₂ : -x + -y = -(x + y)
Tactic: rw [map_add, ihx, ihy, neg_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) (-x)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
add₂ : -x + -y = -(x + y)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
have add₃ : -x + -y = -x + -y
Tactic: rw [map_add, ihx, ihy, neg_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
have ι_mul_ι_mul : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x)
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ι_mul_ι_mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
have ι_mul_ι_mul₁ : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
        CliffordAlgebra Q))
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x)
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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_1 : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ι_mul_ι_mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
ι_mul_ι_mul₁ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁) :
          CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
          CliffordAlgebra Q))
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x) =
    -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x)
have ι_mul_ι_mul₂ : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      (-(ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
        CliffordAlgebra Q))
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      x)
Tactic: rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
h : x ∈ evenOdd Q 1
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
have ι : ∀ (m : M),
  Eq (α := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: induction x, h using odd_induction with
  | ι m => exact involute_ι _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy, neg_add]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
h : x ∈ evenOdd Q 1
ι :
  ∀ (m : M),
    Eq (α := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m) :
        CliffordAlgebra Q)
      (-(CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
have add : ∀ (x y : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 1) (_hy : y ∈ evenOdd Q 1)
  (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x)
  (ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y),
  (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
Tactic: induction x, h using odd_induction with
  | ι m => exact involute_ι _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy, neg_add]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
Cleared hypotheses: h