[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      (x✝² + x✝¹) x✝ =
    (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝² x✝ +
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝¹ x✝
[PROOFSTEP]
simp only [LinearMap.map_add, add_mul]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ {
      val :=
        ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ + ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
      property :=
        (_ :
          (fun x => x ∈ even Q)
            (↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ +
              ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝)) } =
    { val := ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) } +
      { val := ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      (x✝² • x✝¹) x✝ =
    x✝² •
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝¹ x✝
[PROOFSTEP]
simp only [LinearMap.map_smul, smul_mul_assoc]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ { val := x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝),
      property := (_ : (fun x => x ∈ even Q) (x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝))) } =
    x✝² •
      { val := ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      x✝² (x✝¹ + x✝) =
    (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝² x✝¹ +
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝² x✝
[PROOFSTEP]
simp only [LinearMap.map_add, mul_add]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ {
      val :=
        ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹ +
          ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝,
      property :=
        (_ :
          (fun x => x ∈ even Q)
            (↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹ +
              ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝)) } =
    { val := ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹ ∈ evenOdd Q 0) } +
      { val := ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      x✝¹ (x✝² • x✝) =
    x✝² •
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝¹ x✝
[PROOFSTEP]
simp only [LinearMap.map_smul, mul_smul_comm]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ { val := x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝),
      property := (_ : (fun x => x ∈ even Q) (x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝))) } =
    x✝² •
      { val := ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * (↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₃) =
    ↑(CliffordAlgebra.ι Q) m₁ * (↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₃)
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ ↑(CliffordAlgebra.ι Q) m₁ * (↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₃) =
    ↑Q m₂ • (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₃)
[PROOFSTEP]
rw [Algebra.smul_def, ι_sq_scalar, Algebra.left_comm]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : EvenHom.compr₂ (ι Q) f = EvenHom.compr₂ (ι Q) g
⊢ f = g
[PROOFSTEP]
rw [EvenHom.ext_iff] at h 
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
⊢ f = g
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case H.mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
[PROOFSTEP]
refine' even_induction _ _ _ _ _ hx
[GOAL]
case H.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ∀ (r : R),
    ↑f
        { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
          property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) } =
      ↑g
        { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
          property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) }
[PROOFSTEP]
intro r
[GOAL]
case H.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
r : R
⊢ ↑f
      { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) } =
    ↑g
      { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) }
[PROOFSTEP]
exact (f.commutes r).trans (g.commutes r).symm
[GOAL]
case H.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    ↑f { val := x, property := hx } = ↑g { val := x, property := hx } →
      ↑f { val := y, property := hy } = ↑g { val := y, property := hy } →
        ↑f { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } =
          ↑g { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) }
[PROOFSTEP]
intro x y hx hy ihx ihy
[GOAL]
case H.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
ihy : ↑f { val := y, property := hy } = ↑g { val := y, property := hy }
⊢ ↑f { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } =
    ↑g { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) }
[PROOFSTEP]
have := congr_arg₂ (· + ·) ihx ihy
[GOAL]
case H.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
ihy : ↑f { val := y, property := hy } = ↑g { val := y, property := hy }
this :
  (fun x_1 x_2 => x_1 + x_2) (↑f { val := x, property := hx }) (↑f { val := y, property := hy }) =
    (fun x_1 x_2 => x_1 + x_2) (↑g { val := x, property := hx }) (↑g { val := y, property := hy })
⊢ ↑f { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } =
    ↑g { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) }
[PROOFSTEP]
exact (f.map_add _ _).trans (this.trans <| (g.map_add _ _).symm)
[GOAL]
case H.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    ↑f { val := x, property := hx } = ↑g { val := x, property := hx } →
      ↑f
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } =
        ↑g
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) }
[PROOFSTEP]
intro m₁ m₂ x hx ih
[GOAL]
case H.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
⊢ ↑f
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } =
    ↑g
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) }
[PROOFSTEP]
have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
[GOAL]
case H.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
this :
  (fun x_1 x_2 => x_1 * x_2) (↑(↑(EvenHom.compr₂ (ι Q) f).bilin m₁) m₂) (↑f { val := x, property := hx }) =
    (fun x_1 x_2 => x_1 * x_2) (↑(↑(EvenHom.compr₂ (ι Q) g).bilin m₁) m₂) (↑g { val := x, property := hx })
⊢ ↑f
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } =
    ↑g
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) }
[PROOFSTEP]
exact (f.map_mul _ _).trans (this.trans <| (g.map_mul _ _).symm)
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
a : A × { x // x ∈ CliffordAlgebra.even.lift.S f }
m₃ : M
⊢ ↑(↑f.bilin m₃) (m₁ + m₂) * a.fst = ↑(↑f.bilin m₃) m₁ * a.fst + ↑(↑f.bilin m₃) m₂ * a.fst
[PROOFSTEP]
rw [map_add, add_mul]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
c : R
m : M
a : A × { x // x ∈ CliffordAlgebra.even.lift.S f }
m₃ : M
⊢ ↑(↑f.bilin m₃) (c • m) * a.fst = c • (↑(↑f.bilin m₃) m * a.fst)
[PROOFSTEP]
rw [LinearMap.map_smul, smul_mul_assoc]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }
⊢ ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x
[PROOFSTEP]
obtain ⟨a, ⟨g, hg⟩⟩ := x
[GOAL]
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
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(↑(CliffordAlgebra.even.lift.fFold f) m)
      (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg })) =
    ↑Q m • (a, { val := g, property := hg })
[PROOFSTEP]
ext : 2
[GOAL]
case mk.mk.h₁
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ (↑(↑(CliffordAlgebra.even.lift.fFold f) m)
        (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg }))).fst =
    (↑Q m • (a, { val := g, property := hg })).fst
[PROOFSTEP]
change f.bilin m m * a = Q m • a
[GOAL]
case mk.mk.h₁
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(↑f.bilin m) m * a = ↑Q m • a
[PROOFSTEP]
rw [Algebra.smul_def, f.contract]
[GOAL]
case mk.mk.h₂.a
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(↑(↑(CliffordAlgebra.even.lift.fFold f) m)
          (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg }))).snd =
    ↑(↑Q m • (a, { val := g, property := hg })).snd
[PROOFSTEP]
ext m₁
[GOAL]
case mk.mk.h₂.a.h
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑↑(↑(↑(CliffordAlgebra.even.lift.fFold f) m)
              (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg }))).snd
      m₁ =
    ↑↑(↑Q m • (a, { val := g, property := hg })).snd m₁
[PROOFSTEP]
change f.bilin _ _ * g m = Q m • g m₁
[GOAL]
case mk.mk.h₂.a.h
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(↑f.bilin m₁) m * ↑g m = ↑Q m • ↑g m₁
[PROOFSTEP]
apply Submodule.span_induction' _ _ _ _ hg
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ∀ (x : M →ₗ[R] A),
    x ∈ {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
      ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁
[PROOFSTEP]
rintro _ ⟨b, m₃, rfl⟩
[GOAL]
case intro.intro
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
b : A
m₃ : M
⊢ ↑(↑f.bilin m₁) m * ↑(↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₃)) (LinearMap.mulRight R b)) m =
    ↑Q m • ↑(↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₃)) (LinearMap.mulRight R b)) m₁
[PROOFSTEP]
change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)
[GOAL]
case intro.intro
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
b : A
m₃ : M
⊢ ↑(↑f.bilin m₁) m * (↑(↑f.bilin m) m₃ * b) = ↑Q m • (↑(↑f.bilin m₁) m₃ * b)
[PROOFSTEP]
rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(↑f.bilin m₁) m * ↑0 m = ↑Q m • ↑0 m₁
[PROOFSTEP]
change
  f.bilin m₁ m * 0 =
    Q m •
      (0 : A)
        -- porting note: `•` now needs the type of `0`
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(↑f.bilin m₁) m * 0 = ↑Q m • 0
[PROOFSTEP]
rw [mul_zero, smul_zero]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ∀ (x : M →ₗ[R] A),
    x ∈
        Submodule.span R
          {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
      ∀ (y : M →ₗ[R] A),
        y ∈
            Submodule.span R
              {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
          ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁ →
            ↑(↑f.bilin m₁) m * ↑y m = ↑Q m • ↑y m₁ → ↑(↑f.bilin m₁) m * ↑(x + y) m = ↑Q m • ↑(x + y) m₁
[PROOFSTEP]
rintro x hx y hy ihx ihy
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
x : M →ₗ[R] A
hx :
  x ∈
    Submodule.span R {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)}
y : M →ₗ[R] A
hy :
  y ∈
    Submodule.span R {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)}
ihx : ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁
ihy : ↑(↑f.bilin m₁) m * ↑y m = ↑Q m • ↑y m₁
⊢ ↑(↑f.bilin m₁) m * ↑(x + y) m = ↑Q m • ↑(x + y) m₁
[PROOFSTEP]
rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ∀ (a : R) (x : M →ₗ[R] A),
    x ∈
        Submodule.span R
          {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
      ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁ → ↑(↑f.bilin m₁) m * ↑(a • x) m = ↑Q m • ↑(a • x) m₁
[PROOFSTEP]
rintro x hx c ihx
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
x : R
hx : M →ₗ[R] A
c :
  hx ∈
    Submodule.span R {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)}
ihx : ↑(↑f.bilin m₁) m * ↑hx m = ↑Q m • ↑hx m₁
⊢ ↑(↑f.bilin m₁) m * ↑(x • hx) m = ↑Q m • ↑(x • hx) m₁
[PROOFSTEP]
rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
  -- Porting note: In Lean 3, `aux_apply` isn't a simp lemma. I changed `{ attrs := [] }` to
  -- `{ isSimp := false }`, so that `aux_apply` isn't a simp lemma.
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
⊢ { x // x ∈ even Q } →ₗ[R] A
[PROOFSTEP]
refine ?_ ∘ₗ (even Q).val.toLinearMap
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
⊢ CliffordAlgebra Q →ₗ[R] A
[PROOFSTEP]
letI : AddCommGroup (S f) := AddSubgroupClass.toAddCommGroup _
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
this : AddCommGroup { x // x ∈ CliffordAlgebra.even.lift.S f } :=
  AddSubgroupClass.toAddCommGroup (CliffordAlgebra.even.lift.S f)
⊢ CliffordAlgebra Q →ₗ[R] A
[PROOFSTEP]
exact LinearMap.fst R _ _ ∘ₗ foldr Q (fFold f) (fFold_fFold f) (1, 0)
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              (↑(CliffordAlgebra.ι Q) m₂)))
        (↑(CliffordAlgebra.ι Q) m₁)).fst =
    ↑(↑f.bilin m₁) m₂
[PROOFSTEP]
rw [foldr_ι, foldr_ι]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
⊢ (↑(↑(CliffordAlgebra.even.lift.fFold f) m₁) (↑(↑(CliffordAlgebra.even.lift.fFold f) m₂) (1, 0))).fst =
    ↑(↑f.bilin m₁) m₂
[PROOFSTEP]
exact mul_one _
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x y : { x // x ∈ even Q }
⊢ ↑(aux f) (x * y) = ↑(aux f) x * ↑(aux f) y
[PROOFSTEP]
cases' x with x x_property
[GOAL]
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
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
y : { x // x ∈ even Q }
x : CliffordAlgebra Q
x_property : x ∈ even Q
⊢ ↑(aux f) ({ val := x, property := x_property } * y) = ↑(aux f) { val := x, property := x_property } * ↑(aux f) y
[PROOFSTEP]
cases y
[GOAL]
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
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ↑(aux f) ({ val := x, property := x_property } * { val := val✝, property := property✝ }) =
    ↑(aux f) { val := x, property := x_property } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
refine' (congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans _
[GOAL]
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
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
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)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              ↑{ val := val✝, property := property✝ }))
        ↑{ val := x, property := x_property }).fst =
    ↑(aux f) { val := x, property := x_property } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
dsimp only
[GOAL]
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
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
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)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := x_property } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
refine' even_induction Q _ _ _ _ x_property
[GOAL]
case mk.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ∀ (r : R),
    (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                  (_ :
                    ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                      ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                        ↑Q m • x))
              (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                        (_ :
                          ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                            ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                              ↑Q m • x))
                    (1, 0))
                val✝))
          (↑(algebraMap R (CliffordAlgebra Q)) r)).fst =
      ↑(aux f)
          { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
            property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0) } *
        ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
intro r
[GOAL]
case mk.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        (↑(algebraMap R (CliffordAlgebra Q)) r)).fst =
    ↑(aux f)
        { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
          property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0) } *
      ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rw [foldr_algebraMap, aux_algebraMap]
[GOAL]
case mk.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (r •
        ↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                  (_ :
                    ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                      ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                        ↑Q m • x))
              (1, 0))
          val✝).fst =
    ↑(algebraMap R A) r * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
exact Algebra.smul_def r _
[GOAL]
case mk.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                          (_ :
                            ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                              ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                ↑Q m • x))
                      (1, 0))
                  val✝))
            x).fst =
        ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ } →
      (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                            (_ :
                              ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                                ↑(↑(CliffordAlgebra.even.lift.fFold f) m)
                                    (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                  ↑Q m • x))
                        (1, 0))
                    val✝))
              y).fst =
          ↑(aux f) { val := y, property := hy } * ↑(aux f) { val := val✝, property := property✝ } →
        (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                            (_ :
                              ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                                ↑(↑(CliffordAlgebra.even.lift.fFold f) m)
                                    (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                  ↑Q m • x))
                        (1, 0))
                    val✝))
              (x + y)).fst =
          ↑(aux f) { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } *
            ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
intro x y hx hy ihx ihy
[GOAL]
case mk.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
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)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
ihy :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        y).fst =
    ↑(aux f) { val := y, property := hy } * ↑(aux f) { val := val✝, property := property✝ }
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        (x + y)).fst =
    ↑(aux f) { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rw [LinearMap.map_add, Prod.fst_add, ihx, ihy, ← add_mul, ← LinearMap.map_add]
[GOAL]
case mk.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
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)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
ihy :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        y).fst =
    ↑(aux f) { val := y, property := hy } * ↑(aux f) { val := val✝, property := property✝ }
⊢ ↑(aux f) ({ val := x, property := hx } + { val := y, property := hy }) *
      ↑(aux f) { val := val✝, property := property✝ } =
    ↑(aux f) { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                          (_ :
                            ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                              ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                ↑Q m • x))
                      (1, 0))
                  val✝))
            x).fst =
        ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ } →
      (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                          (_ :
                            ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                              ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                ↑Q m • x))
                      (1, 0))
                  val✝))
            (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x)).fst =
        ↑(aux f)
            { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
              property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } *
          ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rintro m₁ m₂ x (hx : x ∈ even Q) ih
[GOAL]
case mk.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ even Q
ih :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x)).fst =
    ↑(aux f)
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } *
      ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
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]
[GOAL]
case mk.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ even Q
ih :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
⊢ ↑(↑f.bilin m₁) m₂ * ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ } =
    ↑(↑f.bilin m₁) m₂ *
        (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (1, 0))
            x).fst *
      ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
