awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(pinGroup Q)
⊢ star x * x = 1

Tactic:
Subtype.ext <| coe_star_mul_self x

Premises used: pinGroup.coe_star_mul_self, Subtype.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(pinGroup Q)
⊢ x * star x = 1

Tactic:
Subtype.ext <| coe_mul_star_self x

Premises used: pinGroup.coe_mul_star_self, Subtype.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(pinGroup Q)
⊢ star x = x⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ Eq (α := ↥(pinGroup Q) → ↥(pinGroup Q)) star Inv.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ Function.Injective (α := ↥(pinGroup Q)) (β := (CliffordAlgebra Q)ˣ)
    (⇑toUnits : (a : ↥(pinGroup Q)) → (CliffordAlgebra Q)ˣ)

Tactic:
fun _x _y h => Subtype.ext <| Units.ext_iff.mp h

Premises used: Units.ext_iff, Iff.mp, Function.Injective, Subtype.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ spinGroup Q ↔ x ∈ pinGroup Q ∧ x ∈ even Q

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ pinGroup Q

Tactic:
hx.1

Premises used: Set.Mem, And.left
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ even Q

Tactic:
hx.2

Premises used: Set.Mem, And.right
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ lipschitzGroup Q

Tactic:
pinGroup.units_mem_lipschitzGroup (mem_pin hx)

Premises used: pinGroup.units_mem_lipschitzGroup, spinGroup.mem_pin
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x

Tactic:
involute_eq_of_mem_even (mem_even hx)

Premises used: spinGroup.mem_even, CliffordAlgebra.involute_eq_of_mem_even
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [involute_eq hx, @ConjAct.units_smul_def, @ConjAct.ofConjAct_toConjAct]

Premises used: ConjAct.units_smul_def, ConjAct.ofConjAct_toConjAct, spinGroup.involute_eq
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
inst_3 : Invertible (α := R) 2
y : M
⊢ 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) ∈
    (ι Q).range

Tactic:
lipschitzGroup.conjAct_smul_ι_mem_range_ι (units_mem_lipschitzGroup hx) y

Premises used: spinGroup.units_mem_lipschitzGroup, lipschitzGroup.conjAct_smul_ι_mem_range_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
inst_3 : Invertible (α := R) 2
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) ∈
    (ι Q).range

Tactic:
lipschitzGroup.involute_act_ι_mem_range_ι (units_mem_lipschitzGroup hx) y

Premises used: spinGroup.units_mem_lipschitzGroup, lipschitzGroup.involute_act_ι_mem_range_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
inst_3 : Invertible (α := R) 2
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range =
    (ι Q).range

Tactic:
lipschitzGroup.conjAct_smul_range_ι (units_mem_lipschitzGroup hx)

Premises used: spinGroup.units_mem_lipschitzGroup, lipschitzGroup.conjAct_smul_range_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 * x = 1

Tactic:
hx.1.2.1

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x * star x = 1

Tactic:
hx.1.2.2

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ pinGroup Q ∧ x ∈ even Q

Tactic:
rw [mem_iff] at hx ⊢

Premises used: spinGroup.mem_iff
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ pinGroup Q

Tactic:
obtain ⟨hx₁, hx₂⟩ := hx
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ x ∈ even Q

Tactic:
obtain ⟨hx₁, hx₂⟩ := hx
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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

Tactic:
⟨pinGroup.star_mem hx₁, ?_⟩

Premises used: pinGroup.star_mem, And.intro
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
refine : star x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q

Tactic:
refine ⟨pinGroup.star_mem hx₁, ?_⟩
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 ⋯ ⋯
⊢ x ∈ evenOdd Q 0

Tactic:
simp only [Submodule.mem_toSubalgebra] at hx₂ ⊢

Premises used: Submodule.mem_toSubalgebra
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ star x ∈ evenOdd Q 0

Tactic:
simp only [star_def, reverse_mem_evenOdd_iff, involute_mem_evenOdd_iff, hx₂]

Premises used: CliffordAlgebra.star_def, CliffordAlgebra.involute_mem_evenOdd_iff, CliffordAlgebra.reverse_mem_evenOdd_iff
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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

Tactic:
⟨?_, star_mem⟩

Premises used: spinGroup.star_mem, Iff.intro
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
refine : star x ∈ spinGroup Q → x ∈ spinGroup Q
⊢ star x ∈ spinGroup Q ↔ x ∈ spinGroup Q

Tactic:
refine ⟨?_, star_mem⟩
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ star (star x) ∈ spinGroup Q

Tactic:
star_mem hx

Premises used: spinGroup.star_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
h : x = star (star x)
⊢ x ∈ spinGroup Q

Tactic:
convert! star_mem hx

Premises used: spinGroup.star_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 = star (star x)

Tactic:
(star_star x).symm

Premises used: star_star, Eq.symm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 = star (star x)

Tactic:
exact (star_star x).symm

Premises used: star_star, Eq.symm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(spinGroup Q)
⊢ (↑(star x) : CliffordAlgebra Q) = star (↑x : CliffordAlgebra Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(spinGroup Q)
⊢ star (↑x : CliffordAlgebra Q) * (↑x : CliffordAlgebra Q) = 1

Tactic:
star_mul_self_of_mem x.prop

Premises used: Subtype.prop, spinGroup.star_mul_self_of_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(spinGroup Q)
⊢ (↑x : CliffordAlgebra Q) * (↑(star x) : CliffordAlgebra Q) = 1

Tactic:
mul_star_self_of_mem x.prop

Premises used: spinGroup.mul_star_self_of_mem, Subtype.prop
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(spinGroup Q)
⊢ star x * x = 1

Tactic:
Subtype.ext <| coe_star_mul_self x

Premises used: spinGroup.coe_star_mul_self, Subtype.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(spinGroup Q)
⊢ x * star x = 1

Tactic:
Subtype.ext <| coe_mul_star_self x

Premises used: spinGroup.coe_mul_star_self, Subtype.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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 : ↥(spinGroup Q)
⊢ star x = x⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ Eq (α := ↥(spinGroup Q) → ↥(spinGroup Q)) star Inv.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
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
⊢ Function.Injective (α := ↥(spinGroup Q)) (β := (CliffordAlgebra Q)ˣ)
    (⇑toUnits : (a : ↥(spinGroup Q)) → (CliffordAlgebra Q)ˣ)

Tactic:
fun _x _y h => Subtype.ext <| Units.ext_iff.mp h

Premises used: Units.ext_iff, Iff.mp, Function.Injective, Subtype.ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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
⊢ (fun (x : CliffordAlgebra Q) ↦
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
          CliffordAlgebra Q))
      ((fun (x : CliffordAlgebra Q) ↦
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
            CliffordAlgebra Q))
        x) =
    x

Tactic:
simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute]

Premises used: CliffordAlgebra.reverse_involute_commute, Function.Semiconj.eq, CliffordAlgebra.reverse_reverse, CliffordAlgebra.involute_involute
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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 y : CliffordAlgebra Q
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x * y)) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y) :
        CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)

Tactic:
simp only [map_mul, reverse.map_mul]

Premises used: CliffordAlgebra.reverse.map_mul, map_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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 y : CliffordAlgebra Q
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y)) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y) :
        CliffordAlgebra Q)

Tactic:
simp only [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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 =
    (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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 =
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)

Tactic:
reverse_involute _

Premises used: CliffordAlgebra.reverse_involute
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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)
rw₃ rw₄ :
  Eq (α := 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)

Tactic:
rw [star_def, involute_ι, map_neg, reverse_ι]

Premises used: CliffordAlgebra.star_def, map_neg, CliffordAlgebra.involute_ι, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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)
rw₃ 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)
⊢ star (r • x) = r • star x

Tactic:
rw [star_def, star_def, map_smul, map_smul]

Premises used: CliffordAlgebra.star_def, map_smul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Star
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)
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)
rw₂ rw₃ :
  Eq (α := 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)

Tactic:
rw [star_def, involute.commutes, reverse.commutes]

Premises used: CliffordAlgebra.star_def, CliffordAlgebra.reverse.commutes, AlgHom.commutes, CliffordAlgebra.involute