[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]


[GOAL]
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ charpoly (↑(leftMulMatrix h.basis) h.gen) = minpoly R h.gen
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ charpoly (↑(leftMulMatrix h.basis) h.gen) = minpoly R h.gen
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case inr
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ charpoly (↑(leftMulMatrix h.basis) h.gen) = minpoly R h.gen
[PROOFSTEP]
apply minpoly.unique' R h.gen (charpoly_monic _)
[GOAL]
case inr.hp
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ↑(aeval h.gen) (charpoly (↑(leftMulMatrix h.basis) h.gen)) = 0
[PROOFSTEP]
apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp (leftMulMatrix_injective h.basis)
[GOAL]
case inr.hp.a
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ↑(leftMulMatrix h.basis) (↑(aeval h.gen) (charpoly (↑(leftMulMatrix h.basis) h.gen))) = 0
[PROOFSTEP]
rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ∀ (q : R[X]), degree q < degree (charpoly (↑(leftMulMatrix h.basis) h.gen)) → q = 0 ∨ ↑(aeval h.gen) q ≠ 0
[PROOFSTEP]
refine' fun q hq => or_iff_not_imp_left.2 fun h0 => _
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : degree q < degree (charpoly (↑(leftMulMatrix h.basis) h.gen))
h0 : ¬q = 0
⊢ ↑(aeval h.gen) q ≠ 0
[PROOFSTEP]
rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : degree q < ↑h.dim
h0 : ¬q = 0
⊢ ↑(aeval h.gen) q ≠ 0
[PROOFSTEP]
contrapose! hq
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : ↑(aeval h.gen) q = 0
⊢ ↑h.dim ≤ degree q
[PROOFSTEP]
exact h.dim_le_degree_of_root h0 hq


[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i : n
⊢ charmatrix M i i = X - ↑C (M i i)
[PROOFSTEP]
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply_eq, map_apply]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : i ≠ j
⊢ charmatrix M i j = -↑C (M i j)
[PROOFSTEP]
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply_ne _ _ _ h, map_apply, sub_eq_neg_self]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ↑matPolyEquiv (charmatrix M) = X - ↑C M
[PROOFSTEP]
ext k i j
[GOAL]
case a.a.h
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (charmatrix M)) k i j = coeff (X - ↑C M) k i j
[PROOFSTEP]
simp only [matPolyEquiv_coeff_apply, coeff_sub, Pi.sub_apply]
[GOAL]
case a.a.h
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
[PROOFSTEP]
subst h
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff (charmatrix M i i) k = (coeff X k - coeff (↑C M) k) i i
[PROOFSTEP]
rw [charmatrix_apply_eq, coeff_sub]
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff X k - coeff (↑C (M i i)) k = (coeff X k - coeff (↑C M) k) i i
[PROOFSTEP]
simp only [coeff_X, coeff_C]
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i i
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : 1 = k
h✝ : k = 0
⊢ 1 - M i i = (1 - M) i i
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : 1 = k
h✝ : ¬k = 0
⊢ 1 - 0 = (1 - 0) i i
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : ¬1 = k
h✝ : k = 0
⊢ 0 - M i i = (0 - M) i i
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : ¬1 = k
h✝ : ¬k = 0
⊢ 0 - 0 = (0 - 0) i i
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
[PROOFSTEP]
rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i j
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
h✝¹ : k = 0
h✝ : 1 = k
⊢ -M i j = (1 - M) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
h✝¹ : k = 0
h✝ : ¬1 = k
⊢ -M i j = (0 - M) i j
[PROOFSTEP]
simp [h]
[GOAL]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
h✝¹ : ¬k = 0
h✝ : 1 = k
⊢ -0 = (1 - 0) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
h✝¹ : ¬k = 0
h✝ : ¬1 = k
⊢ -0 = (0 - 0) i j
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ charmatrix (↑(reindex e e) M) = ↑(reindex e e) (charmatrix M)
[PROOFSTEP]
ext i j x
[GOAL]
case a.h.a
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
all_goals simp [h]
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ charpoly (↑(reindex e e) M) = charpoly M
[PROOFSTEP]
unfold Matrix.charpoly
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ det (charmatrix (↑(reindex e e) M)) = det (charmatrix M)
[PROOFSTEP]
rw [charmatrix_reindex, Matrix.det_reindex_self]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M := (adjugate_mul _).symm
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : charpoly M • 1 = adjugate (charmatrix M) * charmatrix M
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
apply_fun matPolyEquiv at h
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : ↑matPolyEquiv (charpoly M • 1) = ↑matPolyEquiv (adjugate (charmatrix M) * charmatrix M)
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
simp only [matPolyEquiv.map_mul, matPolyEquiv_charmatrix] at h
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : ↑matPolyEquiv (charpoly M • 1) = ↑matPolyEquiv (adjugate (charmatrix M)) * (X - ↑C M)
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
apply_fun fun p => p.eval M at h
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (↑matPolyEquiv (charpoly M • 1)) = eval M (↑matPolyEquiv (adjugate (charmatrix M)) * (X - ↑C M))
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
rw [eval_mul_X_sub_C] at h
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (↑matPolyEquiv (charpoly M • 1)) = 0
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
rw [matPolyEquiv_smul_one, eval_map] at h
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M (charpoly M) = 0
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
exact h


[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (map f g) =
    kroneckerMap (fun x x_1 => x * x_1) (↑(toMatrix bM bM') f) (↑(toMatrix bN bN') g)
[PROOFSTEP]
ext ⟨i, j⟩ ⟨i', j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (map f g) (i, j) (i', j') =
    kroneckerMap (fun x x_1 => x * x_1) (↑(toMatrix bM bM') f) (↑(toMatrix bN bN') g) (i, j) (i', j')
[PROOFSTEP]
simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply, TensorProduct.map_tmul,
  Basis.tensorProduct_repr_tmul_apply]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
⊢ ↑(toLin (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (kroneckerMap (fun x x_1 => x * x_1) A B) =
    TensorProduct.map (↑(toLin bM bM') A) (↑(toLin bN bN') B)
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin, toMatrix_toLin]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bN bM)) ↑(TensorProduct.comm R M N) =
    submatrix 1 Prod.swap _root_.id
[PROOFSTEP]
ext ⟨i, j⟩ ⟨i', j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : κ
j i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bN bM)) ↑(TensorProduct.comm R M N) (i, j) (i', j') =
    submatrix 1 Prod.swap _root_.id (i, j) (i', j')
[PROOFSTEP]
simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul,
  Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Prod.swap_prod_mk, id.def, Basis.repr_self_apply,
  Matrix.one_apply, Prod.ext_iff, ite_and, @eq_comm _ i', @eq_comm _ j']
[GOAL]
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : κ
j i' : ι
j' : κ
⊢ ((if i = j' then 1 else 0) * if j = i' then 1 else 0) = if j = i' then if i = j' then 1 else 0 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : κ
j i' : ι
j' : κ
h✝¹ : i = j'
h✝ : j = i'
⊢ 1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : κ
j i' : ι
j' : κ
h✝¹ : i = j'
h✝ : ¬j = i'
⊢ 1 * 0 = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : κ
j i' : ι
j' : κ
h✝¹ : ¬i = j'
h✝ : j = i'
⊢ 0 * 1 = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : κ
j i' : ι
j' : κ
h✝¹ : ¬i = j'
h✝ : ¬j = i'
⊢ 0 * 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
⊢ ↑(toMatrix (Basis.tensorProduct (Basis.tensorProduct bM bN) bP) (Basis.tensorProduct bM (Basis.tensorProduct bN bP)))
      ↑(TensorProduct.assoc R M N P) =
    submatrix 1 _root_.id ↑(Equiv.prodAssoc ι κ τ)
[PROOFSTEP]
ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
[GOAL]
case a.mk.mk.h.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct (Basis.tensorProduct bM bN) bP) (Basis.tensorProduct bM (Basis.tensorProduct bN bP)))
      ↑(TensorProduct.assoc R M N P) (i, j, k) ((i', j'), k') =
    submatrix 1 _root_.id ↑(Equiv.prodAssoc ι κ τ) (i, j, k) ((i', j'), k')
[PROOFSTEP]
simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.assoc_tmul,
  Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Equiv.prodAssoc_apply, id.def, Basis.repr_self_apply,
  Matrix.one_apply, Prod.ext_iff, ite_and, @eq_comm _ i', @eq_comm _ j', @eq_comm _ k']
[GOAL]
case a.mk.mk.h.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
⊢ (if i = i' then 1 else 0) * ((if j = j' then 1 else 0) * if k = k' then 1 else 0) =
    if i = i' then if j = j' then if k = k' then 1 else 0 else 0 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : j = j'
h✝ : k = k'
⊢ 1 * (1 * 1) = 1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : j = j'
h✝ : ¬k = k'
⊢ 1 * (1 * 0) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : ¬j = j'
h✝ : k = k'
⊢ 1 * (0 * 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : ¬j = j'
h✝ : ¬k = k'
⊢ 1 * (0 * 0) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : j = j'
h✝ : k = k'
⊢ 0 * (1 * 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : j = j'
h✝ : ¬k = k'
⊢ 0 * (1 * 0) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : ¬j = j'
h✝ : k = k'
⊢ 0 * (0 * 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : ¬j = j'
h✝ : ¬k = k'
⊢ 0 * (0 * 0) = 0
[PROOFSTEP]
simp


[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ (Finsupp.sum (↑b₁.repr x) fun i xi =>
      Finsupp.sum (↑b₂.repr y) fun j yj => ↑ρ₁₂ xi • ↑σ₁₂ yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ↑(↑B x) y
[PROOFSTEP]
conv_rhs => rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ (Finsupp.sum (↑b₁.repr x) fun i xi =>
      Finsupp.sum (↑b₂.repr y) fun j yj => ↑ρ₁₂ xi • ↑σ₁₂ yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ↑(↑B (↑(Finsupp.total ι₁ M R ↑b₁) (↑b₁.repr x))) (↑(Finsupp.total ι₂ N S ↑b₂) (↑b₂.repr y))
[PROOFSTEP]
simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smulₛₗ₂, LinearMap.map_smulₛₗ]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
⊢ (Finsupp.sum (↑b₁'.repr x) fun i xi => Finsupp.sum (↑b₂'.repr y) fun j yj => xi • yj • ↑(↑B (↑b₁' i)) (↑b₂' j)) =
    ↑(↑B x) y
[PROOFSTEP]
conv_rhs => rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
⊢ (Finsupp.sum (↑b₁'.repr x) fun i xi => Finsupp.sum (↑b₂'.repr y) fun j yj => xi • yj • ↑(↑B (↑b₁' i)) (↑b₂' j)) =
    ↑(↑B (↑(Finsupp.total ι₁ Mₗ R ↑b₁') (↑b₁'.repr x))) (↑(Finsupp.total ι₂ Nₗ R ↑b₂') (↑b₂'.repr y))
[PROOFSTEP]
simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smul₂, LinearMap.map_smul]


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ RTendsto' r l (𝓝 a) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → Rel.preimage r s ∈ l
[PROOFSTEP]
rw [rtendsto'_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ (∀ (s : Set α), s ∈ 𝓝 a → Rel.preimage r s ∈ l) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → Rel.preimage r s ∈ l
[PROOFSTEP]
apply all_mem_nhds_filter
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : Rel β α
l : Filter β
a : α
⊢ ∀ (s t : Set α), s ⊆ t → Rel.preimage r s ⊆ Rel.preimage r t
[PROOFSTEP]
apply Rel.preimage_mono
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.Dom f)
[PROOFSTEP]
rw [← PFun.preimage_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.preimage f Set.univ)
[PROOFSTEP]
exact h _ isOpen_univ
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f ↔ ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ PContinuous f → ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
[PROOFSTEP]
intro h x y h'
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
x : α
y : β
h' : y ∈ f x
⊢ PTendsto' f (𝓝 x) (𝓝 y)
[PROOFSTEP]
simp only [ptendsto'_def, mem_nhds_iff]
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
x : α
y : β
h' : y ∈ f x
⊢ ∀ (s : Set β), (∃ t, t ⊆ s ∧ IsOpen t ∧ y ∈ t) → ∃ t, t ⊆ PFun.preimage f s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rintro s ⟨t, tsubs, opent, yt⟩
[GOAL]
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
x : α
y : β
h' : y ∈ f x
s t : Set β
tsubs : t ⊆ s
opent : IsOpen t
yt : y ∈ t
⊢ ∃ t, t ⊆ PFun.preimage f s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
exact ⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
⊢ (∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f
[PROOFSTEP]
intro hf s os
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
⊢ IsOpen (PFun.preimage f s)
[PROOFSTEP]
rw [isOpen_iff_nhds]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
⊢ ∀ (a : α), a ∈ PFun.preimage f s → 𝓝 a ≤ 𝓟 (PFun.preimage f s)
[PROOFSTEP]
rintro x ⟨y, ys, fxy⟩ t
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
⊢ t ∈ 𝓟 (PFun.preimage f s) → t ∈ 𝓝 x
[PROOFSTEP]
rw [mem_principal]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
⊢ PFun.preimage f s ⊆ t → t ∈ 𝓝 x
[PROOFSTEP]
intro (h : f.preimage s ⊆ t)
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ t ∈ 𝓝 x
[PROOFSTEP]
change t ∈ 𝓝 x
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ t ∈ 𝓝 x
[PROOFSTEP]
apply mem_of_superset _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x := by
  intro s hs
  have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
  rw [ptendsto'_def] at this
  exact this s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
⊢ ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set β
os : IsOpen s✝
x : α
y : β
ys : y ∈ s✝
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s✝ ⊆ t
s : Set β
hs : s ∈ 𝓝 y
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set β
os : IsOpen s✝
x : α
y : β
ys : y ∈ s✝
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s✝ ⊆ t
s : Set β
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
rw [ptendsto'_def] at this
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set β
os : IsOpen s✝
x : α
y : β
ys : y ∈ s✝
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s✝ ⊆ t
s : Set β
hs : s ∈ 𝓝 y
this : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
exact this s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
show f.preimage s ∈ 𝓝 x
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ PFun.preimage f s ∈ 𝓝 x
[PROOFSTEP]
apply h'
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ s ∈ 𝓝 y
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
hf : ∀ {x : α} {y : β}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set β
os : IsOpen s
x : α
y : β
ys : y ∈ s
fxy : y ∈ f x
t : Set α
h : PFun.preimage f s ⊆ t
h' : ∀ (s : Set β), s ∈ 𝓝 y → PFun.preimage f s ∈ 𝓝 x
⊢ ∃ t, t ⊆ s ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
exact ⟨s, Set.Subset.refl _, os, ys⟩