awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n_1 → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n_1.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1) (hy : y ∈ evenOdd Q n_1),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1),
    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_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n_1
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n_1.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
n : CliffordAlgebra Q
hn_1 : n ∈ (ι Q).range
hn : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = n
m₁ : M
hm : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
mem_mul_mem :
  ∀ (m₂ : M)
    (hn :
      Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)),
    motive
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          y *
        b)
      ⋯
⊢ motive (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q) n * y * b) ⋯

Tactic:
obtain ⟨m₂, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
m₂ : M
hn : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
mem_mul_mem :
  motive
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      (y * b))
    ⋯
⊢ motive
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        y *
      b)
    ⋯

Tactic:
simp_rw [mul_assoc _ y b]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
m₂ : M
hn : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
⊢ motive
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      (y * b))
    ⋯

Tactic:
ι_mul_ι_mul _ _ _ _ ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
m₂ : M
hn : Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
⊢ motive
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
      (y * b))
    ⋯

Tactic:
exact ι_mul_ι_mul _ _ _ _ ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x_2 : CliffordAlgebra Q
n'' : ℕ
y_1 : CliffordAlgebra Q
hy_1 : y_1 ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy_1 : motive (y_1 * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y_1 * b) ⋯
ihy : motive (y * y_1 * b) ⋯
mem_mul_mem : motive (x * y_1 * b + y * y_1 * b) ⋯
⊢ motive ((x + y) * y_1 * b) ⋯

Tactic:
simp_rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x_2 : CliffordAlgebra Q
n'' : ℕ
y_1 : CliffordAlgebra Q
hy_1 : y_1 ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy_1 : motive (y_1 * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y_1 * b) ⋯
ihy : motive (y * y_1 * b) ⋯
⊢ motive (x * y_1 * b + y * y_1 * b) ⋯

Tactic:
apply add _ _ _ _ ihx ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
hx2 : x ∈ (ι Q).range * (ι Q).range
mem_mul_mem :
  ∀ (m : CliffordAlgebra Q) (hm : m ∈ (ι Q).range) (n_1 : CliffordAlgebra Q) (hn : n_1 ∈ (ι Q).range),
    motive (m * n_1 * y * b) ⋯
mem_mul_mem₁ :
  ∀ (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range * (ι Q).range) (y_1 : CliffordAlgebra Q)
    (hy_1 : y_1 ∈ (ι Q).range * (ι Q).range) (ihx : motive (x * y * b) ⋯) (ihy : motive (y_1 * y * b) ⋯),
    motive ((x + y_1) * y * b) ⋯
⊢ motive (x * y * b) ⋯

Tactic:
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

Premises used: add_mul, mul_assoc, LinearMap.mem_range, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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 a : CliffordAlgebra Q
ha : a ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k
b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
mem_mul_mem :
  ∀ (r : R),
    motive
      (HMul.hMul (α := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b)
      ⋯
mem_mul_mem₁ :
  ∀ (x y : CliffordAlgebra Q) (n_1 : ℕ) (hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n_1)
    (hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n_1) (ihx : motive (x * b) ⋯) (ihy : motive (y * b) ⋯),
    motive ((x + y) * b) ⋯
mem_mul_mem₂ :
  ∀ (x : CliffordAlgebra Q) (hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2) (n'' : ℕ) (y : CliffordAlgebra Q)
    (hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n'') (ihy : motive (y * b) ⋯), motive (x * y * b) ⋯
⊢ motive (a * b) ⋯

Tactic:
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

Premises used: add_mul, pow_two, Algebra.algebraMap, LinearMap.mem_range, Algebra.smul_def, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n
k : ℕ
xv 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 ⋯
ihy : motive hx ⋯
⊢ motive (x + hx) ⋯

Tactic:
apply add _ _ _ _ ihx ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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) ⋯
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 ⋯)
    (ihy : motive hx ⋯), motive (x + hx) ⋯
⊢ motive xv ⋯

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

Premises used: add_mul, pow_two, Algebra.algebraMap, LinearMap.mem_range, Algebra.smul_def, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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

Tactic:
evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx

Premises used: CliffordAlgebra.evenOdd_induction
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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
refine : ∀ (rx : CliffordAlgebra Q) (h : rx ∈ (ι Q).range ^ ZMod.val (n := 2) 0), motive rx ⋯
⊢ motive x hx

Tactic:
refine evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx

Premises used: CliffordAlgebra.evenOdd_induction
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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
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) ⋯
⊢ motive rx ⋯

Tactic:
obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h

Premises used: Submodule.mem_one, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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
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) ⋯

Tactic:
algebraMap r
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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
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) ⋯

Tactic:
exact algebraMap r
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
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

Tactic:
evenOdd_induction _ _ (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx

Premises used: CliffordAlgebra.evenOdd_induction