awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
hxv : xv ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k * (ι Q).range ^ n.val
mem_mul_mem :
  ∀ (a : CliffordAlgebra Q) (ha : a ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k) (b : CliffordAlgebra Q)
    (hb : b ∈ (ι Q).range ^ n.val), motive (a * b) ⋯
⊢ motive xv ⋯
have add₁ : ∀ (x : CliffordAlgebra Q) (y : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k * (ι Q).range ^ n.val) (hx : CliffordAlgebra Q)
  (hy : hx ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k * (ι Q).range ^ n.val) (ihx : motive x sorry) (ihy : motive hx sorry),
  motive (x + hx) sorry
Tactic: induction hxv using Submodule.mul_induction_on' with
  | mem_mul_mem a ha b hb =>
    induction ha using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      simp_rw [← Algebra.smul_def]
      exact range_ι_pow _ (Submodule.smul_mem _ _ hb)
    | add x y n hx hy ihx ihy =>
      simp_rw [add_mul]
      apply add _ _ _ _ ihx ihy
    | mem_mul x hx n'' y hy ihy =>
      revert hx
      simp_rw [pow_two]
      intro hx2
      induction hx2 using Submodule.mul_induction_on' with
      | mem_mul_mem m hm n hn =>
        simp_rw [LinearMap.mem_range] at hm hn
        obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
        simp_rw [mul_assoc _ y b]
        exact ι_mul_ι_mul _ _ _ _ ihy
      | add x hx y hy ihx ihy =>
        simp_rw [add_mul]
        apply add _ _ _ _ ihx ihy
  | add x y hx hy ihx ihy =>
    apply add _ _ _ _ ihx ihy
Cleared hypotheses: hxv
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
⊢ motive x hx
have refine : ∀ (rx : CliffordAlgebra Q) (h : rx ∈ (ι Q).range ^ ZMod.val (n := 2) 0), motive rx sorry
Tactic: refine evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
rx : CliffordAlgebra Q
h : rx ∈ (ι Q).range ^ ZMod.val (n := 2) 0
⊢ motive rx ⋯
have obtain : ∀ (r : R)
  (h :
    Membership.mem (α := CliffordAlgebra Q) ((ι Q).range ^ ZMod.val (n := 2) 0)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)),
  motive ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) sorry
Tactic: obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h
Cleared hypotheses: rx, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx →
      P
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
⊢ P x hx
have refine : ∀ (ιv : CliffordAlgebra Q) (h : ιv ∈ (CliffordAlgebra.ι Q).range ^ ZMod.val (n := 2) 1), P ιv sorry
Tactic: refine evenOdd_induction _ _ (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx →
      P
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
⊢ ∀ (h : ιv ∈ (CliffordAlgebra.ι Q).range ^ ZMod.val (n := 2) 1), P ιv ⋯
have simp_rw : ∀ (h : ιv ∈ (CliffordAlgebra.ι Q).range), P ιv sorry
Tactic: simp_rw [ZMod.val_one, pow_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw : HMul.hMul (β := CliffordAlgebra Q)
    (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
  1
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw₁ : HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
  1
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw₂ : HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
  1
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw₃ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
  1
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw₄ : Eq (α := CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((Q : (a : M) → R) m : R)) :
    CliffordAlgebra Q)
  (1 : CliffordAlgebra Q)
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
          ((Q : (a : M) → R) m : R)) :
      CliffordAlgebra Q)
    (1 : CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw₅ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) 1
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
          ((Q : (a : M) → R) m : R)) :
      CliffordAlgebra Q)
    (1 : CliffordAlgebra Q)
rw₅ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) 1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
have rw₆ : Eq (α := CliffordAlgebra Q) 1 1
Tactic: rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw : HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
    (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
  1
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw₁ : HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
  1
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw₂ : HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
  1
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]