awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)ˣ
b : M
one :
  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
one₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 1 : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      1 ∈
    (ι Q).range
one₂ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      1 ∈
    (ι Q).range
one₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) (1 : CliffordAlgebra Q) ∈
    (ι Q).range
one₄ : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
⊢ 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

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

Premises used: inv_one, LinearMap.mem_range_self, map_one, Units.val_one, mul_one, one_mul
-- 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 y z : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y
hy_1 :
  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
mul :
  HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : 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) * (↑y⁻¹ : CliffordAlgebra Q)) ∈
    (ι Q).range
⊢ 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

Tactic:
simp_rw [mul_inv_rev, Units.val_mul, map_mul]

Premises used: map_mul, mul_inv_rev, Units.val_mul
-- 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 y z : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y
hy_1 :
  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
this :
  HMul.hMul (α := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        (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)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : 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) * (↑y⁻¹ : CliffordAlgebra Q)) ∈
    (ι Q).range

Tactic:
simpa only [mul_assoc] using this

Premises used: mul_assoc
-- 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 y z : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y
hy_1 :
  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
mul :
  HMul.hMul (α := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        (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)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : 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) * (↑y⁻¹ : CliffordAlgebra Q)) ∈
    (ι Q).range

Tactic:
suffices involute (Q := Q) ↑y * (involute (Q := Q) ↑z * ι Q b * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
      simpa only [mul_assoc] using this
-- 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 y z : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y
hy_1 :
  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
mul :
  ∀ (z' : M)
    (hz' :
      (ι Q : (a : M) → CliffordAlgebra Q) z' =
        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)),
    HMul.hMul (α := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
          (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)) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        (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)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range

Tactic:
obtain ⟨z', hz'⟩ := hz b
-- 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 y z : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y
hy_1 :
  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 z' : M
hz' :
  (ι Q : (a : M) → CliffordAlgebra Q) z' =
    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)
mul :
  ∀ (y' : M)
    (hy' :
      (ι Q : (a : M) → CliffordAlgebra Q) y' =
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
          (↑y⁻¹ : CliffordAlgebra Q)),
    HMul.hMul (α := CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
          (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)) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        (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)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range

Tactic:
obtain ⟨y', hy'⟩ := hy z'
-- 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 y z : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y
hy_1 :
  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 z' : M
hz' :
  (ι Q : (a : M) → CliffordAlgebra Q) z' =
    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)
y' : M
hy' :
  (ι Q : (a : M) → CliffordAlgebra Q) y' =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
      (↑y⁻¹ : CliffordAlgebra Q)
mul :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
mul₁ : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) y' : CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (↑y : CliffordAlgebra Q) : CliffordAlgebra Q)
        (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)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range

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

Premises used: LinearMap.mem_range_self
-- 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
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
a :
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range ≤
    (ι Q).range
a₁ :
  (ι Q).range ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range =
    (ι Q).range

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range ≤
    (ι Q).range

Tactic:
this _ hx
-- 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
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range ≤
    (ι Q).range

Tactic:
exact this _ hx
-- 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
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x⁻¹ :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range) ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range

Tactic:
have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)
-- 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
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this_1 :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
this :
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x⁻¹ :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range) ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range
⊢ (ι Q).range ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range

Tactic:
Eq.trans_le ?_ this

Premises used: Eq.trans_le
-- 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
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
this_1 :
  ∀ x ∈ lipschitzGroup Q,
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range ≤
      (ι Q).range
this :
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x⁻¹ :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range) ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range
a :
  (ι Q).range =
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
        ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x⁻¹ :
          ConjAct (CliffordAlgebra Q)ˣ)
        (ι Q).range)
⊢ (ι Q).range ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range

Tactic:
refine Eq.trans_le ?_ this

Premises used: Eq.trans_le