-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem evenOdd_induction (n : ZMod 2) {motive : ∀ x, x ∈ evenOdd Q n → Prop}
    (range_ι_pow : ∀ (v) (h : v ∈ LinearMap.range (ι Q) ^ n.val),
        motive v (Submodule.mem_iSup_of_mem ⟨n.val, n.natCast_zmod_val⟩ h))
    (add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (Submodule.add_mem _ hx hy))
    (ι_mul_ι_mul :
      ∀ m₁ m₂ x hx,
        motive x hx →
          motive (ι Q m₁ * ι Q m₂ * x)
            (zero_add n ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
    (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) : motive x hx

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : 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 ∈ LinearMap.range (ι Q) ^ 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
hxv : xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ n.val
⊢ 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

Result:
no goals

Proof state:
case intro.mem_mul_mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : 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 ∈ LinearMap.range (ι Q) ^ 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : motive (y * b) ⋯
hx2 : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
⊢ 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

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : 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 ∈ LinearMap.range (ι Q) ^ 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ ↑⟨val, property⟩),
    motive x ⋯

Tactic:
simp_rw [ZMod.natCast_eq_iff, add_comm n.val]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : 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 ∈ LinearMap.range (ι Q) ^ 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ∃ k, val = 2 * k + n.val) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
    motive x ⋯

Proof state:
case intro.mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : 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 ∈ LinearMap.range (ι Q) ^ 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
n : CliffordAlgebra Q
hn : n ∈ LinearMap.range (ι Q)
⊢ motive (m * n * y * b) ⋯

Tactic:
simp_rw [LinearMap.mem_range] at hm hn

Result:
case intro.mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : 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 ∈ LinearMap.range (ι Q) ^ 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm✝ : m ∈ LinearMap.range (ι Q)
n : CliffordAlgebra Q
hn✝ : n ∈ LinearMap.range (ι Q)
hm : ∃ y, (ι Q) y = m
hn : ∃ y, (ι Q) y = n
⊢ motive (m * n * y * b) ⋯