-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem even_induction {motive : ∀ x, x ∈ evenOdd Q 0 → Prop}
    (algebraMap : ∀ r : R, motive (algebraMap _ _ r) (SetLike.algebraMap_mem_graded _ _))
    (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 (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
    (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : motive x hx

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((_root_.algebraMap 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
rx : CliffordAlgebra Q
h : rx ∈ LinearMap.range (ι Q) ^ ZMod.val 0
⊢ motive rx ⋯

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

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
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((_root_.algebraMap 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
r : R
h : (_root_.algebraMap R (CliffordAlgebra Q)) r ∈ LinearMap.range (ι Q) ^ ZMod.val 0
⊢ motive ((_root_.algebraMap R (CliffordAlgebra Q)) r) ⋯

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
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((_root_.algebraMap 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
r : R
h : (_root_.algebraMap R (CliffordAlgebra Q)) r ∈ LinearMap.range (ι Q) ^ ZMod.val 0
⊢ motive ((_root_.algebraMap R (CliffordAlgebra Q)) r) ⋯

Tactic:
exact algebraMap r

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
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((_root_.algebraMap 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
⊢ motive x hx

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

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((_root_.algebraMap 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 ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
rx : CliffordAlgebra Q
h : rx ∈ LinearMap.range (ι Q) ^ ZMod.val 0
⊢ motive rx ⋯