-- Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
theorem aux_mul (x y : even Q) : aux f (x * y) = aux f x * aux f y

Proof state:
case mk.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯)
          (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ↑⟨val✝, property✝⟩))
        ↑⟨x, x_property⟩).1 =
    (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
dsimp only

Result:
case mk.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        x).1 =
    (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩

Proof state:
case mk.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        x).1 =
    (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
induction x, x_property using even_induction Q with
| algebraMap r =>
  rw [foldr_algebraMap, aux_algebraMap]
  exact Algebra.smul_def r _
| add x y hx hy ihx ihy =>
  rw [LinearMap.map_add, Prod.fst_add, ihx, ihy, ← add_mul, ← LinearMap.map_add]
  rfl
| ι_mul_ι_mul m₁ m₂ x hx ih =>
  rw [aux_apply, foldr_mul, foldr_mul, foldr_ι, foldr_ι, fst_fFold_fFold, ih, ← mul_assoc,
    Subtype.coe_mk, foldr_mul, foldr_mul, foldr_ι, foldr_ι, fst_fFold_fFold]
  rfl

Result:
no goals

Proof state:
case mk.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (aux f) (⟨x, x_property⟩ * ⟨val✝, property✝⟩) = (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
refine (congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans ?_

Result:
case mk.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯)
          (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ↑⟨val✝, property✝⟩))
        ↑⟨x, x_property⟩).1 =
    (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩

Proof state:
case mk.mk.algebraMap
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (r • ((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝).1 = (algebraMap R A) r * (aux f) ⟨val✝, property✝⟩

Tactic:
exact Algebra.smul_def r _

Result:
no goals

Proof state:
case mk.mk.ι_mul_ι_mul
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x✝ val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih :
  (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        x).1 =
    (aux f) ⟨x, hx⟩ * (aux f) ⟨val✝, property✝⟩
⊢ (f.bilin m₁) m₂ * (aux f) ⟨x, hx⟩ * (aux f) ⟨val✝, property✝⟩ =
    (f.bilin m₁) m₂ * (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) x).1 * (aux f) ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x y : ↥(even Q)
⊢ (aux f) (x * y) = (aux f) x * (aux f) y

Tactic:
obtain ⟨x, x_property⟩ := x

Result:
case mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
y : ↥(even Q)
x : CliffordAlgebra Q
x_property : x ∈ even Q
⊢ (aux f) (⟨x, x_property⟩ * y) = (aux f) ⟨x, x_property⟩ * (aux f) y

Proof state:
case mk.mk.algebraMap
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        ((algebraMap R (CliffordAlgebra Q)) r)).1 =
    (aux f) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
rw [foldr_algebraMap, aux_algebraMap]

Result:
case mk.mk.algebraMap
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (r • ((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝).1 = (algebraMap R A) r * (aux f) ⟨val✝, property✝⟩

Proof state:
case mk.mk.add
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x✝ val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx :
  (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        x).1 =
    (aux f) ⟨x, hx⟩ * (aux f) ⟨val✝, property✝⟩
ihy :
  (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        y).1 =
    (aux f) ⟨y, hy⟩ * (aux f) ⟨val✝, property✝⟩
⊢ (aux f) (⟨x, hx⟩ + ⟨y, hy⟩) * (aux f) ⟨val✝, property✝⟩ = (aux f) ⟨x + y, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals