[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂') =
    reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
[PROOFSTEP]
ext
[GOAL]
case h.a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
x✝¹ : Matrix m n A
i✝ : m''
x✝ : n''
⊢ ↑(LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂')) x✝¹ i✝ x✝ =
    ↑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) x✝¹ i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ↑(reindexLinearEquiv R A e₁' e₂') ∘ ↑(reindexLinearEquiv R A e₁ e₂) =
    ↑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
[PROOFSTEP]
rw [← reindexLinearEquiv_trans]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ↑(reindexLinearEquiv R A e₁' e₂') ∘ ↑(reindexLinearEquiv R A e₁ e₂) =
    ↑(LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂'))
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝⁴ : CommSemiring R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
e : m ≃ n
src✝ : Matrix m m R ≃ₗ[R] Matrix n n R := reindexLinearEquiv R R e e
r : R
⊢ toFun
      { toFun := ↑(reindex e e), invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R (Matrix m m R)) r) =
    ↑(algebraMap R (Matrix n n R)) r
[PROOFSTEP]
simp [algebraMap, Algebra.toRingHom, submatrix_smul _ 1]


[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(-ι Q) m * ↑(-ι Q) m = ↑(algebraMap R (CliffordAlgebra Q)) (↑Q m)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ AlgHom.comp involute involute = AlgHom.id R (CliffordAlgebra Q)
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp involute involute)) (ι Q)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q))) (ι Q)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ unop (↑(LinearMap.comp (↑(opLinearEquiv R)) (ι Q)) m * ↑(LinearMap.comp (↑(opLinearEquiv R)) (ι Q)) m) =
    unop (↑(algebraMap R (CliffordAlgebra Q)ᵐᵒᵖ) (↑Q m))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑reverse (↑(ι Q) m) = ↑(ι Q) m
[PROOFSTEP]
simp [reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
⊢ ↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r) = ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
simp [reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ↑reverse 1 = 1
[PROOFSTEP]
convert reverse.commutes (Q := Q) (1 : R)
[GOAL]
case h.e'_2.h.e'_6
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 = ↑(algebraMap R (CliffordAlgebra Q)) 1
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 = ↑(algebraMap R (CliffordAlgebra Q)) 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
⊢ ↑reverse (a * b) = ↑reverse b * ↑reverse a
[PROOFSTEP]
simp [reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.comp reverse reverse = LinearMap.id
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : CliffordAlgebra Q
⊢ ↑(LinearMap.comp reverse reverse) m = ↑LinearMap.id m
[PROOFSTEP]
simp only [LinearMap.id_apply, LinearMap.comp_apply]
[GOAL]
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : CliffordAlgebra Q
⊢ ↑reverse (↑reverse m) = m
[PROOFSTEP]
induction m using CliffordAlgebra.induction
[GOAL]
case h.h_grade0
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ ↑reverse (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r✝)) = ↑(algebraMap R (CliffordAlgebra Q)) r✝
case h.h_grade1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑reverse (↑(ι Q) x✝)) = ↑(ι Q) x✝
case h.h_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² * b✝)) = a✝² * b✝
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² + b✝)) = a✝² + b✝
[PROOFSTEP]
case h_grade0 => rw [reverse.commutes, reverse.commutes]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ ↑reverse (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r✝)) = ↑(algebraMap R (CliffordAlgebra Q)) r✝
[PROOFSTEP]
case h_grade0 => rw [reverse.commutes, reverse.commutes]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ ↑reverse (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r✝)) = ↑(algebraMap R (CliffordAlgebra Q)) r✝
[PROOFSTEP]
rw [reverse.commutes, reverse.commutes]
[GOAL]
case h.h_grade1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑reverse (↑(ι Q) x✝)) = ↑(ι Q) x✝
case h.h_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² * b✝)) = a✝² * b✝
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² + b✝)) = a✝² + b✝
[PROOFSTEP]
case h_grade1 => rw [reverse_ι, reverse_ι]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑reverse (↑(ι Q) x✝)) = ↑(ι Q) x✝
[PROOFSTEP]
case h_grade1 => rw [reverse_ι, reverse_ι]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑reverse (↑(ι Q) x✝)) = ↑(ι Q) x✝
[PROOFSTEP]
rw [reverse_ι, reverse_ι]
[GOAL]
case h.h_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² * b✝)) = a✝² * b✝
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² + b✝)) = a✝² + b✝
[PROOFSTEP]
case h_mul a b ha hb => rw [reverse.map_mul, reverse.map_mul, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑reverse a) = a
hb : ↑reverse (↑reverse b) = b
⊢ ↑reverse (↑reverse (a * b)) = a * b
[PROOFSTEP]
case h_mul a b ha hb => rw [reverse.map_mul, reverse.map_mul, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑reverse a) = a
hb : ↑reverse (↑reverse b) = b
⊢ ↑reverse (↑reverse (a * b)) = a * b
[PROOFSTEP]
rw [reverse.map_mul, reverse.map_mul, ha, hb]
[GOAL]
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑reverse a✝²) = a✝²
a✝ : ↑reverse (↑reverse b✝) = b✝
⊢ ↑reverse (↑reverse (a✝² + b✝)) = a✝² + b✝
[PROOFSTEP]
case h_add a b ha hb => rw [reverse.map_add, reverse.map_add, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑reverse a) = a
hb : ↑reverse (↑reverse b) = b
⊢ ↑reverse (↑reverse (a + b)) = a + b
[PROOFSTEP]
case h_add a b ha hb => rw [reverse.map_add, reverse.map_add, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑reverse a) = a
hb : ↑reverse (↑reverse b) = b
⊢ ↑reverse (↑reverse (a + b)) = a + b
[PROOFSTEP]
rw [reverse.map_add, reverse.map_add, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.comp reverse (AlgHom.toLinearMap involute) = LinearMap.comp (AlgHom.toLinearMap involute) reverse
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ ↑(LinearMap.comp reverse (AlgHom.toLinearMap involute)) x = ↑(LinearMap.comp (AlgHom.toLinearMap involute) reverse) x
[PROOFSTEP]
simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply]
[GOAL]
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ ↑reverse (↑involute x) = ↑involute (↑reverse x)
[PROOFSTEP]
induction x using CliffordAlgebra.induction
[GOAL]
case h.h_grade0
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ ↑reverse (↑involute (↑(algebraMap R (CliffordAlgebra Q)) r✝)) =
    ↑involute (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r✝))
case h.h_grade1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑involute (↑(ι Q) x✝)) = ↑involute (↑reverse (↑(ι Q) x✝))
case h.h_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² * b✝)) = ↑involute (↑reverse (a✝² * b✝))
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² + b✝)) = ↑involute (↑reverse (a✝² + b✝))
[PROOFSTEP]
case h_grade0 => simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ ↑reverse (↑involute (↑(algebraMap R (CliffordAlgebra Q)) r✝)) =
    ↑involute (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r✝))
[PROOFSTEP]
case h_grade0 => simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ ↑reverse (↑involute (↑(algebraMap R (CliffordAlgebra Q)) r✝)) =
    ↑involute (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r✝))
[PROOFSTEP]
simp
[GOAL]
case h.h_grade1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑involute (↑(ι Q) x✝)) = ↑involute (↑reverse (↑(ι Q) x✝))
case h.h_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² * b✝)) = ↑involute (↑reverse (a✝² * b✝))
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² + b✝)) = ↑involute (↑reverse (a✝² + b✝))
[PROOFSTEP]
case h_grade1 => simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑involute (↑(ι Q) x✝)) = ↑involute (↑reverse (↑(ι Q) x✝))
[PROOFSTEP]
case h_grade1 => simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑reverse (↑involute (↑(ι Q) x✝)) = ↑involute (↑reverse (↑(ι Q) x✝))
[PROOFSTEP]
simp
[GOAL]
case h.h_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² * b✝)) = ↑involute (↑reverse (a✝² * b✝))
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² + b✝)) = ↑involute (↑reverse (a✝² + b✝))
[PROOFSTEP]
case h_mul a b ha hb => simp only [ha, hb, reverse.map_mul, AlgHom.map_mul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑involute a) = ↑involute (↑reverse a)
hb : ↑reverse (↑involute b) = ↑involute (↑reverse b)
⊢ ↑reverse (↑involute (a * b)) = ↑involute (↑reverse (a * b))
[PROOFSTEP]
case h_mul a b ha hb => simp only [ha, hb, reverse.map_mul, AlgHom.map_mul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑involute a) = ↑involute (↑reverse a)
hb : ↑reverse (↑involute b) = ↑involute (↑reverse b)
⊢ ↑reverse (↑involute (a * b)) = ↑involute (↑reverse (a * b))
[PROOFSTEP]
simp only [ha, hb, reverse.map_mul, AlgHom.map_mul]
[GOAL]
case h.h_add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑reverse (↑involute a✝²) = ↑involute (↑reverse a✝²)
a✝ : ↑reverse (↑involute b✝) = ↑involute (↑reverse b✝)
⊢ ↑reverse (↑involute (a✝² + b✝)) = ↑involute (↑reverse (a✝² + b✝))
[PROOFSTEP]
case h_add a b ha hb => simp only [ha, hb, reverse.map_add, AlgHom.map_add]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑involute a) = ↑involute (↑reverse a)
hb : ↑reverse (↑involute b) = ↑involute (↑reverse b)
⊢ ↑reverse (↑involute (a + b)) = ↑involute (↑reverse (a + b))
[PROOFSTEP]
case h_add a b ha hb => simp only [ha, hb, reverse.map_add, AlgHom.map_add]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : ↑reverse (↑involute a) = ↑involute (↑reverse a)
hb : ↑reverse (↑involute b) = ↑involute (↑reverse b)
⊢ ↑reverse (↑involute (a + b)) = ↑involute (↑reverse (a + b))
[PROOFSTEP]
simp only [ha, hb, reverse.map_add, AlgHom.map_add]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ↑reverse (List.prod (List.map ↑(ι Q) [])) = List.prod (List.reverse (List.map ↑(ι Q) []))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
xs : List M
⊢ ↑reverse (List.prod (List.map (↑(ι Q)) (x :: xs))) = List.prod (List.reverse (List.map (↑(ι Q)) (x :: xs)))
[PROOFSTEP]
simp [reverse_prod_map_ι xs]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ↑involute (List.prod (List.map ↑(ι Q) [])) = (-1) ^ List.length [] • List.prod (List.map ↑(ι Q) [])
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
xs : List M
⊢ ↑involute (List.prod (List.map (↑(ι Q)) (x :: xs))) =
    (-1) ^ List.length (x :: xs) • List.prod (List.map (↑(ι Q)) (x :: xs))
[PROOFSTEP]
simp [pow_succ, involute_prod_map_ι xs]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.comap (AlgHom.toLinearMap involute) (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
[PROOFSTEP]
rw [← submodule_map_involute_eq_comap, ι_range_map_involute]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
[PROOFSTEP]
simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.comap (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
[PROOFSTEP]
rw [← submodule_map_involute_eq_comap, evenOdd_map_involute]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
[PROOFSTEP]
rw [reverse, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp, ← Submodule.map_comp]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map (LinearMap.comp ↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) ↑(MulOpposite.opLinearEquiv R))
      (LinearMap.range (ι Q)) =
    LinearMap.range (ι Q)
[PROOFSTEP]
exact Submodule.map_id _
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.comap reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
[PROOFSTEP]
rw [← submodule_map_reverse_eq_comap, ι_range_map_reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
[PROOFSTEP]
simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.comap reverse (p * q) = Submodule.comap reverse q * Submodule.comap reverse p
[PROOFSTEP]
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_mul_reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
[PROOFSTEP]
simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n
[PROOFSTEP]
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_pow_reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n
[PROOFSTEP]
simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n
[PROOFSTEP]
rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
⊢ ↑involute x = x
[PROOFSTEP]
refine' even_induction Q (AlgHom.commutes _) _ _ x h
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
⊢ ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    ↑involute x = x → ↑involute y = y → ↑involute (x + y) = x + y
[PROOFSTEP]
rintro x y _hx _hy ihx ihy
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
h : x✝ ∈ evenOdd Q 0
x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : ↑involute x = x
ihy : ↑involute y = y
⊢ ↑involute (x + y) = x + y
[PROOFSTEP]
rw [map_add, ihx, ihy]
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
⊢ ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    ↑involute x = x → ↑involute (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) = ↑(ι Q) m₁ * ↑(ι Q) m₂ * x
[PROOFSTEP]
intro m₁ m₂ x _hx ihx
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
h : x✝ ∈ evenOdd Q 0
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : ↑involute x = x
⊢ ↑involute (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) = ↑(ι Q) m₁ * ↑(ι Q) m₂ * x
[PROOFSTEP]
rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
⊢ ↑involute x = -x
[PROOFSTEP]
refine' odd_induction Q involute_ι _ _ x h
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
⊢ ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    ↑involute x = -x → ↑involute y = -y → ↑involute (x + y) = -(x + y)
[PROOFSTEP]
rintro x y _hx _hy ihx ihy
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
h : x✝ ∈ evenOdd Q 1
x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : ↑involute x = -x
ihy : ↑involute y = -y
⊢ ↑involute (x + y) = -(x + y)
[PROOFSTEP]
rw [map_add, ihx, ihy, neg_add]
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
⊢ ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    ↑involute x = -x → ↑involute (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) = -(↑(ι Q) m₁ * ↑(ι Q) m₂ * x)
[PROOFSTEP]
intro m₁ m₂ x _hx ihx
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
h : x✝ ∈ evenOdd Q 1
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
ihx : ↑involute x = -x
⊢ ↑involute (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) = -(↑(ι Q) m₁ * ↑(ι Q) m₂ * x)
[PROOFSTEP]
rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]