-- 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 one
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
m : M
⊢ ↑1 * (ι Q) m * ↑1⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
simp_rw [inv_one, Units.val_one, one_mul, mul_one, LinearMap.mem_range_self]

Result:
no goals

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
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI := invertibleNeg (ι Q a)

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✝²
this✝ : Invertible (Q a) := invertibleOfInvertibleι Q a
this : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι 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 ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
inst✝ : Invertible 2
m : M
⊢ ConjAct.toConjAct x • (ι Q) m ∈ LinearMap.range (ι Q)

Tactic:
rw [ConjAct.units_smul_def, ConjAct.ofConjAct_toConjAct]

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

Tactic:
induction hx using Subgroup.closure_induction'' generalizing m with
| mem x hx =>
  obtain ⟨a, ha⟩ := hx
  letI := x.invertible
  letI : Invertible (ι Q a) := by rwa [ha]
  letI : Invertible (Q a) := invertibleOfInvertibleι Q a
  simp_rw [← invOf_units x, ← ha, ι_mul_ι_mul_invOf_ι, LinearMap.mem_range_self]
| inv_mem x hx =>
  obtain ⟨a, ha⟩ := hx
  letI := x.invertible
  letI : Invertible (ι Q a) := by rwa [ha]
  letI : Invertible (Q a) := invertibleOfInvertibleι Q a
  letI := invertibleNeg (ι Q a)
  letI := Invertible.map involute (ι Q a)
  simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, LinearMap.mem_range_self]
| one => simp_rw [inv_one, Units.val_one, one_mul, mul_one, LinearMap.mem_range_self]
| mul y z _ _ hy hz =>
  simp_rw [mul_inv_rev, Units.val_mul]
  suffices ↑y * (↑z * ι Q m * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
    simpa only [mul_assoc] using this
  obtain ⟨z', hz'⟩ := hz m
  obtain ⟨y', hy'⟩ := hy z'
  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)ˣ
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 : M
this : ↑y * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.24496
⊢ ↑y * ↑z * (ι Q) m * (↑z⁻¹ * ↑y⁻¹) ∈ LinearMap.range (ι Q)

Tactic:
simpa only [mul_assoc] using this

Result:
no goals

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
this✝ : Invertible ↑x := x.invertible
this : Invertible ((ι Q) a) := ⋯.mpr this✝
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI : Invertible (Q a) := invertibleOfInvertibleι Q a

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
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑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✝
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI : Invertible (Q a) := invertibleOfInvertibleι Q a

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✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑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
this : Invertible ↑x := x.invertible
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ LinearMap.range (ι Q)

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

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
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
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ LinearMap.range (ι Q)

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

Result:
no goals