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

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

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

Tactic:
rwa [ha]

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
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:
simp_rw [← invOf_units x, ← ha, involute_ι, neg_mul, ι_mul_ι_mul_invOf_ι Q a b, ← map_neg,
  LinearMap.mem_range_self]

Result:
no goals

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:
suffices involute (Q := Q) ↑y * (involute (Q := Q) ↑z * ι Q b * ↑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
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✝
⊢ involute ↑x⁻¹ * (ι Q) b * ↑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
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)

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
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✝
⊢ involute ↑x * (ι Q) b * ↑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
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)

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 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
this : involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.60780
⊢ involute ↑y * involute ↑z * (ι Q) b * (↑z⁻¹ * ↑y⁻¹) ∈ LinearMap.range (ι Q)

Tactic:
simpa only [mul_assoc] using this

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

Tactic:
induction hx using Subgroup.closure_induction'' generalizing b 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, involute_ι, neg_mul, ι_mul_ι_mul_invOf_ι Q a b, ← map_neg,
    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, map_invOf, involute_ι, invOf_neg, neg_mul,
    invOf_ι_mul_ι_mul_ι, ← map_neg, LinearMap.mem_range_self]
| one => simp_rw [inv_one, Units.val_one, map_one, one_mul, mul_one, LinearMap.mem_range_self]
| mul y z _ _ hy hz =>
  simp_rw [mul_inv_rev, Units.val_mul, map_mul]
  suffices involute (Q := Q) ↑y * (involute (Q := Q) ↑z * ι Q b * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
    simpa only [mul_assoc] using this
  obtain ⟨z', hz'⟩ := hz b
  obtain ⟨y', hy'⟩ := hy z'
  simp_rw [← hz', ← hy', LinearMap.mem_range_self]

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

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

Result:
no goals