-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
/-- In a unital `ℝ`-algebra `A` with a continuous functional calculus, an element `a : A` is larger
than some `algebraMap ℝ A r` if and only if every element of the `ℝ`-spectrum is nonnegative. -/
lemma CFC.exists_pos_algebraMap_le_iff {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A]
    [PartialOrder A] [StarOrderedRing A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] [Nontrivial A]
    [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)]
    {a : A} (ha : IsSelfAdjoint a

Proof state:
case refine_1
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) → ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
rintro ⟨r, hr, hr_le⟩

Result:
case refine_1.intro.intro
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
r : ℝ
hr : r > 0
hr_le : ∀ x ∈ spectrum ℝ a, r ≤ x
⊢ ∀ x ∈ spectrum ℝ a, 0 < x

Proof state:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
simp_rw [algebraMap_le_iff_le_spectrum (a := a)]

Result:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Proof state:
case refine_2.intro.intro
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
r : ℝ
hr : r ∈ spectrum ℝ a
hr_min : IsMinOn id (spectrum ℝ a) r
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Tactic:
exact ⟨r, h _ hr, hr_min⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
have h_cpct : IsCompact (spectrum ℝ a) := isCompact_iff_compactSpace.mpr inferInstance

Result:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Proof state:
case refine_2
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Tactic:
obtain ⟨r, hr, hr_min⟩ := h_cpct.exists_isMinOn (spectrum_nonempty ℝ a ha) continuousOn_id

Result:
case refine_2.intro.intro
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
r : ℝ
hr : r ∈ spectrum ℝ a
hr_min : IsMinOn id (spectrum ℝ a) r
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Proof state:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) → ∀ x ∈ spectrum ℝ a, 0 < x

case refine_2
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x