-- 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.ι_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✝⟩
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x)).1 =
    (aux f) ⟨(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
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]

Result:
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✝⟩

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✝⟩
⊢ (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝))
        (x + y)).1 =
    (aux f) ⟨x + y, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
rw [LinearMap.map_add, Prod.fst_add, ihx, ihy, ← add_mul, ← LinearMap.map_add]

Result:
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✝⟩

Proof state:
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

Tactic:
cases y

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
⊢ (aux f) (⟨x, x_property⟩ * ⟨val✝, property✝⟩) = (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩