-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem eigenvalue_nonneg_of_nonneg {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : HasEigenvalue T μ)
    (hnn : ∀ x : E, 0 ≤ RCLike.re ⟪x, T x⟫) : 0 ≤ μ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2

Tactic:
have := congr_arg RCLike.re (inner_product_apply_eigenvector hv.1)

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : RCLike.re (inner v (T v)) = RCLike.re (↑μ * ↑‖v‖ ^ 2)
⊢ RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : RCLike.re (inner v (T v)) = RCLike.re (↑μ * ↑‖v‖ ^ 2)
⊢ RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2

Tactic:
rw [← RCLike.ofReal_pow, ← RCLike.ofReal_mul] at this

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : RCLike.re (inner v (T v)) = RCLike.re ↑(μ * ‖v‖ ^ 2)
⊢ RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2

Proof state:
case intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2
⊢ 0 ≤ μ

Tactic:
exact (mul_nonneg_iff_of_pos_right hpos).mp (this ▸ hnn v)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : RCLike.re (inner v (T v)) = RCLike.re ↑(μ * ‖v‖ ^ 2)
⊢ RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2

Tactic:
exact mod_cast this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
⊢ 0 ≤ μ

Tactic:
obtain ⟨v, hv⟩ := hμ.exists_hasEigenvector

Result:
case intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 ≤ μ

Proof state:
case intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ 0 ≤ μ

Tactic:
have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 := by
  have := congr_arg RCLike.re (inner_product_apply_eigenvector hv.1)
  rw [← RCLike.ofReal_pow, ← RCLike.ofReal_mul] at this
  exact mod_cast this

Result:
case intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : RCLike.re (inner v (T v)) = μ * ‖v‖ ^ 2
⊢ 0 ≤ μ

Proof state:
case intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 ≤ μ

Tactic:
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2

Result:
case intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ 0 ≤ μ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re (inner x (T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < ‖v‖ ^ 2

Tactic:
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2

Result:
no goals