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
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Set (CliffordAlgebra Q)ˣ)
    (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)) x
m : M
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have inv_mem : ∀ (a : M) (ha : (ι Q : (a : M) → CliffordAlgebra Q) a = (↑x : CliffordAlgebra Q)),
  HMul.hMul (β := CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
Tactic: obtain ⟨a, ha⟩ := 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_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m 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 : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have inv_mem : HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, 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
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m 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 : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
inv_mem :
  HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have inv_mem₁ : HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    (↑x : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, 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
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m 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 : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
inv_mem :
  HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₁ :
  HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have 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) m : CliffordAlgebra Q))
    ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, 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
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m 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 : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
inv_mem :
  HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
inv_mem₁ :
  HMul.hMul (β := CliffordAlgebra Q) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x : 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) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x⁻¹ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have 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 m : R) •
          a -
        m) :
    CliffordAlgebra Q)
Tactic: simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, 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
x : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
m : M
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have one : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    (↑1 : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: simp_rw [inv_one, Units.val_one, one_mul, mul_one, 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
x : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
m : M
one :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1 : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have one₁ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    1 ∈
  (ι Q).range
Tactic: simp_rw [inv_one, Units.val_one, one_mul, mul_one, 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
x : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
m : M
one :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1 : CliffordAlgebra Q) ∈
    (ι Q).range
one₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      1 ∈
    (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have one₂ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
    (1 : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: simp_rw [inv_one, Units.val_one, one_mul, mul_one, 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
x : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
m : M
one :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1 : CliffordAlgebra Q) ∈
    (ι Q).range
one₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      1 ∈
    (ι Q).range
one₂ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) (1 : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((↑1 : CliffordAlgebra Q) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑1⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have one₃ : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: simp_rw [inv_one, Units.val_one, one_mul, mul_one, 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
x : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
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 :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
hz :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
m : M
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑(y * z) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑(y * z)⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mul : HMul.hMul (β := CliffordAlgebra Q) ((↑y : CliffordAlgebra Q) * (↑z : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    ((↑z⁻¹ : CliffordAlgebra Q) * (↑y⁻¹ : CliffordAlgebra Q)) ∈
  (ι Q).range
Tactic: simp_rw [mul_inv_rev, Units.val_mul]
-- 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)ˣ
inst_3 : Invertible (α := R) 2
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 :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
hz :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
m : M
⊢ HMul.hMul (β := CliffordAlgebra Q) ((↑y : CliffordAlgebra Q) * (↑z : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      ((↑z⁻¹ : CliffordAlgebra Q) * (↑y⁻¹ : CliffordAlgebra Q)) ∈
    (ι Q).range
have mul : (↑y : CliffordAlgebra Q) *
      (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q)) *
    (↑y⁻¹ : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: suffices ↑y * (↑z * ι Q m * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
      simpa only [mul_assoc] using 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)ˣ
inst_3 : Invertible (α := R) 2
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 :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
hz :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
m : M
⊢ (↑y : CliffordAlgebra Q) *
        (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
          (↑z⁻¹ : CliffordAlgebra Q)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mul : ∀ (z' : M)
  (hz' :
    (ι Q : (a : M) → CliffordAlgebra Q) z' =
      HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q)),
  (↑y : CliffordAlgebra Q) *
        (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
          (↑z⁻¹ : CliffordAlgebra Q)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
Tactic: obtain ⟨z', hz'⟩ := hz m
-- 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)ˣ
inst_3 : Invertible (α := R) 2
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 :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
hz :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
m z' : M
hz' :
  (ι Q : (a : M) → CliffordAlgebra Q) z' =
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑z⁻¹ : CliffordAlgebra Q)
⊢ (↑y : CliffordAlgebra Q) *
        (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
          (↑z⁻¹ : CliffordAlgebra Q)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mul : ∀ (y' : M)
  (hy' :
    (ι Q : (a : M) → CliffordAlgebra Q) y' =
      HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q)),
  (↑y : CliffordAlgebra Q) *
        (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
          (↑z⁻¹ : CliffordAlgebra Q)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
Tactic: obtain ⟨y', hy'⟩ := hy z'
-- 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)ˣ
inst_3 : Invertible (α := R) 2
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 :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
hz :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
m z' : M
hz' :
  (ι Q : (a : M) → CliffordAlgebra Q) z' =
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑z⁻¹ : CliffordAlgebra Q)
y' : M
hy' :
  (ι Q : (a : M) → CliffordAlgebra Q) y' =
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
      (↑y⁻¹ : CliffordAlgebra Q)
⊢ (↑y : CliffordAlgebra Q) *
        (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
          (↑z⁻¹ : CliffordAlgebra Q)) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mul : HMul.hMul (β := CliffordAlgebra Q) (↑y : 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
x : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
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 :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑y⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
hz :
  ∀ (m : M),
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
        (↑z⁻¹ : CliffordAlgebra Q) ∈
      (ι Q).range
m z' : M
hz' :
  (ι Q : (a : M) → CliffordAlgebra Q) z' =
    HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑z⁻¹ : CliffordAlgebra Q)
y' : M
hy' :
  (ι Q : (a : M) → CliffordAlgebra Q) y' =
    HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
      (↑y⁻¹ : CliffordAlgebra Q)
mul :
  HMul.hMul (β := CliffordAlgebra Q) (↑y : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) z' : CliffordAlgebra Q) *
      (↑y⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ (↑y : CliffordAlgebra Q) *
        (HMul.hMul (β := CliffordAlgebra Q) (↑z : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : 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]