-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem involute_act_ι_mem_range_ι [Invertible (2 : R)]
    {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q) (b : M) :
      involute (Q := Q) ↑x * ι Q b * ↑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
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ LinearMap.range (ι Q)
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ LinearMap.range (ι Q)
b : M
⊢ involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ LinearMap.range (ι Q)

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

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

Tactic:
simp_rw [mul_inv_rev, Units.val_mul, map_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
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ LinearMap.range (ι Q)
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ LinearMap.range (ι Q)
b : M
⊢ involute ↑y * involute ↑z * (ι Q) b * (↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b 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)
⊢ involute ↑x⁻¹ * (ι Q) b * ↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b 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)
⊢ involute ↑x⁻¹ * (ι Q) b * ↑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
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
b : M
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ 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
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
b : M
⊢ involute ↑x * (ι Q) b * ↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ involute ↑x⁻¹ * (ι Q) b * ↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b 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)
⊢ involute ↑x⁻¹ * (ι Q) b * ↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
hx : x ∈ Units.val ⁻¹' Set.range ⇑(ι Q)
b : M
⊢ involute ↑x * (ι Q) b * ↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ 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
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ LinearMap.range (ι Q)
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ LinearMap.range (ι Q)
b z' : M
hz' : (ι Q) z' = involute ↑z * (ι Q) b * ↑z⁻¹
⊢ involute ↑y * (involute ↑z * (ι Q) b * ↑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
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ LinearMap.range (ι Q)
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ LinearMap.range (ι Q)
b z' : M
hz' : (ι Q) z' = involute ↑z * (ι Q) b * ↑z⁻¹
y' : M
hy' : (ι Q) y' = involute ↑y * (ι Q) z' * ↑y⁻¹
⊢ involute ↑y * (involute ↑z * (ι Q) b * ↑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
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b 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)
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
simp_rw [← invOf_units x, inv_inv, ← ha, map_invOf, involute_ι, invOf_neg, neg_mul,
  invOf_ι_mul_ι_mul_ι, ← map_neg, LinearMap.mem_range_self]

Result:
no goals