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 : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this_1 :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
this :
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x⁻¹ :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range) ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range
⊢ (ι Q).range =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x⁻¹ :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range)

Tactic:
simp only [map_inv, smul_inv_smul]

Premises used: map_inv, smul_inv_smul
-- 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 ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
suffices :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range =
    (ι Q).range

Tactic:
suffices ∀ x ∈ lipschitzGroup Q,
      ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) by
    apply le_antisymm
    · exact this _ hx
    · have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)
      refine Eq.trans_le ?_ this
      simp only [map_inv, smul_inv_smul]
-- 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_1 : (CliffordAlgebra Q)ˣ
hx_1 : x_1 ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
rw :
  (ι Q).range ≤
    Submodule.comap
      (DistribSMul.toLinearMap R (S := ConjAct (CliffordAlgebra Q)ˣ) (CliffordAlgebra Q)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ))
      (ι Q).range
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range ≤
    (ι Q).range

Tactic:
rw [Submodule.pointwise_smul_def, Submodule.map_le_iff_le_comap]

Premises used: Submodule.pointwise_smul_def, Submodule.map_le_iff_le_comap
-- 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_1 : (CliffordAlgebra Q)ˣ
hx_1 : x_1 ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
m : M
⊢ Membership.mem (α := CliffordAlgebra Q)
    (Submodule.comap
      (DistribSMul.toLinearMap R (S := ConjAct (CliffordAlgebra Q)ˣ) (CliffordAlgebra Q)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ))
      (ι Q).range)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
conjAct_smul_ι_mem_range_ι hx _

Premises used: Set.Mem, setOf, lipschitzGroup.conjAct_smul_ι_mem_range_ι, Set.preimage, Set.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_1 : (CliffordAlgebra Q)ˣ
hx_1 : x_1 ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
m : M
⊢ Membership.mem (α := CliffordAlgebra Q)
    (Submodule.comap
      (DistribSMul.toLinearMap R (S := ConjAct (CliffordAlgebra Q)ˣ) (CliffordAlgebra Q)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ))
      (ι Q).range)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
exact conjAct_smul_ι_mem_range_ι hx _

Premises used: 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)ˣ
norm_cast : (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q
⊢ (∃ x_1 ∈ lipschitzGroup Q, (↑x_1 : CliffordAlgebra Q) = (↑x : CliffordAlgebra Q)) ↔ x ∈ lipschitzGroup Q

Tactic:
norm_cast
-- 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_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q

Tactic:
exists_eq_right

Premises used: Set.Mem, exists_eq_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)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q

Tactic:
exact exists_eq_right

Premises used: exists_eq_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
⊢ x ∈ pinGroup Q ↔
    Membership.mem (γ := Submonoid (CliffordAlgebra Q))
        (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
          (lipschitzGroup Q).toSubmonoid)
        x ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x

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 ∈ pinGroup Q
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    x

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 ∈ pinGroup Q
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x

Tactic:
hx.2

Premises used: Set.Mem, setOf, 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)ˣ
rw :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
        (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
          (lipschitzGroup Q).toSubmonoid)
        (↑x : CliffordAlgebra Q) ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q) ↔
    x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
rw₁ rw₂ :
  x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q) ↔
    x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
⊢ (↑x : CliffordAlgebra Q) ∈ pinGroup Q ↔
    x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)

Tactic:
rw [mem_iff, lipschitzGroup.coe_mem_iff_mem]

Premises used: pinGroup.mem_iff, lipschitzGroup.coe_mem_iff_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 : (↑x : CliffordAlgebra Q) ∈ pinGroup Q
⊢ x ∈ lipschitzGroup Q

Tactic:
(units_mem_iff.1 hx).1

Premises used: pinGroup.units_mem_iff, And.left, Iff.mp
-- 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) ∈ pinGroup 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: lipschitzGroup.conjAct_smul_ι_mem_range_ι, pinGroup.units_mem_lipschitzGroup
-- 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) ∈ pinGroup 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: pinGroup.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) ∈ pinGroup 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: pinGroup.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 ∈ pinGroup Q
⊢ star x * x = 1

Tactic:
hx.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 ∈ pinGroup Q
⊢ x * star x = 1

Tactic:
hx.2.2

Premises used: 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 ∈ pinGroup Q
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      x ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x

Tactic:
rw [mem_iff] at hx ⊢

Premises used: pinGroup.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 :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      x ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      (star x) ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (star x)

Tactic:
⟨?_, Unitary.star_mem hx.2⟩

Premises used: And.right, And.intro, Unitary.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 :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      x ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x
refine :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    (star x)
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      (star x) ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (star x)

Tactic:
refine ⟨?_, Unitary.star_mem hx.2⟩
-- 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 :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      x ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x
rcases :
  ∀ (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)
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    (star x)

Tactic:
rcases hx with ⟨⟨y, hy₁, hy₂⟩, _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
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
⊢ y ∈ lipschitzGroup Q

Tactic:
simp only [Subgroup.coe_toSubmonoid, SetLike.mem_coe] at hy₁

Premises used: SetLike.mem_coe, Subgroup.coe_toSubmonoid
-- 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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ (↑(star y) : CliffordAlgebra Q) = star x

Tactic:
simp only [hy₂, Units.coe_star]

Premises used: Units.coe_star
-- 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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
refine : star y ∈ lipschitzGroup Q
⊢ ∃ x_1 ∈ lipschitzGroup Q, (↑x_1 : CliffordAlgebra Q) = star x

Tactic:
refine ⟨star y, ?_, by simp only [hy₂, Units.coe_star]⟩
-- 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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1

Tactic:
rw [← hy₂] at 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
y : (CliffordAlgebra Q)ˣ
hy₂ : (↑y : CliffordAlgebra Q) = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
hx₄ : (↑y : CliffordAlgebra Q) * star (↑y : CliffordAlgebra Q) = 1
⊢ y ∈ lipschitzGroup Q

Tactic:
rw [← hy₂] at 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
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
rw : (↑(y * star y) : CliffordAlgebra Q) = (↑1 : CliffordAlgebra Q)
⊢ y * star y = 1

Tactic:
rw [← Units.val_inj]

Premises used: Units.val_inj
-- 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
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) : CliffordAlgebra Q) = (↑1 : CliffordAlgebra Q)

Tactic:
simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]

Premises used: Units.coe_star, Units.val_one, Units.val_mul
-- 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
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

Tactic:
have hy₃ : y * star y = 1 := by
    rw [← Units.val_inj]
    simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]
-- 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
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
⊢ y⁻¹ * (y * star y) = y⁻¹ * 1

Tactic:
apply_fun fun x => y⁻¹ * x at hy₃

Premises used: HMul.hMul, Inv.inv
-- 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
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 = y⁻¹

Tactic:
simp only [inv_mul_cancel_left, mul_one] at hy₃

Premises used: inv_mul_cancel_left, mul_one
-- 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
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₃ : star y = y⁻¹
⊢ star y ∈ lipschitzGroup Q

Tactic:
simp only [hy₃, hy₁, inv_mem_iff]

Premises used: inv_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
⊢ star x ∈ pinGroup Q ↔ x ∈ pinGroup Q

Tactic:
⟨?_, star_mem⟩

Premises used: pinGroup.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 ∈ pinGroup Q → x ∈ pinGroup Q
⊢ star x ∈ pinGroup Q ↔ x ∈ pinGroup 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 ∈ pinGroup Q
⊢ star (star x) ∈ pinGroup Q

Tactic:
star_mem hx

Premises used: pinGroup.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 ∈ pinGroup Q
h : x = star (star x)
⊢ x ∈ pinGroup Q

Tactic:
convert! star_mem hx

Premises used: pinGroup.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 ∈ pinGroup 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 ∈ pinGroup 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 : ↥(pinGroup 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 : ↥(pinGroup Q)
⊢ star (↑x : CliffordAlgebra Q) * (↑x : CliffordAlgebra Q) = 1

Tactic:
star_mul_self_of_mem x.prop

Premises used: Subtype.prop, pinGroup.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 : ↥(pinGroup Q)
⊢ (↑x : CliffordAlgebra Q) * (↑(star x) : CliffordAlgebra Q) = 1

Tactic:
mul_star_self_of_mem x.prop

Premises used: Subtype.prop, pinGroup.mul_star_self_of_mem