awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
y : (CliffordAlgebra Q)ˣ
hy₁ : y ∈ (↑(lipschitzGroup Q).toSubmonoid : Set (CliffordAlgebra Q)ˣ)
hy₂ : (Units.coeHom (CliffordAlgebra Q) : (a : (CliffordAlgebra Q)ˣ) → CliffordAlgebra Q) y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    (star x)
have hy₃ : y ∈ lipschitzGroup Q
Tactic: simp only [Subgroup.coe_toSubmonoid, SetLike.mem_coe] at hy₁
Cleared hypotheses: hy₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ∃ x_1 ∈ lipschitzGroup Q, (↑x_1 : CliffordAlgebra Q) = star x
have refine : star y ∈ lipschitzGroup Q
Tactic: refine ⟨star y, ?_, by simp only [hy₂, Units.coe_star]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q
have hx₄ : (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1
Tactic: rw [← hy₂] at hx₃
Cleared hypotheses: hx₃, hy₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ y * star y = 1
have rw : (↑(y * star y) : CliffordAlgebra Q) = (↑1 : CliffordAlgebra Q)
Tactic: rw [← Units.val_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q
have hy₃ : y * star y = 1
Tactic: have hy₃ : y * star y = 1 := by
    rw [← Units.val_inj]
    simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : y * star y = 1
⊢ star y ∈ lipschitzGroup Q
have hy₄ : y⁻¹ * (y * star y) = y⁻¹ * 1
Tactic: apply_fun fun x => y⁻¹ * x at hy₃
Cleared hypotheses: hy₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : y⁻¹ * (y * star y) = y⁻¹ * 1
⊢ star y ∈ lipschitzGroup Q
have hy₄ : star y = y⁻¹
Tactic: simp only [inv_mul_cancel_left, mul_one] at hy₃
Cleared hypotheses: hy₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
⊢ star x ∈ pinGroup Q ↔ x ∈ pinGroup Q
have refine : star x ∈ pinGroup Q → x ∈ pinGroup Q
Tactic: refine ⟨?_, star_mem⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
hx : star x ∈ pinGroup Q
⊢ x ∈ pinGroup Q
have h : x = star (star x)
Tactic: convert! star_mem hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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)ˣ
hx : (↑x : CliffordAlgebra Q) ∈ spinGroup Q
y : M
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑x : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q)
have rw : HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
    (↑x⁻¹ : CliffordAlgebra Q) =
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
    ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
    ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q)
Tactic: rw [involute_eq hx, @ConjAct.units_smul_def, @ConjAct.ofConjAct_toConjAct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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)ˣ
hx : (↑x : CliffordAlgebra Q) ∈ spinGroup Q
y : M
rw :
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑x : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q)
have rw₁ : HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
    (↑x⁻¹ : CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((↑((ConjAct.ofConjAct : (a : ConjAct (CliffordAlgebra Q)ˣ) → (CliffordAlgebra Q)ˣ)
              ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x)) :
          CliffordAlgebra Q) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
    (↑((ConjAct.ofConjAct : (a : ConjAct (CliffordAlgebra Q)ˣ) → (CliffordAlgebra Q)ˣ)
            ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x))⁻¹ :
      CliffordAlgebra Q)
Tactic: rw [involute_eq hx, @ConjAct.units_smul_def, @ConjAct.ofConjAct_toConjAct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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)ˣ
hx : (↑x : CliffordAlgebra Q) ∈ spinGroup Q
y : M
rw :
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q)
rw₁ :
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((↑((ConjAct.ofConjAct : (a : ConjAct (CliffordAlgebra Q)ˣ) → (CliffordAlgebra Q)ˣ)
                ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x)) :
            CliffordAlgebra Q) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑((ConjAct.ofConjAct : (a : ConjAct (CliffordAlgebra Q)ˣ) → (CliffordAlgebra Q)ˣ)
              ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x))⁻¹ :
        CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑x : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q)
have rw₂ : HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
    (↑x⁻¹ : CliffordAlgebra Q) =
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) y : CliffordAlgebra Q) *
    (↑x⁻¹ : CliffordAlgebra Q)
Tactic: rw [involute_eq hx, @ConjAct.units_smul_def, @ConjAct.ofConjAct_toConjAct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
hx : x ∈ spinGroup Q
⊢ star x ∈ spinGroup Q
have hx₁ : x ∈ pinGroup Q ∧ x ∈ even Q
Tactic: rw [mem_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
hx : x ∈ pinGroup Q ∧ x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q
have hx₁ : x ∈ pinGroup Q
Tactic: obtain ⟨hx₁, hx₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
hx : x ∈ pinGroup Q ∧ x ∈ even Q
hx₁ : x ∈ pinGroup Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q
have hx₂ : x ∈ even Q
Tactic: obtain ⟨hx₁, hx₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q
have refine : star x ∈ even Q
Tactic: refine ⟨pinGroup.star_mem hx₁, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯
⊢ star x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯
have hx₃ : x ∈ evenOdd Q 0
Tactic: simp only [Submodule.mem_toSubalgebra] at hx₂ ⊢
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
⊢ star x ∈ spinGroup Q ↔ x ∈ spinGroup Q
have refine : star x ∈ spinGroup Q → x ∈ spinGroup Q
Tactic: refine ⟨?_, star_mem⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (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
hx : star x ∈ spinGroup Q
⊢ x ∈ spinGroup Q
have h : x = star (star x)
Tactic: convert! star_mem hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
m : M
⊢ Eq (α := CliffordAlgebra Q) (star ((ι Q : (a : M) → CliffordAlgebra Q) m) : CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have rw : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → 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: rw [star_def, involute_ι, map_neg, reverse_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
m : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q) (star ((ι Q : (a : M) → CliffordAlgebra Q) m) : CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have rw₁ : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (-(ι Q : (a : M) → CliffordAlgebra Q) m) : CliffordAlgebra Q)
  (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [star_def, involute_ι, map_neg, reverse_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
m : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (-(ι Q : (a : M) → CliffordAlgebra Q) m) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q) (star ((ι Q : (a : M) → CliffordAlgebra Q) m) : CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have rw₂ : Eq (α := CliffordAlgebra Q)
  (-(reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) : CliffordAlgebra Q)
  (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [star_def, involute_ι, map_neg, reverse_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
m : M
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (-(ι Q : (a : M) → CliffordAlgebra Q) m) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
rw₂ :
  Eq (α := CliffordAlgebra Q)
    (-(reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q) (star ((ι Q : (a : M) → CliffordAlgebra Q) m) : CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have rw₃ : Eq (α := CliffordAlgebra Q) (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
  (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [star_def, involute_ι, map_neg, reverse_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
r : R
x : CliffordAlgebra Q
⊢ star (r • x) = r • star x
have rw : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
  r • star x
Tactic: rw [star_def, star_def, map_smul, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
r : R
x : CliffordAlgebra Q
rw :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
    r • star x
⊢ star (r • x) = r • star x
have rw₁ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
  HSMul.hSMul (β := CliffordAlgebra Q) r
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
Tactic: rw [star_def, star_def, map_smul, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
r : R
x : CliffordAlgebra Q
rw :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
    r • star x
rw₁ :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
    HSMul.hSMul (β := CliffordAlgebra Q) r
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
⊢ star (r • x) = r • star x
have rw₂ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
    (HSMul.hSMul (β := CliffordAlgebra Q) r
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
  HSMul.hSMul (β := CliffordAlgebra Q) r
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
Tactic: rw [star_def, star_def, map_smul, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
r : R
x : CliffordAlgebra Q
rw :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
    r • star x
rw₁ :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (r • x)) =
    HSMul.hSMul (β := CliffordAlgebra Q) r
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
rw₂ :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HSMul.hSMul (β := CliffordAlgebra Q) r
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    HSMul.hSMul (β := CliffordAlgebra Q) r
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
⊢ star (r • x) = r • star x
have rw₃ : HSMul.hSMul (β := CliffordAlgebra Q) r
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q) =
  HSMul.hSMul (β := CliffordAlgebra Q) r
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
Tactic: rw [star_def, star_def, map_smul, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
r : R
⊢ Eq (α := CliffordAlgebra Q)
    (star ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) : CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have rw : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → 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: rw [star_def, involute.commutes, reverse.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (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
r : R
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → 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)
⊢ Eq (α := CliffordAlgebra Q)
    (star ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) : CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have rw₁ : Eq (α := CliffordAlgebra Q)
  ((reverse : (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: rw [star_def, involute.commutes, reverse.commutes]