-- 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.mem_mul_mem.mem_mul.add
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) ⋯
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
y : CliffordAlgebra Q
hy : y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
ihx : motive (x * y✝ * b) ⋯
ihy : motive (y * y✝ * b) ⋯
⊢ motive (x * y✝ * b + y * y✝ * b) ⋯

Tactic:
apply add _ _ _ _ ihx ihy

Result:
no goals

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
⊢ ∀ (hx : xv ∈ LinearMap.range (ι Q) ^ (2 * k + n.val)), motive xv ⋯

Tactic:
simp_rw [pow_add, pow_mul]

Result:
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
⊢ ∀ (hx : xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ n.val), motive xv ⋯

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) ⋯
⊢ ∀ (hx : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)), motive (x * y * b) ⋯

Tactic:
intro hx2

Result:
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) ⋯

Proof state:
case intro.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 : CliffordAlgebra Q
ha : a ∈ (LinearMap.range (ι Q) ^ 2) ^ k
b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ n.val
⊢ 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

Result:
no goals