-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
/-- A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue. -/
lemma exists_eigenvector_of_ne_zero (hA : IsHermitian A) (h_ne : A ≠ 0) :
    ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : A = ↑hA.eigenvectorUnitary * diagonal (Function.const n 0) * star ↑hA.eigenvectorUnitary
⊢ Function.const n 0 = fun x => 0

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp this

Result:
case intro
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
i : n
hi : hA.eigenvalues i ≠ 0 i
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
⊢ A = 0

Tactic:
have := hA.spectral_theorem

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : A = ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary
⊢ A = 0

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : A = ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary
⊢ A = 0

Tactic:
rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
  diagonal_zero, mul_zero, zero_mul] at this

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
i : n
hi : hA.eigenvalues i ≠ 0 i
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
exact ⟨_, _, hi, hA.eigenvectorBasis.orthonormal.ne_zero i, hA.mulVec_eigenvectorBasis i⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
have : hA.eigenvalues ≠ 0 := by
  contrapose! h_ne
  have := hA.spectral_theorem
  rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
    diagonal_zero, mul_zero, zero_mul] at this

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ hA.eigenvalues ≠ 0

Tactic:
contrapose! h_ne

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
⊢ A = 0

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
classical
have : hA.eigenvalues ≠ 0 := by
  contrapose! h_ne
  have := hA.spectral_theorem
  rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
    diagonal_zero, mul_zero, zero_mul] at this
obtain ⟨i, hi⟩ := Function.ne_iff.mp this
exact ⟨_, _, hi, hA.eigenvectorBasis.orthonormal.ne_zero i, hA.mulVec_eigenvectorBasis i⟩

Result:
no goals