awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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)
⊢ 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
have 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
Tactic: simp_rw [← hz', ← hy', LinearMap.mem_range_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
⊢ 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
have mul₁ : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) y' : CliffordAlgebra Q)
Tactic: simp_rw [← hz', ← hy', LinearMap.mem_range_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
⊢ 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
have 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
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]
Cleared hypotheses: hx, b
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
⊢ 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
have 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
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]
Cleared hypotheses: hx, b
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
have a : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range =
    (ι Q).range
have a₁ : (ι Q).range ≤
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
    ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
    (ι Q).range
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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
⊢ (ι Q).range ≤
    HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range
have 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
Tactic: have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
have 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)
Tactic: refine Eq.trans_le ?_ this
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range =
    (ι Q).range
have suffices : ∀ x ∈ lipschitzGroup Q,
  HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range ≤
    (ι Q).range
Tactic: suffices ∀ x ∈ lipschitzGroup Q,
      ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) by
    apply le_antisymm
    · exact this _ hx
    · have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)
      refine Eq.trans_le ?_ this
      simp only [map_inv, smul_inv_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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_1 : (CliffordAlgebra Q)ˣ
hx_1 : x_1 ∈ lipschitzGroup Q
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      (ι Q).range ≤
    (ι Q).range
have rw : (ι Q).range ≤
  Submodule.comap
    (DistribSMul.toLinearMap R (S := ConjAct (CliffordAlgebra Q)ˣ) (CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x :
        ConjAct (CliffordAlgebra Q)ˣ))
    (ι Q).range
Tactic: rw [Submodule.pointwise_smul_def, Submodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, (↑x_1 : CliffordAlgebra Q) = (↑x : CliffordAlgebra Q)) ↔ x ∈ lipschitzGroup Q
have norm_cast : (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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)ˣ
⊢ (↑x : CliffordAlgebra Q) ∈ pinGroup Q ↔
    x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
have rw : Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      (↑x : CliffordAlgebra Q) ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q) ↔
  x ∈ lipschitzGroup Q ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
Tactic: rw [mem_iff, lipschitzGroup.coe_mem_iff_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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)ˣ
rw :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
        (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
          (lipschitzGroup Q).toSubmonoid)
        (↑x : CliffordAlgebra Q) ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q) ↔
    x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
⊢ (↑x : CliffordAlgebra Q) ∈ pinGroup Q ↔
    x ∈ lipschitzGroup Q ∧
      Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
have rw₁ : x ∈ lipschitzGroup Q ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q) ↔
  x ∈ lipschitzGroup Q ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (↑x : CliffordAlgebra Q)
Tactic: rw [mem_iff, lipschitzGroup.coe_mem_iff_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (hypothesis)
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 ∈ pinGroup Q
⊢ star x ∈ pinGroup Q
have hx₁ : Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    x ∧
  Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x
Tactic: rw [mem_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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 :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      x ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      (star x) ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) (star x)
have refine : Membership.mem (γ := Submonoid (CliffordAlgebra Q))
  (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
    (lipschitzGroup Q).toSubmonoid)
  (star x)
Tactic: refine ⟨?_, Unitary.star_mem hx.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
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 :
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
      (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
        (lipschitzGroup Q).toSubmonoid)
      x ∧
    Membership.mem (γ := Submonoid (CliffordAlgebra Q)) (unitary (CliffordAlgebra Q)) x
⊢ Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    (star x)
have rcases : ∀ (y : (CliffordAlgebra Q)ˣ) (hy₁ : y ∈ (↑(lipschitzGroup Q).toSubmonoid : Set (CliffordAlgebra Q)ˣ))
  (hy₂ : (Units.coeHom (CliffordAlgebra Q) : (a : (CliffordAlgebra Q)ˣ) → CliffordAlgebra Q) y = x)
  (_hx₂ : star x * x = 1) (hx₃ : x * star x = 1),
  Membership.mem (γ := Submonoid (CliffordAlgebra Q))
    (Submonoid.map (F := (CliffordAlgebra Q)ˣ →* CliffordAlgebra Q) (Units.coeHom (CliffordAlgebra Q))
      (lipschitzGroup Q).toSubmonoid)
    (star x)
Tactic: rcases hx with ⟨⟨y, hy₁, hy₂⟩, _hx₂, hx₃⟩
Cleared hypotheses: hx