-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem coe_toEven_reverse_involute (x : CliffordAlgebra Q) :
    ↑(toEven Q (reverse (involute x))) =
      reverse (Q := Q' Q) (toEven Q x : CliffordAlgebra (Q' Q))

Proof state:
case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
⊢ ↑((toEven Q) (reverse (involute ((algebraMap R (CliffordAlgebra Q)) r)))) =
    reverse ↑((toEven Q) ((algebraMap R (CliffordAlgebra Q)) r))

Tactic:
simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]

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
x : CliffordAlgebra Q
⊢ ↑((toEven Q) (reverse (involute x))) = reverse ↑((toEven Q) x)

Tactic:
induction x using CliffordAlgebra.induction with
| algebraMap r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
| ι m =>
  letI : SubtractionMonoid (even (Q' Q)) := AddGroup.toSubtractionMonoid
  simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
    reverse_ι, neg_e0_mul_v, map_neg]
| mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
| add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]

Result:
no goals

Proof state:
case mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
hx : ↑((toEven Q) (reverse (involute x))) = reverse ↑((toEven Q) x)
hy : ↑((toEven Q) (reverse (involute y))) = reverse ↑((toEven Q) y)
⊢ ↑((toEven Q) (reverse (involute (x * y)))) = reverse ↑((toEven Q) (x * y))

Tactic:
simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]

Result:
no goals

Proof state:
case ι
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
this : SubtractionMonoid ↥(even (Q' Q)) := AddGroup.toSubtractionMonoid
⊢ ↑((toEven Q) (reverse (involute ((ι Q) m)))) = reverse ↑((toEven Q) ((ι Q) m))

Tactic:
simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
  reverse_ι, neg_e0_mul_v, map_neg]

Result:
no goals

Proof state:
case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
hx : ↑((toEven Q) (reverse (involute x))) = reverse ↑((toEven Q) x)
hy : ↑((toEven Q) (reverse (involute y))) = reverse ↑((toEven Q) y)
⊢ ↑((toEven Q) (reverse (involute (x + y)))) = reverse ↑((toEven Q) (x + y))

Tactic:
simp only [map_add, Subalgebra.coe_add, hx, hy]

Result:
no goals

Proof state:
case ι
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑((toEven Q) (reverse (involute ((ι Q) m)))) = reverse ↑((toEven Q) ((ι Q) m))

Tactic:
letI : SubtractionMonoid (even (Q' Q)) := AddGroup.toSubtractionMonoid

Result:
case ι
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
this : SubtractionMonoid ↥(even (Q' Q)) := AddGroup.toSubtractionMonoid
⊢ ↑((toEven Q) (reverse (involute ((ι Q) m)))) = reverse ↑((toEven Q) ((ι Q) m))