-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
b : M
mem :
  ∀ (x : (CliffordAlgebra Q)ˣ)
    (hx :
      Membership.mem (γ := Set (CliffordAlgebra Q)ˣ)
        (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)) x)
    (b : M),
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑x : CliffordAlgebra Q) : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        (↑x⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
inv_mem :
  ∀ (x : (CliffordAlgebra Q)ˣ)
    (hx :
      Membership.mem (γ := Set (CliffordAlgebra Q)ˣ)
        (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)) x)
    (b : M),
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q) : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
one :
  ∀ (b : M),
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        (↑1⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
mul :
  ∀ (y z : (CliffordAlgebra Q)ˣ),
    Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
        (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y →
      Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
          (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) z →
        ∀
          (hy :
            ∀ (b : M),
              HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
                    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) :
                      CliffordAlgebra Q)
                    ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
                  (↑y⁻¹ : CliffordAlgebra Q) ∈
                (ι Q).range)
          (hz :
            ∀ (b : M),
              HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
                    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑z : CliffordAlgebra Q) :
                      CliffordAlgebra Q)
                    ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
                  (↑z⁻¹ : CliffordAlgebra Q) ∈
                (ι Q).range)
          (b : M),
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
                ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑(y * z) : CliffordAlgebra Q) :
                  CliffordAlgebra Q)
                ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
              (↑(y * z)⁻¹ : CliffordAlgebra Q) ∈
            (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑x : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range

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]

Premises used: inv_one, CliffordAlgebra.invOf_ι_mul_ι_mul_ι, map_neg, LinearMap.mem_range_self, InvMemClass.inv_mem, map_mul, invOf_neg, CliffordAlgebra.involute_ι, map_one, inv_inv, Units.val_one, neg_mul, mul_inv_rev, mul_one, invOf_units, map_invOf, Units.val_mul, one_mul