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

Tactic:
obtain ⟨z', hz'⟩ := hz m

Result:
case mul.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 * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case inv_mem
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)ˣ
hx : x ∈ Units.val ⁻¹' Set.range ⇑(ι Q)
m : M
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
obtain ⟨a, ha⟩ := hx

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

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

Proof state:
case mul
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
⊢ ↑(y * z) * (ι Q) m * ↑(y * z)⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
simp_rw [mul_inv_rev, Units.val_mul]

Result:
case mul
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
⊢ ↑y * ↑z * (ι Q) m * (↑z⁻¹ * ↑y⁻¹) ∈ LinearMap.range (ι Q)

Proof state:
case mul.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 * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
obtain ⟨y', hy'⟩ := hy z'

Result:
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)

Proof state:
case mul
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
⊢ ↑y * ↑z * (ι Q) m * (↑z⁻¹ * ↑y⁻¹) ∈ LinearMap.range (ι Q)

Tactic:
suffices ↑y * (↑z * ι Q m * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
  simpa only [mul_assoc] using this

Result:
case mul
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
⊢ ↑y * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ 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
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI := x.invertible

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

Proof state:
case mem
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)ˣ
hx : x ∈ Units.val ⁻¹' Set.range ⇑(ι Q)
m : M
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
obtain ⟨a, ha⟩ := hx

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