-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem conjAct_smul_ι_mem_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q)
    [Invertible (2 : R)] (m : M) :
    ConjAct.toConjAct x • ι Q m ∈ LinearMap.range (ι Q)

Proof state:
case inv_mem.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)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI : Invertible (ι Q a) := by rwa [ha]

Result:
case inv_mem.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)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝ : Invertible ↑x := x.invertible
this : Invertible ((ι Q) a) := ⋯.mpr this✝
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case mem.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)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI := x.invertible

Result:
case mem.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)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case inv_mem.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)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, LinearMap.mem_range_self]

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)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ Invertible ((ι Q) a)

Tactic:
rwa [ha]

Result:
no goals

Proof state:
case mul.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)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ LinearMap.range (ι Q)
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ LinearMap.range (ι Q)
m z' : M
hz' : (ι Q) z' = ↑z * (ι Q) m * ↑z⁻¹
y' : M
hy' : (ι Q) y' = ↑y * (ι Q) z' * ↑y⁻¹
⊢ ↑y * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
simp_rw [← hz', ← hy', LinearMap.mem_range_self]

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 ∈ lipschitzGroup Q
inst✝ : Invertible 2
m : M
⊢ ConjAct.toConjAct x • (ι Q) m ∈ LinearMap.range (ι Q)

Tactic:
unfold lipschitzGroup 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 ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
inst✝ : Invertible 2
m : M
⊢ ConjAct.toConjAct x • (ι Q) m ∈ LinearMap.range (ι Q)