-- 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_1 x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q : (a : M) → CliffordAlgebra Q) a = (↑x : CliffordAlgebra Q)
this_1 : Invertible (↑x : CliffordAlgebra Q) := x.invertible
this_2 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) :=
  Eq.mpr ⋯ this_1
this_3 : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
this_4 : Invertible (α := CliffordAlgebra Q) (-(ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) :=
  invertibleNeg ((ι Q : (a : M) → CliffordAlgebra Q) a)
this : Invertible (α := CliffordAlgebra Q)
  ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a) :
    CliffordAlgebra Q) :=
  Invertible.map involute ((ι Q : (a : M) → CliffordAlgebra Q) a)
inv_mem :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      (↑x : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₂ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₃ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ MulOne.toMul MulOne.toOne
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a)) _ :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₄ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ MulOne.toMul MulOne.toOne (-(ι Q : (a : M) → CliffordAlgebra Q) a) _ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₅ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (-@Invertible.invOf _ MulOne.toMul MulOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₆ :
  -HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₇ :
  Membership.mem (α := CliffordAlgebra Q) (ι Q).range
    (-(ι Q : (a : M) → CliffordAlgebra Q)
          (HMul.hMul (α := R) (β := R)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
                (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
              a -
            b) :
      CliffordAlgebra Q)
inv_mem₈ :
  Membership.mem (α := CliffordAlgebra Q) (ι Q).range
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (-(HMul.hMul (α := R) (β := R)
                (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
                (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
              a -
            b)) :
      CliffordAlgebra Q)
⊢ 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:
simp_rw [← invOf_units x, inv_inv, ← ha, map_invOf, involute_ι, invOf_neg, neg_mul,
      invOf_ι_mul_ι_mul_ι, ← map_neg, LinearMap.mem_range_self]

Premises used: CliffordAlgebra.invOf_ι_mul_ι_mul_ι, map_neg, LinearMap.mem_range_self, invOf_neg, CliffordAlgebra.involute_ι, inv_inv, neg_mul, invOf_units, map_invOf