-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
/-- The `ℝ`-spectrum of an element of the form `star b * b` in a C⋆-algebra is nonnegative.

This is the key result used to establish `CStarAlgebra.instNonnegSpectrumClass`. -/
lemma spectrum_star_mul_self_nonneg {b : A} : ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ ∀ x ∈ (fun x => x⁻ ^ 3) '' spectrum ℝ a, 0 ≤ x

Tactic:
rintro - ⟨x, -, rfl⟩

Result:
case intro.intro
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
x : ℝ
⊢ 0 ≤ (fun x => x⁻ ^ 3) x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : 0 = cfcₙ (fun x => x⁻) a ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ 0⁻ = 0

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)) ⇑ContinuousMap.realToNNReal

Tactic:
refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀

Result:
case refine_1
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ IsSelfAdjoint (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2))

case refine_2
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ IsSelfAdjoint (-(star c * c))

case refine_3
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2)) ⇑ContinuousMap.realToNNReal

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : cfc 0 a = cfc (fun x => x⁻ ^ 3) a
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
h_eqOn : Set.EqOn 0 (fun x => x⁻ ^ 3) (spectrum ℝ a)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
exact fun x hx ↦ negPart_eq_zero.mp <| pow_eq_zero (h_eqOn hx).symm

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
⊢ ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x

Tactic:
set a := star b * b with a_def

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ 0 ≤ ↑2

Tactic:
norm_num

Result:
no goals