[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
r : R
⊢ ↑(ι (Q' Q)) (m, r) = ↑(v Q) m + r • e0 Q
[PROOFSTEP]
rw [e0, v, LinearMap.comp_apply, LinearMap.inl_apply, ← LinearMap.map_smul, Prod.smul_mk, smul_zero, smul_eq_mul,
  mul_one, ← LinearMap.map_add, Prod.mk_add_mk, zero_add, add_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ↑(algebraMap R (CliffordAlgebra (Q' Q))) (↑(Q' Q) (0, 1)) = -1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(algebraMap R (CliffordAlgebra (Q' Q))) (↑(Q' Q) (↑(LinearMap.inl R M R) m)) =
    ↑(algebraMap R (CliffordAlgebra (Q' Q))) (↑Q m)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ -(e0 Q * ↑(v Q) m) = ↑(v Q) m * e0 Q
[PROOFSTEP]
refine' neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(algebraMap R (CliffordAlgebra (Q' Q))) (QuadraticForm.polar ↑(Q' Q) (0, 1) (↑(LinearMap.inl R M R) m)) = 0
[PROOFSTEP]
dsimp [QuadraticForm.polar]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(algebraMap R (CliffordAlgebra (Q' Q))) (↑Q (0 + m) + -((1 + 0) * (1 + 0)) - (↑Q 0 + -(1 * 1)) - (↑Q m + -(0 * 0))) =
    0
[PROOFSTEP]
simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero, QuadraticForm.map_zero, add_sub_cancel, sub_self, map_zero,
  zero_sub]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ -(↑(v Q) m * e0 Q) = e0 Q * ↑(v Q) m
[PROOFSTEP]
rw [neg_eq_iff_eq_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(v Q) m * e0 Q = -(e0 Q * ↑(v Q) m)
[PROOFSTEP]
exact (neg_e0_mul_v _ m).symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ e0 Q * ↑(v Q) m * e0 Q = ↑(v Q) m
[PROOFSTEP]
rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ CliffordAlgebra Q →ₐ[R] { x // x ∈ even (Q' Q) }
[PROOFSTEP]
refine' CliffordAlgebra.lift Q ⟨_, fun m => _⟩
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] { x // x ∈ even (Q' Q) }
[PROOFSTEP]
refine' LinearMap.codRestrict _ _ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ _
[GOAL]
case refine'_1.refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] CliffordAlgebra (Q' Q)
case refine'_1.refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑?refine'_1.refine'_1 m ∈ LinearMap.range (ι (Q' Q)) ^ ↑{ val := 2, property := (_ : ↑2 = ↑2) }
[PROOFSTEP]
exact (LinearMap.mulLeft R <| e0 Q).comp (v Q)
[GOAL]
case refine'_1.refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
    LinearMap.range (ι (Q' Q)) ^ ↑{ val := 2, property := (_ : ↑2 = ↑2) }
[PROOFSTEP]
rw [Subtype.coe_mk, pow_two]
[GOAL]
case refine'_1.refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈ LinearMap.range (ι (Q' Q)) * LinearMap.range (ι (Q' Q))
[PROOFSTEP]
exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
            (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
            (_ :
              ∀ (m : M),
                ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                  ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
        m *
      ↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
            (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
            (_ :
              ∀ (m : M),
                ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                  ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
        m =
    ↑(algebraMap R { x // x ∈ even (Q' Q) }) (↑Q m)
[PROOFSTEP]
ext1
[GOAL]
case refine'_2.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
              (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
              (_ :
                ∀ (m : M),
                  ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                    ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
          m *
        ↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
              (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
              (_ :
                ∀ (m : M),
                  ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                    ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
          m) =
    ↑(↑(algebraMap R { x // x ∈ even (Q' Q) }) (↑Q m))
[PROOFSTEP]
rw [Subalgebra.coe_mul]
  -- porting note: was part of the `dsimp only` below
[GOAL]
case refine'_2.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
              (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
              (_ :
                ∀ (m : M),
                  ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                    ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
          m) *
      ↑(↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
              (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
              (_ :
                ∀ (m : M),
                  ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                    ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
          m) =
    ↑(↑(algebraMap R { x // x ∈ even (Q' Q) }) (↑Q m))
[PROOFSTEP]
erw [LinearMap.codRestrict_apply]
  -- porting note: was part of the `dsimp only` below
[GOAL]
case refine'_2.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m * ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m =
    ↑(↑(algebraMap R { x // x ∈ even (Q' Q) }) (↑Q m))
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, LinearMap.mulLeft_apply, Subalgebra.coe_algebraMap]
[GOAL]
case refine'_2.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ e0 Q * ↑(v Q) m * (e0 Q * ↑(v Q) m) = ↑(algebraMap R (CliffordAlgebra (Q' Q))) (↑Q m)
[PROOFSTEP]
rw [← mul_assoc, e0_mul_v_mul_e0, v_sq_scalar]
[GOAL]
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) (↑(ι Q) m)) = e0 Q * ↑(v Q) m
[PROOFSTEP]
rw [toEven, CliffordAlgebra.lift_ι_apply]
  -- porting note: was `rw`
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(↑(LinearMap.codRestrict (⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i)
            (LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q))
            (_ :
              ∀ (m : M),
                ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m ∈
                  ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι (Q' Q)) ^ ↑i))
        m) =
    e0 Q * ↑(v Q) m
[PROOFSTEP]
erw [LinearMap.codRestrict_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(LinearMap.comp (LinearMap.mulLeft R (e0 Q)) (v Q)) m = e0 Q * ↑(v Q) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ { x // x ∈ even (Q' Q) } →ₐ[R] CliffordAlgebra Q
[PROOFSTEP]
let f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap.comp <|
        (ι Q).comp (LinearMap.fst _ _ _) + (Algebra.linearMap R _).comp (LinearMap.snd _ _ _)).compl₂
    ((ι Q).comp (LinearMap.fst _ _ _) - (Algebra.linearMap R _).comp (LinearMap.snd _ _ _))
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
⊢ { x // x ∈ even (Q' Q) } →ₐ[R] CliffordAlgebra Q
[PROOFSTEP]
haveI f_apply : ∀ x y, f x y = (ι Q x.1 + algebraMap R _ x.2) * (ι Q y.1 - algebraMap R _ y.2) := fun x y => by rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
x y : M × R
⊢ ↑(↑f x) y =
    (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
      (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
⊢ { x // x ∈ even (Q' Q) } →ₐ[R] CliffordAlgebra Q
[PROOFSTEP]
haveI hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (algebraMap _ _ r) x := Algebra.commutes
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
⊢ { x // x ∈ even (Q' Q) } →ₐ[R] CliffordAlgebra Q
[PROOFSTEP]
haveI hm : ∀ m : M × R, ι Q m.1 * ι Q m.1 - algebraMap R _ m.2 * algebraMap R _ m.2 = algebraMap R _ (Q' Q m) :=
  by
  intro m
  rw [ι_sq_scalar, ← RingHom.map_mul, ← RingHom.map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
⊢ ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
[PROOFSTEP]
intro m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
m : M × R
⊢ ↑(ι Q) m.fst * ↑(ι Q) m.fst - ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
    ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
[PROOFSTEP]
rw [ι_sq_scalar, ← RingHom.map_mul, ← RingHom.map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
⊢ { x // x ∈ even (Q' Q) } →ₐ[R] CliffordAlgebra Q
[PROOFSTEP]
refine' even.lift (Q' Q) ⟨f, _, _⟩
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
⊢ ∀ (m : M × R), ↑(↑f m) m = ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
[PROOFSTEP]
simp_rw [f_apply]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
⊢ ∀ (m₁ m₂ m₃ : M × R), ↑(↑f m₁) m₂ * ↑(↑f m₂) m₃ = ↑(Q' Q) m₂ • ↑(↑f m₁) m₃
[PROOFSTEP]
simp_rw [f_apply]
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
⊢ ∀ (m : M × R),
    (↑(ι Q) m.fst + ↑(algebraMap R (CliffordAlgebra Q)) m.snd) *
        (↑(ι Q) m.fst - ↑(algebraMap R (CliffordAlgebra Q)) m.snd) =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
[PROOFSTEP]
intro m
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
m : M × R
⊢ (↑(ι Q) m.fst + ↑(algebraMap R (CliffordAlgebra Q)) m.snd) *
      (↑(ι Q) m.fst - ↑(algebraMap R (CliffordAlgebra Q)) m.snd) =
    ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
[PROOFSTEP]
rw [← (hc _ _).symm.mul_self_sub_mul_self_eq, hm]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
⊢ ∀ (m₁ m₂ m₃ : M × R),
    (↑(ι Q) m₁.fst + ↑(algebraMap R (CliffordAlgebra Q)) m₁.snd) *
          (↑(ι Q) m₂.fst - ↑(algebraMap R (CliffordAlgebra Q)) m₂.snd) *
        ((↑(ι Q) m₂.fst + ↑(algebraMap R (CliffordAlgebra Q)) m₂.snd) *
          (↑(ι Q) m₃.fst - ↑(algebraMap R (CliffordAlgebra Q)) m₃.snd)) =
      ↑(Q' Q) m₂ •
        ((↑(ι Q) m₁.fst + ↑(algebraMap R (CliffordAlgebra Q)) m₁.snd) *
          (↑(ι Q) m₃.fst - ↑(algebraMap R (CliffordAlgebra Q)) m₃.snd))
[PROOFSTEP]
intro m₁ m₂ m₃
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
f_apply :
  ∀ (x y : M × R),
    ↑(↑f x) y =
      (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
        (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (↑(algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    ↑(ι Q) m.fst * ↑(ι Q) m.fst -
        ↑(algebraMap R (CliffordAlgebra Q)) m.snd * ↑(algebraMap R (CliffordAlgebra Q)) m.snd =
      ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ (↑(ι Q) m₁.fst + ↑(algebraMap R (CliffordAlgebra Q)) m₁.snd) *
        (↑(ι Q) m₂.fst - ↑(algebraMap R (CliffordAlgebra Q)) m₂.snd) *
      ((↑(ι Q) m₂.fst + ↑(algebraMap R (CliffordAlgebra Q)) m₂.snd) *
        (↑(ι Q) m₃.fst - ↑(algebraMap R (CliffordAlgebra Q)) m₃.snd)) =
    ↑(Q' Q) m₂ •
      ((↑(ι Q) m₁.fst + ↑(algebraMap R (CliffordAlgebra Q)) m₁.snd) *
        (↑(ι Q) m₃.fst - ↑(algebraMap R (CliffordAlgebra Q)) m₃.snd))
[PROOFSTEP]
rw [← mul_smul_comm, ← mul_assoc, mul_assoc (_ + _), ← (hc _ _).symm.mul_self_sub_mul_self_eq', Algebra.smul_def, ←
  mul_assoc, hm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : M × R
⊢ ↑(ofEven Q) (↑(↑(even.ι (Q' Q)).bilin x) y) =
    (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
      (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
[PROOFSTEP]
unfold ofEven
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : M × R
⊢ ↑(let f :=
          LinearMap.compl₂
            (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
              (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
            (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
              LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R));
        ↑(even.lift (Q' Q))
          { bilin := f,
            contract :=
              (_ :
                ∀ (m : M × R),
                  ↑(↑(LinearMap.compl₂
                              (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                              (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                          m)
                      m =
                    ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)),
            contract_mid :=
              (_ :
                ∀ (m₁ m₂ m₃ : M × R),
                  ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₁)
                        m₂ *
                      ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₂)
                        m₃ =
                    ↑(Q' Q) m₂ •
                      ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₁)
                        m₃) })
      (↑(↑(even.ι (Q' Q)).bilin x) y) =
    (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
      (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
[PROOFSTEP]
lift_lets
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : M × R
⊢ let f :=
    LinearMap.compl₂
      (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
        (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
          LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R));
  ↑(↑(even.lift (Q' Q))
          { bilin := f,
            contract :=
              (_ :
                ∀ (m : M × R),
                  ↑(↑(LinearMap.compl₂
                              (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                              (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                          m)
                      m =
                    ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)),
            contract_mid :=
              (_ :
                ∀ (m₁ m₂ m₃ : M × R),
                  ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₁)
                        m₂ *
                      ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₂)
                        m₃ =
                    ↑(Q' Q) m₂ •
                      ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₁)
                        m₃) })
      (↑(↑(even.ι (Q' Q)).bilin x) y) =
    (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
      (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : M × R
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  LinearMap.compl₂
    (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
      (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
        LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
    (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
      LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R))
⊢ ↑(↑(even.lift (Q' Q))
          { bilin := f,
            contract :=
              (_ :
                ∀ (m : M × R),
                  ↑(↑(LinearMap.compl₂
                              (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                              (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                          m)
                      m =
                    ↑(algebraMap R (CliffordAlgebra Q)) (↑(Q' Q) m)),
            contract_mid :=
              (_ :
                ∀ (m₁ m₂ m₃ : M × R),
                  ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₁)
                        m₂ *
                      ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₂)
                        m₃ =
                    ↑(Q' Q) m₂ •
                      ↑(↑(LinearMap.compl₂
                                (LinearMap.comp (AlgHom.toLinearMap (Algebra.lmul R (CliffordAlgebra Q)))
                                  (LinearMap.comp (ι Q) (LinearMap.fst R M R) +
                                    LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                                (LinearMap.comp (ι Q) (LinearMap.fst R M R) -
                                  LinearMap.comp (Algebra.linearMap R (CliffordAlgebra Q)) (LinearMap.snd R M R)))
                            m₁)
                        m₃) })
      (↑(↑(even.ι (Q' Q)).bilin x) y) =
    (↑(ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) *
      (↑(ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)
[PROOFSTEP]
refine @even.lift_ι R (M × R) _ _ _ (Q' Q) _ _ _ ⟨f, ?_, ?_⟩ x y
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ ↑(↑(toEven Q) (↑(ofEven Q) (↑(↑(even.ι (Q' Q)).bilin (m₁, r₁)) (m₂, r₂)))) =
    (e0 Q * ↑(v Q) m₁ + ↑(algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * ↑(v Q) m₂ - ↑(algebraMap R (CliffordAlgebra (Q' Q))) r₂)
[PROOFSTEP]
rw [ofEven_ι, AlgHom.map_mul, AlgHom.map_add, AlgHom.map_sub, AlgHom.commutes, AlgHom.commutes, Subalgebra.coe_mul,
  Subalgebra.coe_add, Subalgebra.coe_sub, toEven_ι, toEven_ι, Subalgebra.coe_algebraMap, Subalgebra.coe_algebraMap]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (e0 Q * ↑(v Q) m₁ + ↑(algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * ↑(v Q) m₂ - ↑(algebraMap R (CliffordAlgebra (Q' Q))) r₂) =
    e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) + r₁ • e0 Q * ↑(v Q) m₂ - r₂ • e0 Q * ↑(v Q) m₁ -
      ↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)
[PROOFSTEP]
rw [mul_sub, add_mul, add_mul, ← Algebra.commutes, ← Algebra.smul_def, ← map_mul, ← Algebra.smul_def,
  sub_add_eq_sub_sub, smul_mul_assoc, smul_mul_assoc]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) + r₁ • e0 Q * ↑(v Q) m₂ - r₂ • e0 Q * ↑(v Q) m₁ -
      ↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    ↑(v Q) m₁ * ↑(v Q) m₂ + r₁ • e0 Q * ↑(v Q) m₂ + ↑(v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
[PROOFSTEP]
have h1 : e0 Q * v Q m₁ * (e0 Q * v Q m₂) = v Q m₁ * v Q m₂ := by rw [← mul_assoc, e0_mul_v_mul_e0]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) = ↑(v Q) m₁ * ↑(v Q) m₂
[PROOFSTEP]
rw [← mul_assoc, e0_mul_v_mul_e0]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) = ↑(v Q) m₁ * ↑(v Q) m₂
⊢ e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) + r₁ • e0 Q * ↑(v Q) m₂ - r₂ • e0 Q * ↑(v Q) m₁ -
      ↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    ↑(v Q) m₁ * ↑(v Q) m₂ + r₁ • e0 Q * ↑(v Q) m₂ + ↑(v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
[PROOFSTEP]
have h2 : -(r₂ • e0 Q * v Q m₁) = v Q m₁ * r₂ • e0 Q := by rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) = ↑(v Q) m₁ * ↑(v Q) m₂
⊢ -(r₂ • e0 Q * ↑(v Q) m₁) = ↑(v Q) m₁ * r₂ • e0 Q
[PROOFSTEP]
rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) = ↑(v Q) m₁ * ↑(v Q) m₂
h2 : -(r₂ • e0 Q * ↑(v Q) m₁) = ↑(v Q) m₁ * r₂ • e0 Q
⊢ e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) + r₁ • e0 Q * ↑(v Q) m₂ - r₂ • e0 Q * ↑(v Q) m₁ -
      ↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    ↑(v Q) m₁ * ↑(v Q) m₂ + r₁ • e0 Q * ↑(v Q) m₂ + ↑(v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
[PROOFSTEP]
have h3 : -algebraMap R _ (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q := by
  rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul, e0_mul_e0, smul_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) = ↑(v Q) m₁ * ↑(v Q) m₂
h2 : -(r₂ • e0 Q * ↑(v Q) m₁) = ↑(v Q) m₁ * r₂ • e0 Q
⊢ -↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul, e0_mul_e0, smul_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) = ↑(v Q) m₁ * ↑(v Q) m₂
h2 : -(r₂ • e0 Q * ↑(v Q) m₁) = ↑(v Q) m₁ * r₂ • e0 Q
h3 : -↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q
⊢ e0 Q * ↑(v Q) m₁ * (e0 Q * ↑(v Q) m₂) + r₁ • e0 Q * ↑(v Q) m₂ - r₂ • e0 Q * ↑(v Q) m₁ -
      ↑(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    ↑(v Q) m₁ * ↑(v Q) m₂ + r₁ • e0 Q * ↑(v Q) m₂ + ↑(v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, h1, h2, h3]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ ↑(v Q) m₁ * ↑(v Q) m₂ + r₁ • e0 Q * ↑(v Q) m₂ + ↑(v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q =
    ↑(ι (Q' Q)) (m₁, r₁) * ↑(ι (Q' Q)) (m₂, r₂)
[PROOFSTEP]
rw [ι_eq_v_add_smul_e0, ι_eq_v_add_smul_e0, mul_add, add_mul, add_mul, add_assoc]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(ofEven Q) (↑(toEven Q) (↑(ι Q) m)) =
    ↑(ofEven Q) { val := ↑(↑(toEven Q) (↑(ι Q) m)), property := (_ : ↑(↑(toEven Q) (↑(ι Q) m)) ∈ even (Q' Q)) }
[PROOFSTEP]
rw [Subtype.coe_eta]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(ofEven Q) { val := ↑(↑(toEven Q) (↑(ι Q) m)), property := (_ : ↑(↑(toEven Q) (↑(ι Q) m)) ∈ even (Q' Q)) } =
    (↑(ι Q) 0 + ↑(algebraMap R (CliffordAlgebra Q)) 1) * (↑(ι Q) m - ↑(algebraMap R (CliffordAlgebra Q)) 0)
[PROOFSTEP]
simp_rw [toEven_ι]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(ofEven Q) { val := e0 Q * ↑(v Q) m, property := (_ : (fun x => x ∈ even (Q' Q)) (e0 Q * ↑(v Q) m)) } =
    (↑(ι Q) 0 + ↑(algebraMap R (CliffordAlgebra Q)) 1) * (↑(ι Q) m - ↑(algebraMap R (CliffordAlgebra Q)) 0)
[PROOFSTEP]
exact ofEven_ι Q _ _
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (↑(ι Q) 0 + ↑(algebraMap R (CliffordAlgebra Q)) 1) * (↑(ι Q) m - ↑(algebraMap R (CliffordAlgebra Q)) 0) = ↑(ι Q) m
[PROOFSTEP]
rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
[GOAL]
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)
[PROOFSTEP]
induction x using CliffordAlgebra.induction
[GOAL]
case h_grade0
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✝))
case h_grade1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (↑(ι Q) x✝)))) = ↑reverse ↑(↑(toEven Q) (↑(ι Q) x✝))
case h_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² * b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² * b✝))
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² + b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² + b✝))
[PROOFSTEP]
case h_grade0 r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
[GOAL]
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))
[PROOFSTEP]
case h_grade0 r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
[GOAL]
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))
[PROOFSTEP]
simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
[GOAL]
case h_grade1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (↑(ι Q) x✝)))) = ↑reverse ↑(↑(toEven Q) (↑(ι Q) x✝))
case h_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² * b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² * b✝))
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² + b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² + b✝))
[PROOFSTEP]
case h_grade1 m =>
  -- porting note: added `letI`
  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]
[GOAL]
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))
[PROOFSTEP]
case h_grade1 m =>
  -- porting note: added `letI`
  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]
[GOAL]
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))
[PROOFSTEP]
letI : SubtractionMonoid (even (Q' Q)) := AddGroup.toSubtractionMonoid
[GOAL]
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 { x // x ∈ even (Q' Q) } := AddGroup.toSubtractionMonoid
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (↑(ι Q) m)))) = ↑reverse ↑(↑(toEven Q) (↑(ι Q) m))
[PROOFSTEP]
simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0, reverse_ι, neg_e0_mul_v,
  map_neg]
[GOAL]
case h_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² * b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² * b✝))
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² + b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² + b✝))
[PROOFSTEP]
case h_mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
[GOAL]
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))
[PROOFSTEP]
case h_mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
[GOAL]
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))
[PROOFSTEP]
simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a✝² b✝ : CliffordAlgebra Q
a✝¹ : ↑(↑(toEven Q) (↑reverse (↑involute a✝²))) = ↑reverse ↑(↑(toEven Q) a✝²)
a✝ : ↑(↑(toEven Q) (↑reverse (↑involute b✝))) = ↑reverse ↑(↑(toEven Q) b✝)
⊢ ↑(↑(toEven Q) (↑reverse (↑involute (a✝² + b✝)))) = ↑reverse ↑(↑(toEven Q) (a✝² + b✝))
[PROOFSTEP]
case h_add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
[GOAL]
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))
[PROOFSTEP]
case h_add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
[GOAL]
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))
[PROOFSTEP]
simp only [map_add, Subalgebra.coe_add, hx, hy]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
this✝ : AddCommGroup { x // x ∈ even Q' } := AddSubgroupClass.toAddCommGroup (even Q')
this : HasDistribNeg { x // x ∈ even Q' } := NonUnitalNonAssocRing.toHasDistribNeg
m : M
⊢ ↑(↑(-(even.ι Q').bilin) m) m = ↑(algebraMap R { x // x ∈ even Q' }) (↑Q m)
[PROOFSTEP]
simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticForm.neg_apply, map_neg, neg_neg]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
this✝ : AddCommGroup { x // x ∈ even Q' } := AddSubgroupClass.toAddCommGroup (even Q')
this : HasDistribNeg { x // x ∈ even Q' } := NonUnitalNonAssocRing.toHasDistribNeg
m₁ m₂ m₃ : M
⊢ ↑(↑(-(even.ι Q').bilin) m₁) m₂ * ↑(↑(-(even.ι Q').bilin) m₂) m₃ = ↑Q m₂ • ↑(↑(-(even.ι Q').bilin) m₁) m₃
[PROOFSTEP]
simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h, QuadraticForm.neg_apply, smul_neg, neg_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
⊢ AlgHom.comp (evenToNeg Q' Q h') (evenToNeg Q Q' h) = AlgHom.id R { x // x ∈ even Q }
[PROOFSTEP]
ext m₁ m₂ : 4
[GOAL]
case h.bilin.h.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
m₁ m₂ : M
⊢ ↑(↑(EvenHom.compr₂ (even.ι Q) (AlgHom.comp (evenToNeg Q' Q h') (evenToNeg Q Q' h))).bilin m₁) m₂ =
    ↑(↑(EvenHom.compr₂ (even.ι Q) (AlgHom.id R { x // x ∈ even Q })).bilin m₁) m₂
[PROOFSTEP]
dsimp only [EvenHom.compr₂_bilin, LinearMap.compr₂_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply]
[GOAL]
case h.bilin.h.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
m₁ m₂ : M
⊢ ↑(evenToNeg Q' Q h') (↑(evenToNeg Q Q' h) (↑(↑(even.ι Q).bilin m₁) m₂)) = ↑(↑(even.ι Q).bilin m₁) m₂
[PROOFSTEP]
rw [evenToNeg_ι, map_neg, evenToNeg_ι, neg_neg]
