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_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
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) ⋯
have mem_mul_mem : ∀ (hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2), motive (x * y * b) sorry
Tactic: revert hx
Cleared hypotheses: 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
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) ⋯
⊢ ∀ (hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2), motive (x * y * b) ⋯
have mem_mul_mem : ∀ (hx : x ∈ (ι Q).range * (ι Q).range), motive (x * y * b) sorry
Tactic: simp_rw [pow_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (hypothesis)
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) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
⊢ motive (m * n * y * b) ⋯
have hm₁ : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = m
Tactic: simp_rw [LinearMap.mem_range] at hm hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (hypothesis)
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) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
hm₁ : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = m
⊢ motive (m * n * y * b) ⋯
have hn₁ : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = n
Tactic: simp_rw [LinearMap.mem_range] at hm hn
-- 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_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) ⋯
m : CliffordAlgebra Q
hm_1 : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn_1 : n ∈ (ι Q).range
hm : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = m
hn : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = n
⊢ motive (m * n * y * b) ⋯
have mem_mul_mem : ∀ (m₁ : M)
  (hm :
    Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)),
  motive (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q) n * y * b) sorry
Tactic: obtain ⟨m₁, rfl⟩ := hm
Cleared hypotheses: m, hm_1, hm
-- 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_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)
⊢ motive (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q) n * y * b) ⋯
have 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)
    sorry
Tactic: obtain ⟨m₂, rfl⟩ := hn
Cleared hypotheses: n, hn_1, hn
-- 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_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)
    ⋯
have 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))
  sorry
Tactic: simp_rw [mul_assoc _ y b]
-- 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_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) * y_1 * b) ⋯
have mem_mul_mem : motive (x * y_1 * b + y * y_1 * b) sorry
Tactic: simp_rw [add_mul]
-- 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_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
⊢ motive (x * y * b) ⋯
have 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) sorry
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
Cleared hypotheses: hx2
-- 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_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) ⋯
⊢ motive (x * y * b) ⋯
have 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) sorry) (ihy : motive (y_1 * y * b) sorry),
  motive ((x + y_1) * y * b) sorry
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
Cleared hypotheses: hx2
-- 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 a : CliffordAlgebra Q
ha : a ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k
b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
⊢ motive (a * b) ⋯
have mem_mul_mem : ∀ (r : R),
  motive
    (HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b)
    sorry
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
Cleared hypotheses: ha
-- 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 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)
      ⋯
⊢ motive (a * b) ⋯
have 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) sorry) (ihy : motive (y * b) sorry),
  motive ((x + y) * b) sorry
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
Cleared hypotheses: ha
-- 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 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) ⋯
⊢ motive (a * b) ⋯
have 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) sorry), motive (x * y * b) sorry
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
Cleared hypotheses: ha
-- 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
⊢ motive xv ⋯
have 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) 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