[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ eigenvectorMatrix hA * eigenvectorMatrixInv hA = 1
[PROOFSTEP]
apply Basis.toMatrix_mul_toMatrix_flip
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ eigenvectorMatrix hA i j = ↑(eigenvectorBasis hA) j i
[PROOFSTEP]
simp_rw [eigenvectorMatrix, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis, PiLp.basisFun_repr]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ eigenvectorMatrixInv hA i j = star (↑(eigenvectorBasis hA) i j)
[PROOFSTEP]
rw [eigenvectorMatrixInv, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
  OrthonormalBasis.repr_apply_apply, PiLp.basisFun_apply, PiLp.equiv_symm_single, EuclideanSpace.inner_single_right,
  one_mul, IsROrC.star_def]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ (eigenvectorMatrixInv hA)ᴴ = eigenvectorMatrix hA
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ (eigenvectorMatrixInv hA)ᴴ i j = eigenvectorMatrix hA i j
[PROOFSTEP]
rw [conjTranspose_apply, eigenvectorMatrixInv_apply, eigenvectorMatrix_apply, star_star]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ (eigenvectorMatrix hA)ᴴ = eigenvectorMatrixInv hA
[PROOFSTEP]
rw [← conjTranspose_eigenvectorMatrixInv, conjTranspose_conjTranspose]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ eigenvectorMatrixInv hA * A = diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA
[PROOFSTEP]
rw [eigenvectorMatrixInv, PiLp.basis_toMatrix_basisFun_mul]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ (↑of fun i j =>
      ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i) =
    diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
      Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ ↑of (fun i j => ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i)
      i j =
    (diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
        Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n))
      i j
[PROOFSTEP]
have := isHermitian_iff_isSymmetric.1 hA
[GOAL]
case a.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑of (fun i j => ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i)
      i j =
    (diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
        Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n))
      i j
[PROOFSTEP]
convert
  this.eigenvectorBasis_apply_self_apply finrank_euclideanSpace (EuclideanSpace.single j 1)
    ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm i) using
  1
[GOAL]
case h.e'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑of (fun i j => ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i)
      i j =
    ↑(LinearMap.IsSymmetric.eigenvectorBasis this
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(↑toEuclideanLin A) (EuclideanSpace.single j 1))
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
dsimp only [EuclideanSpace.single, toEuclideanLin_piLp_equiv_symm, toLin'_apply, Matrix.of_apply,
  IsHermitian.eigenvectorBasis]
[GOAL]
case h.e'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑(↑(OrthonormalBasis.toBasis
                (OrthonormalBasis.reindex
                  (LinearMap.IsSymmetric.eigenvectorBasis (_ : LinearMap.IsSymmetric (↑toEuclideanLin A))
                    (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n))
                  (Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)))).repr
          (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j)))
      i =
    ↑(LinearMap.IsSymmetric.eigenvectorBasis this
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(PiLp.equiv 2 fun i => 𝕜).symm (mulVec A (Pi.single j 1)))
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
simp_rw [mulVec_single, mul_one, OrthonormalBasis.coe_toBasis_repr_apply, OrthonormalBasis.repr_reindex]
[GOAL]
case h.e'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑(LinearMap.IsSymmetric.eigenvectorBasis (_ : LinearMap.IsSymmetric (↑toEuclideanLin A))
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i) =
    ↑(LinearMap.IsSymmetric.eigenvectorBasis this
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(PiLp.equiv 2 fun i => 𝕜).symm fun i => A i j)
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ (diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
        Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n))
      i j =
    ↑(LinearMap.IsSymmetric.eigenvalues this (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)
          (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)) *
      ↑(LinearMap.IsSymmetric.eigenvectorBasis this
              (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
        (EuclideanSpace.single j 1)
        (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
simp only [diagonal_mul, (· ∘ ·), eigenvalues]
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑(eigenvalues₀ hA (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)) *
      Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) (↑(PiLp.basisFun 2 𝕜 n)) i j =
    ↑(LinearMap.IsSymmetric.eigenvalues this (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)
          (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)) *
      ↑(LinearMap.IsSymmetric.eigenvectorBasis this
              (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
        (EuclideanSpace.single j 1)
        (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
rw [eigenvectorBasis, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply, OrthonormalBasis.repr_reindex,
  eigenvalues₀, PiLp.basisFun_apply, PiLp.equiv_symm_single]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
have := hA.spectral_theorem
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this : eigenvectorMatrixInv hA * A = diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
rw [← @Matrix.mul_inv_eq_iff_eq_mul_of_invertible (A := hA.eigenvectorMatrixInv)] at this
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this : eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹ = diagonal (IsROrC.ofReal ∘ eigenvalues hA)
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
have := congr_arg IsROrC.re (congr_fun (congr_fun this i) i)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this✝ : eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹ = diagonal (IsROrC.ofReal ∘ eigenvalues hA)
this :
  ↑IsROrC.re ((eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹) i i) =
    ↑IsROrC.re (diagonal (IsROrC.ofReal ∘ eigenvalues hA) i i)
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
rw [diagonal_apply_eq, Function.comp_apply, IsROrC.ofReal_re, inv_eq_left_inv hA.eigenvectorMatrix_mul_inv, ←
  conjTranspose_eigenvectorMatrix, mul_mul_apply] at this
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this✝ : eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹ = diagonal (IsROrC.ofReal ∘ eigenvalues hA)
this : ↑IsROrC.re ((eigenvectorMatrix hA)ᴴ i ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i)) = eigenvalues hA i
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
exact this.symm
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ det A = ∏ i : n, ↑(eigenvalues hA i)
[PROOFSTEP]
apply mul_left_cancel₀ (det_ne_zero_of_left_inverse (eigenvectorMatrix_mul_inv hA))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ det (eigenvectorMatrixInv hA) * det A = det (eigenvectorMatrixInv hA) * ∏ i : n, ↑(eigenvalues hA i)
[PROOFSTEP]
rw [← det_mul, spectral_theorem, det_mul, mul_comm, det_diagonal]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ det (eigenvectorMatrixInv hA) * ∏ i : n, (IsROrC.ofReal ∘ eigenvalues hA) i =
    det (eigenvectorMatrixInv hA) * ∏ i : n, ↑(eigenvalues hA i)
[PROOFSTEP]
simp_rw [Function.comp_apply]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ A = eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA
[PROOFSTEP]
simpa [← Matrix.mul_assoc, hA.eigenvectorMatrix_mul_inv, Matrix.one_mul] using
  congr_arg (hA.eigenvectorMatrix * ·) hA.spectral_theorem
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ rank A = rank (diagonal (eigenvalues hA))
[PROOFSTEP]
conv_lhs => rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
| rank A
[PROOFSTEP]
rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
| rank A
[PROOFSTEP]
rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
| rank A
[PROOFSTEP]
rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ rank (eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA) =
    rank (diagonal (eigenvalues hA))
[PROOFSTEP]
have hE := isUnit_det_of_invertible (hA.eigenvectorMatrix)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
hE : IsUnit (det (eigenvectorMatrix hA))
⊢ rank (eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA) =
    rank (diagonal (eigenvalues hA))
[PROOFSTEP]
have hiE := isUnit_det_of_invertible (hA.eigenvectorMatrixInv)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
hE : IsUnit (det (eigenvectorMatrix hA))
hiE : IsUnit (det (eigenvectorMatrixInv hA))
⊢ rank (eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA) =
    rank (diagonal (eigenvalues hA))
[PROOFSTEP]
simp only [rank_mul_eq_right_of_isUnit_det hA.eigenvectorMatrix _ hE,
  rank_mul_eq_left_of_isUnit_det hA.eigenvectorMatrixInv _ hiE, rank_diagonal, Function.comp_apply, ne_eq,
  algebraMap.lift_map_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ rank A = Fintype.card { i // eigenvalues hA i ≠ 0 }
[PROOFSTEP]
rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]


[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case inl
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ False
[PROOFSTEP]
exact hμ (Submodule.eq_bot_of_subsingleton _)
[GOAL]
case inr
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector
[GOAL]
case inr.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz : v ≠ 0
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
obtain ⟨i, -, h_i⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty (fun i => ‖v i‖)
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
have h_nz : v i ≠ 0 := by
  contrapose! h_nz
  ext j
  rw [Pi.zero_apply, ← norm_le_zero_iff]
  refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
  exact norm_le_zero_iff.mpr h_nz
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
⊢ v i ≠ 0
[PROOFSTEP]
contrapose! h_nz
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
⊢ v = 0
[PROOFSTEP]
ext j
[GOAL]
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ v j = OfNat.ofNat 0 j
[PROOFSTEP]
rw [Pi.zero_apply, ← norm_le_zero_iff]
[GOAL]
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v j‖ ≤ 0
[PROOFSTEP]
refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
[GOAL]
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v i‖ ≤ 0
[PROOFSTEP]
exact norm_le_zero_iff.mpr h_nz
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
have h_le : ∀ j, ‖v j * (v i)⁻¹‖ ≤ 1 := fun j =>
  by
  rw [norm_mul, norm_inv, mul_inv_le_iff' (norm_pos_iff.mpr h_nz), one_mul]
  exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j * (v i)⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_mul, norm_inv, mul_inv_le_iff' (norm_pos_iff.mpr h_nz), one_mul]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j‖ ≤ ‖v i‖
[PROOFSTEP]
exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
simp_rw [mem_closedBall_iff_norm']
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ k, ‖A k k - μ‖ ≤ ∑ j in Finset.erase Finset.univ k, ‖A k j‖
[PROOFSTEP]
refine ⟨i, ?_⟩
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ ≤ ∑ j in Finset.erase Finset.univ i, ‖A i j‖
[PROOFSTEP]
calc
  _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field_simp [h_nz]; ring
  _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
    rw [show μ * v i = ∑ x : n, A i x * v x
        by
        rw [← Matrix.dotProduct, ← Matrix.mulVec]
        exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
  _ = ‖(∑ j in Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
    rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
  _ ≤ ∑ j in Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ :=
    by
    rw [Finset.sum_mul]
    exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
  _ ≤ ∑ j in Finset.univ.erase i, ‖A i j‖ :=
    (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
[PROOFSTEP]
congr
[GOAL]
case e_a
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ A i i - μ = (A i i * v i - μ * v i) * (v i)⁻¹
[PROOFSTEP]
field_simp [h_nz]
[GOAL]
case e_a
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ (A i i - μ) * v i = A i i * v i - μ * v i
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
[PROOFSTEP]
rw [show μ * v i = ∑ x : n, A i x * v x by
    rw [← Matrix.dotProduct, ← Matrix.mulVec]
    exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ μ * v i = ∑ x : n, A i x * v x
[PROOFSTEP]
rw [← Matrix.dotProduct, ← Matrix.mulVec]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ μ * v i = Matrix.mulVec A (fun x => v x) i
[PROOFSTEP]
exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j in Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
[PROOFSTEP]
rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(∑ j in Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖ ≤
    ∑ j in Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
[PROOFSTEP]
rw [Finset.sum_mul]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖∑ x in Finset.erase Finset.univ i, A i x * v x * (v i)⁻¹‖ ≤
    ∑ j in Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
[PROOFSTEP]
exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∑ i_1 in Finset.erase Finset.univ i, ‖A i i_1 * v i_1 * (v i)⁻¹‖ =
    ∑ j in Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
[PROOFSTEP]
simp_rw [mul_assoc, norm_mul]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ j in Finset.erase Finset.univ k, ‖A k j‖ < ‖A k k‖
⊢ Matrix.det A ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ∃ k, ‖A k k‖ ≤ ∑ j in Finset.erase Finset.univ k, ‖A k j‖
[PROOFSTEP]
suffices ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.univ.erase k, ‖A k j‖) by
  exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h )
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
this : ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ k, ‖A k k‖ ≤ ∑ j in Finset.erase Finset.univ k, ‖A k j‖
[PROOFSTEP]
exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h )
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h✝ : Matrix.det A = 0
this : ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
a : n
h : 0 ∈ Metric.closedBall (A a a) (∑ j in Finset.erase Finset.univ a, ‖A a j‖)
⊢ ‖A a a‖ ≤ ∑ j in Finset.erase Finset.univ a, ‖A a j‖
[PROOFSTEP]
rwa [mem_closedBall_iff_norm', sub_zero] at h
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
refine eigenvalue_mem_ball ?_
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ Module.End.HasEigenvalue (↑Matrix.toLin' fun k => A k) 0
[PROOFSTEP]
rw [Module.End.HasEigenvalue, Module.End.eigenspace_zero, ne_comm]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ⊥ ≠ LinearMap.ker (↑Matrix.toLin' fun k => A k)
[PROOFSTEP]
exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ↑LinearMap.det (↑Matrix.toLin' fun k => A k) = 0
[PROOFSTEP]
rwa [LinearMap.det_toLin']
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ Matrix.det A ≠ 0
[PROOFSTEP]
rw [← Matrix.det_transpose]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ Matrix.det (Matrix.transpose A) ≠ 0
[PROOFSTEP]
exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ j in Finset.erase Finset.univ k, ‖Matrix.transpose A k j‖ < ‖Matrix.transpose A k k‖
[PROOFSTEP]
simp_rw [Matrix.transpose_apply]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ x in Finset.erase Finset.univ k, ‖A x k‖ < ‖A k k‖
[PROOFSTEP]
exact h


[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ℕ
m : M
⊢ ↑(ι Q) m * ↑(ι Q) m = ↑(algebraMap R (CliffordAlgebra Q)) (↑Q m)
[PROOFSTEP]
erw [← AlgHom.map_mul, RingQuot.mkAlgHom_rel R (Rel.of m), AlgHom.commutes]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ℕ
m : M
⊢ ↑(algebraMap R (RingQuot (Rel Q))) (↑Q m) = ↑(algebraMap R (CliffordAlgebra Q)) (↑Q m)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ ↑g (↑(ι Q) m) * ↑g (↑(ι Q) m) = ↑(algebraMap R A) (↑Q m)
[PROOFSTEP]
rw [← AlgHom.map_mul, ι_sq_scalar, AlgHom.commutes]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
x y : TensorAlgebra R M
h : Rel Q x y
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y
[PROOFSTEP]
induction h
[GOAL]
case of
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
x y : TensorAlgebra R M
m✝ : M
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) (↑(TensorAlgebra.ι R) m✝ * ↑(TensorAlgebra.ι R) m✝) =
    ↑(↑(TensorAlgebra.lift R) ↑f) (↑(algebraMap R (TensorAlgebra R M)) (↑Q m✝))
[PROOFSTEP]
rw [AlgHom.commutes, AlgHom.map_mul, TensorAlgebra.lift_ι_apply, f.prop]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
    ↑(algebraMap R A) (↑Q m)
[PROOFSTEP]
rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
⊢ (fun F =>
        { val := LinearMap.comp (AlgHom.toLinearMap F) (ι Q),
          property :=
            (_ :
              ∀ (m : M),
                ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
                  ↑(algebraMap R A) (↑Q m)) })
      ((fun f =>
          ↑(RingQuot.liftAlgHom R)
            { val := ↑(TensorAlgebra.lift R) ↑f,
              property :=
                (_ :
                  ∀ (x y : TensorAlgebra R M),
                    Rel Q x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y) })
        f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case a.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
x : M
⊢ ↑↑((fun F =>
              { val := LinearMap.comp (AlgHom.toLinearMap F) (ι Q),
                property :=
                  (_ :
                    ∀ (m : M),
                      ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m *
                          ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
                        ↑(algebraMap R A) (↑Q m)) })
            ((fun f =>
                ↑(RingQuot.liftAlgHom R)
                  { val := ↑(TensorAlgebra.lift R) ↑f,
                    property :=
                      (_ :
                        ∀ (x y : TensorAlgebra R M),
                          Rel Q x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y) })
              f))
      x =
    ↑↑f x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
x : M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp
              ((fun f =>
                  ↑(RingQuot.liftAlgHom R)
                    { val := ↑(TensorAlgebra.lift R) ↑f,
                      property :=
                        (_ :
                          ∀ (x y : TensorAlgebra R M),
                            Rel Q x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y) })
                ((fun F =>
                    { val := LinearMap.comp (AlgHom.toLinearMap F) (ι Q),
                      property :=
                        (_ :
                          ∀ (m : M),
                            ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m *
                                ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
                              ↑(algebraMap R A) (↑Q m)) })
                  F))
              (RingQuot.mkAlgHom R fun x y => Rel Q x y)))
          (TensorAlgebra.ι R))
      x =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp F (RingQuot.mkAlgHom R fun x y => Rel Q x y)))
          (TensorAlgebra.ι R))
      x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ _)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι Q) = f ↔ g = ↑(lift Q) { val := f, property := cond }
[PROOFSTEP]
convert (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq
[GOAL]
case h.e'_1.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι Q) = f ↔ ↑(lift Q).symm g = { val := f, property := cond }
[PROOFSTEP]
rw [lift_symm_apply, Subtype.mk_eq_mk]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ ↑(lift Q)
      { val := LinearMap.comp (AlgHom.toLinearMap g) (ι Q),
        property := (_ : ∀ (m : M), ↑g (↑(ι Q) m) * ↑g (↑(ι Q) m) = ↑(algebraMap R A) (↑Q m)) } =
    g
[PROOFSTEP]
exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q) → f = g
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q)
⊢ f = g
[PROOFSTEP]
apply (lift Q).symm.injective
[GOAL]
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q)
⊢ ↑(lift Q).symm f = ↑(lift Q).symm g
[PROOFSTEP]
rw [lift_symm_apply, lift_symm_apply]
[GOAL]
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q)
⊢ { val := LinearMap.comp (AlgHom.toLinearMap f) (ι Q),
      property :=
        (_ :
          ∀ (m : M),
            ↑(LinearMap.comp (AlgHom.toLinearMap f) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap f) (ι Q)) m =
              ↑(algebraMap R A) (↑Q m)) } =
    { val := LinearMap.comp (AlgHom.toLinearMap g) (ι Q),
      property :=
        (_ :
          ∀ (m : M),
            ↑(LinearMap.comp (AlgHom.toLinearMap g) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap g) (ι Q)) m =
              ↑(algebraMap R A) (↑Q m)) }
[PROOFSTEP]
simp only [h]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
⊢ C a
[PROOFSTEP]
let s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C
    mul_mem' := @h_mul
    add_mem' := @h_add
    algebraMap_mem' := h_grade0 }
    -- porting note: Added `h`. `h` is needed for `of`.
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
⊢ C a
[PROOFSTEP]
letI h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
⊢ C a
[PROOFSTEP]
let of : { f : M →ₗ[R] s // ∀ m, f m * f m = algebraMap _ _ (Q m) } :=
  ⟨(ι Q).codRestrict (Subalgebra.toSubmodule s) h_grade1, fun m => Subtype.eq <| ι_sq_scalar Q m⟩
    -- the mapping through the subalgebra is the identity
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
⊢ C a
[PROOFSTEP]
have of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp (lift Q of) :=
  by
  ext
  simp
    -- porting note: `simp` can't apply this
  erw [LinearMap.codRestrict_apply]
    -- finding a proof is finding an element of the subalgebra
      -- porting note: was `convert Subtype.prop (lift Q of a); exact AlgHom.congr_fun of_id a`
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
⊢ AlgHom.id R (CliffordAlgebra Q) = AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q))) (ι Q)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (Subalgebra.val s) (↑(lift Q) of))) (ι Q)) x✝
[PROOFSTEP]
simp
  -- porting note: `simp` can't apply this
[GOAL]
case a.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
x✝ : M
⊢ ↑(ι Q) x✝ = ↑(↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) x✝)
[PROOFSTEP]
erw [LinearMap.codRestrict_apply]
  -- finding a proof is finding an element of the subalgebra
    -- porting note: was `convert Subtype.prop (lift Q of a); exact AlgHom.congr_fun of_id a`
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
of_id : AlgHom.id R (CliffordAlgebra Q) = AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)
⊢ C a
[PROOFSTEP]
rw [← AlgHom.id_apply (R := R) a, of_id]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
of_id : AlgHom.id R (CliffordAlgebra Q) = AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)
⊢ C (↑(AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)) a)
[PROOFSTEP]
exact Subtype.prop (lift Q of a)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) a =
    ↑(ι Q) (a + b) * ↑(ι Q) (a + b) - ↑(ι Q) a * ↑(ι Q) a - ↑(ι Q) b * ↑(ι Q) b
[PROOFSTEP]
rw [(ι Q).map_add, mul_add, add_mul, add_mul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) a =
    ↑(ι Q) a * ↑(ι Q) a + ↑(ι Q) b * ↑(ι Q) a + (↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) b) - ↑(ι Q) a * ↑(ι Q) a -
      ↑(ι Q) b * ↑(ι Q) b
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) a =
    ↑(ι Q) a * ↑(ι Q) a + ↑(ι Q) b * ↑(ι Q) a + (↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) b) - ↑(ι Q) a * ↑(ι Q) a -
      ↑(ι Q) b * ↑(ι Q) b
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) (a + b) * ↑(ι Q) (a + b) - ↑(ι Q) a * ↑(ι Q) a - ↑(ι Q) b * ↑(ι Q) b =
    ↑(algebraMap R (CliffordAlgebra Q)) (↑Q (a + b)) - ↑(algebraMap R (CliffordAlgebra Q)) (↑Q a) -
      ↑(algebraMap R (CliffordAlgebra Q)) (↑Q b)
[PROOFSTEP]
rw [ι_sq_scalar, ι_sq_scalar, ι_sq_scalar]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(algebraMap R (CliffordAlgebra Q)) (↑Q (a + b)) - ↑(algebraMap R (CliffordAlgebra Q)) (↑Q a) -
      ↑(algebraMap R (CliffordAlgebra Q)) (↑Q b) =
    ↑(algebraMap R (CliffordAlgebra Q)) (↑Q (a + b) - ↑Q a - ↑Q b)
[PROOFSTEP]
rw [← RingHom.map_sub, ← RingHom.map_sub]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b * ↑(ι Q) a = ↑(ι Q) (QuadraticForm.polar (↑Q) a b • a - ↑Q a • b)
[PROOFSTEP]
rw [ι_mul_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ← Algebra.smul_def, ← map_smul,
  ← map_smul, ← map_sub]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m)
⊢ Submodule.map (AlgHom.toLinearMap (↑(lift Q) { val := f, property := cond })) (LinearMap.range (ι Q)) =
    LinearMap.range f
[PROOFSTEP]
rw [← LinearMap.range_comp, ι_comp_lift]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ map Q₁ Q₁ LinearMap.id (_ : ∀ (m : M₁), ↑Q₁ (↑LinearMap.id m) = ↑Q₁ (↑LinearMap.id m)) =
    AlgHom.id R (CliffordAlgebra Q₁)
[PROOFSTEP]
ext m
[GOAL]
case a.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
m : M₁
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap (map Q₁ Q₁ LinearMap.id (_ : ∀ (m : M₁), ↑Q₁ (↑LinearMap.id m) = ↑Q₁ (↑LinearMap.id m))))
          (ι Q₁))
      m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q₁))) (ι Q₁)) m
[PROOFSTEP]
exact map_apply_ι _ _ _ _ m
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : M₂ →ₗ[R] M₃
hf : ∀ (m : M₂), ↑Q₃ (↑f m) = ↑Q₂ m
g : M₁ →ₗ[R] M₂
hg : ∀ (m : M₁), ↑Q₂ (↑g m) = ↑Q₁ m
⊢ AlgHom.comp (map Q₂ Q₃ f hf) (map Q₁ Q₂ g hg) =
    map Q₁ Q₃ (LinearMap.comp f g) (_ : ∀ (m : M₁), ↑Q₃ (↑f (↑g m)) = ↑Q₁ m)
[PROOFSTEP]
ext m
[GOAL]
case a.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : M₂ →ₗ[R] M₃
hf : ∀ (m : M₂), ↑Q₃ (↑f m) = ↑Q₂ m
g : M₁ →ₗ[R] M₂
hg : ∀ (m : M₁), ↑Q₂ (↑g m) = ↑Q₁ m
m : M₁
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (map Q₂ Q₃ f hf) (map Q₁ Q₂ g hg))) (ι Q₁)) m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (map Q₁ Q₃ (LinearMap.comp f g) (_ : ∀ (m : M₁), ↑Q₃ (↑f (↑g m)) = ↑Q₁ m)))
          (ι Q₁))
      m
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]
[GOAL]
case a.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : M₂ →ₗ[R] M₃
hf : ∀ (m : M₂), ↑Q₃ (↑f m) = ↑Q₂ m
g : M₁ →ₗ[R] M₂
hg : ∀ (m : M₁), ↑Q₂ (↑g m) = ↑Q₁ m
m : M₁
⊢ ↑(map Q₂ Q₃ f hf) (↑(map Q₁ Q₂ g hg) (↑(ι Q₁) m)) =
    ↑(map Q₁ Q₃ (LinearMap.comp f g) (_ : ∀ (m : M₁), ↑Q₃ (↑f (↑g m)) = ↑Q₁ m)) (↑(ι Q₁) m)
[PROOFSTEP]
rw [map_apply_ι, map_apply_ι, map_apply_ι, LinearMap.comp_apply]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ map Q₂ Q₂ (LinearMap.comp ↑↑e ↑↑(QuadraticForm.IsometryEquiv.symm e))
      (_ : ∀ (m : M₂), ↑Q₂ (↑↑↑e (↑↑↑(QuadraticForm.IsometryEquiv.symm e) m)) = ↑Q₂ m) =
    AlgHom.id R (CliffordAlgebra Q₂)
[PROOFSTEP]
convert map_id Q₂ using 2
  -- porting note: replaced `_` with `Q₂`
[GOAL]
case h.e'_2.h.e'_11
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ LinearMap.comp ↑↑e ↑↑(QuadraticForm.IsometryEquiv.symm e) = LinearMap.id
[PROOFSTEP]
ext m
[GOAL]
case h.e'_2.h.e'_11.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
m : M₂
⊢ ↑(LinearMap.comp ↑↑e ↑↑(QuadraticForm.IsometryEquiv.symm e)) m = ↑LinearMap.id m
[PROOFSTEP]
exact e.toLinearEquiv.apply_symm_apply m
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ map Q₁ Q₁ (LinearMap.comp ↑↑(QuadraticForm.IsometryEquiv.symm e) ↑↑e)
      (_ : ∀ (m : M₁), ↑Q₁ (↑↑↑(QuadraticForm.IsometryEquiv.symm e) (↑↑↑e m)) = ↑Q₁ m) =
    AlgHom.id R (CliffordAlgebra Q₁)
[PROOFSTEP]
convert map_id Q₁ using 2
  -- porting note: replaced `_` with `Q₁`
[GOAL]
case h.e'_2.h.e'_11
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ LinearMap.comp ↑↑(QuadraticForm.IsometryEquiv.symm e) ↑↑e = LinearMap.id
[PROOFSTEP]
ext m
[GOAL]
case h.e'_2.h.e'_11.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
m : M₁
⊢ ↑(LinearMap.comp ↑↑(QuadraticForm.IsometryEquiv.symm e) ↑↑e) m = ↑LinearMap.id m
[PROOFSTEP]
exact e.toLinearEquiv.symm_apply_apply m
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticForm.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticForm.IsometryEquiv Q₂ Q₃
⊢ AlgEquiv.trans (equivOfIsometry e₁₂) (equivOfIsometry e₂₃) =
    equivOfIsometry (QuadraticForm.IsometryEquiv.trans e₁₂ e₂₃)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticForm.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticForm.IsometryEquiv Q₂ Q₃
x : CliffordAlgebra Q₁
⊢ ↑(AlgEquiv.trans (equivOfIsometry e₁₂) (equivOfIsometry e₂₃)) x =
    ↑(equivOfIsometry (QuadraticForm.IsometryEquiv.trans e₁₂ e₂₃)) x
[PROOFSTEP]
exact AlgHom.congr_fun (map_comp_map Q₁ Q₂ Q₃ _ _ _ _) x
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ equivOfIsometry (QuadraticForm.IsometryEquiv.refl Q₁) = AlgEquiv.refl
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
x : CliffordAlgebra Q₁
⊢ ↑(equivOfIsometry (QuadraticForm.IsometryEquiv.refl Q₁)) x = ↑AlgEquiv.refl x
[PROOFSTEP]
exact AlgHom.congr_fun (map_id Q₁) x
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
m : M
inst✝ : Invertible (↑Q m)
⊢ ↑(ι Q) (⅟(↑Q m) • m) * ↑(ι Q) m = 1
[PROOFSTEP]
rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
m : M
inst✝ : Invertible (↑Q m)
⊢ ↑(ι Q) m * ↑(ι Q) (⅟(↑Q m) • m) = 1
[PROOFSTEP]
rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
m : M
inst✝¹ : Invertible (↑Q m)
inst✝ : Invertible (↑(ι Q) m)
⊢ ⅟(↑(ι Q) m) = ↑(ι Q) (⅟(↑Q m) • m)
[PROOFSTEP]
letI := invertibleιOfInvertible Q m
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
m : M
inst✝¹ : Invertible (↑Q m)
inst✝ : Invertible (↑(ι Q) m)
this : Invertible (↑(ι Q) m) := invertibleιOfInvertible Q m
⊢ ⅟(↑(ι Q) m) = ↑(ι Q) (⅟(↑Q m) • m)
[PROOFSTEP]
convert (rfl : ⅟(ι Q m) = _)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
h : IsUnit (↑Q m)
⊢ IsUnit (↑(ι Q) m)
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
h : IsUnit (↑Q m)
val✝ : Invertible (↑Q m)
⊢ IsUnit (↑(ι Q) m)
[PROOFSTEP]
letI := invertibleιOfInvertible Q m
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
h : IsUnit (↑Q m)
val✝ : Invertible (↑Q m)
this : Invertible (↑(ι Q) m) := invertibleιOfInvertible Q m
⊢ IsUnit (↑(ι Q) m)
[PROOFSTEP]
exact isUnit_of_invertible (ι Q m)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
a b : M
inst✝¹ : Invertible (↑(ι Q) a)
inst✝ : Invertible (↑Q a)
⊢ ↑(ι Q) a * ↑(ι Q) b * ⅟(↑(ι Q) a) = ↑(ι Q) ((⅟(↑Q a) * QuadraticForm.polar (↑Q) a b) • a - b)
[PROOFSTEP]
rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul, invOf_mul_self,
  one_smul]
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
a b : M
inst✝¹ : Invertible (↑(ι Q) a)
inst✝ : Invertible (↑Q a)
⊢ ⅟(↑(ι Q) a) * ↑(ι Q) b * ↑(ι Q) a = ↑(ι Q) ((⅟(↑Q a) * QuadraticForm.polar (↑Q) a b) • a - b)
[PROOFSTEP]
rw [invOf_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
  invOf_mul_self, one_smul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ℕ
m : M
⊢ ↑toClifford (↑(ι R) m) = ↑(CliffordAlgebra.ι Q) m
[PROOFSTEP]
simp [toClifford]


[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ det (mvPolynomialX m m R) ≠ 0
[PROOFSTEP]
intro h_det
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
⊢ False
[PROOFSTEP]
have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
this : det (↑(RingHom.mapMatrix (MvPolynomial.eval fun p => OfNat.ofNat 1 p.fst p.snd)) (mvPolynomialX m m R)) = det 1
⊢ False
[PROOFSTEP]
rw [det_one, ← RingHom.map_det, h_det, RingHom.map_zero] at this
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
this : 0 = 1
⊢ False
[PROOFSTEP]
exact zero_ne_one this


[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ker (↑toLin' (diagonal w)) = ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
rw [← comap_bot, ← iInf_ker_proj, comap_iInf]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ⨅ (i : m), comap (↑toLin' (diagonal w)) (ker (proj i)) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
have := fun i : m => ker_comp (toLin' (diagonal w)) (proj i)
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
⊢ ⨅ (i : m), comap (↑toLin' (diagonal w)) (ker (proj i)) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
simp only [comap_iInf, ← this, proj_diagonal, ker_smul']
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
⊢ ⨅ (i : m) (_ : w i ≠ 0), ker (proj i) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
have : univ ⊆ {i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ := by rw [Set.union_compl_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
⊢ univ ⊆ {i | w i = 0} ∪ {i | w i = 0}ᶜ
[PROOFSTEP]
rw [Set.union_compl_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this✝ : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
this : univ ⊆ {i | w i = 0} ∪ {i | w i = 0}ᶜ
⊢ ⨅ (i : m) (_ : w i ≠ 0), ker (proj i) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
exact (iSup_range_stdBasis_eq_iInf_ker_proj K (fun _ : m => K) disjoint_compl_right this (Set.toFinite _)).symm
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (↑toLin' (diagonal w)) =
    ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
dsimp only [mem_setOf_eq]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (↑toLin' (diagonal w)) =
    ⨆ (i : m) (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
rw [← Submodule.map_top, ← iSup_range_stdBasis, Submodule.map_iSup]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ⨆ (i : m), Submodule.map (↑toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i)) =
    ⨆ (i : m) (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
congr
[GOAL]
case e_s
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i => Submodule.map (↑toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i))) = fun i =>
    ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
funext i
[GOAL]
case e_s.h
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
i : m
⊢ Submodule.map (↑toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i)) =
    ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
rw [← LinearMap.range_comp, diagonal_comp_stdBasis, ← range_smul']
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have hu : univ ⊆ {i : m | w i = 0}ᶜ ∪ {i : m | w i = 0} := by rw [Set.compl_union_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
[PROOFSTEP]
rw [Set.compl_union_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have hd : Disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := disjoint_compl_left
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have B₁ := iSup_range_stdBasis_eq_iInf_ker_proj K (fun _ : m => K) hd hu (Set.toFinite _)
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have B₂ := iInfKerProjEquiv K (fun _ ↦ K) hd hu
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
B₂ : { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
rw [LinearMap.rank, range_diagonal, B₁, ← @rank_fun' K]
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
B₂ : { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i
⊢ Module.rank K { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } = Module.rank K ({ i // w i ≠ 0 } → K)
[PROOFSTEP]
apply LinearEquiv.rank_eq
[GOAL]
case f
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
B₂ : { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i
⊢ { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] { i // w i ≠ 0 } → K
[PROOFSTEP]
apply B₂


[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), ↑abv (A i j) ≤ x
σ : Perm n
x✝ : σ ∈ univ
⊢ ↑abv (↑Perm.sign σ • ∏ i : n, A (↑σ i) i) = ∏ i : n, ↑abv (A (↑σ i) i)
[PROOFSTEP]
rw [abv.map_units_int_smul, abv.map_prod]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), ↑abv (A i j) ≤ x
x✝¹ : Perm n
x✝ : x✝¹ ∈ univ
⊢ ∏ _i : n, x = x ^ Fintype.card n
[PROOFSTEP]
rw [prod_const, Finset.card_univ]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), ↑abv (A i j) ≤ x
⊢ ∑ _σ : Perm n, x ^ Fintype.card n = Nat.factorial (Fintype.card n) • x ^ Fintype.card n
[PROOFSTEP]
rw [sum_const, Finset.card_univ, Fintype.card_perm]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), ↑abv (A k i j) ≤ x
i j : n
⊢ ↑abv (Finset.sum s (fun k => A k) i j) = ↑abv (∑ k in s, A k i j)
[PROOFSTEP]
simp only [sum_apply]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
c : ι → R
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), ↑abv (A k i j) ≤ x
y : S
hy : ∀ (k : ι), ↑abv (c k) ≤ y
⊢ ↑abv (det (∑ k in s, c k • A k)) ≤ Nat.factorial (Fintype.card n) • (card s • y * x) ^ Fintype.card n
[PROOFSTEP]
simpa only [smul_mul_assoc] using
  det_sum_le s fun k i j =>
    calc
      abv (c k * A k i j) = abv (c k) * abv (A k i j) := abv.map_mul _ _
      _ ≤ y * x := mul_le_mul (hy k) (hx k i j) (abv.nonneg _) ((abv.nonneg _).trans (hy k))


[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype p
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ trace 1 = ↑(Fintype.card n)
[PROOFSTEP]
simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype p
inst✝¹ : AddCommMonoid R
inst✝ : CommSemigroup R
A : Matrix m n R
B : Matrix n m R
⊢ trace (A * B) = trace (B * A)
[PROOFSTEP]
rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ trace (A * B * C) = trace (C * A * B)
[PROOFSTEP]
rw [trace_mul_comm, Matrix.mul_assoc]
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ trace (A * (B * C)) = trace (C * (A * B))
[PROOFSTEP]
rw [← Matrix.mul_assoc, trace_mul_comm]
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ trace (col a * row b) = a ⬝ᵥ b
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ (x : n), x ∈ Finset.univ → diag (col a * row b) x = a x * b x
[PROOFSTEP]
simp [mul_apply]
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ trace A = A 0 0 + A 1 1 + A 2 2
[PROOFSTEP]
rw [← add_zero (A 2 2), add_assoc]
[GOAL]
ι : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
α : Type u_5
R : Type u_6
S : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ trace A = A 0 0 + (A 1 1 + (A 2 2 + 0))
[PROOFSTEP]
rfl