-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) : star x ∈ pinGroup Q

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : (Units.coeHom (CliffordAlgebra Q)) y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Tactic:
simp only [Units.coeHom_apply] at hy₂

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : y * star y = 1
⊢ star y ∈ lipschitzGroup Q

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

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : y⁻¹ * (y * star y) = y⁻¹ * 1
⊢ star y ∈ lipschitzGroup Q

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = star x

Tactic:
refine ⟨star y, ?_, by simp only [hy₂, Units.coe_star]⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₁ : y ∈ ↑(lipschitzGroup Q).toSubmonoid
hy₂ : (Units.coeHom (CliffordAlgebra Q)) y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

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

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : (Units.coeHom (CliffordAlgebra Q)) y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ↑(y * star y) = ↑1

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

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q

Tactic:
rw [← hy₂] at hx₃

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx :
  x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧ x ∈ unitary (CliffordAlgebra Q)
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Tactic:
rcases hx with ⟨⟨y, hy₁, hy₂⟩, _hx₂, hx₃⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₁ : y ∈ ↑(lipschitzGroup Q).toSubmonoid
hy₂ : (Units.coeHom (CliffordAlgebra Q)) y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : star y = y⁻¹
⊢ star y ∈ lipschitzGroup Q

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

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : x ∈ pinGroup Q
⊢ star x ∈ pinGroup Q

Tactic:
rw [mem_iff] at hx ⊢

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx :
  x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧ x ∈ unitary (CliffordAlgebra Q)
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧
    star x ∈ unitary (CliffordAlgebra Q)

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : y⁻¹ * (y * star y) = y⁻¹ * 1
⊢ star y ∈ lipschitzGroup Q

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

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : star y = y⁻¹
⊢ star y ∈ lipschitzGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx :
  x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧ x ∈ unitary (CliffordAlgebra Q)
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧
    star x ∈ unitary (CliffordAlgebra Q)

Tactic:
refine ⟨?_, unitary.star_mem hx.2⟩

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx :
  x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧ x ∈ unitary (CliffordAlgebra Q)
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid