-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma SpectrumRestricts.smul_of_nonneg {A : Type*} [Ring A] [Algebra ℝ A] {a : A}
    (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ} (hr : 0 ≤ r) :
    SpectrumRestricts (r • a) ContinuousMap.realToNNReal

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
⊢ ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x

Tactic:
intro x hx

Result:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
⊢ 0 ≤ x

Proof state:
case pos
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hr' : r = 0
hx : x = 0
⊢ 0 ≤ x

Tactic:
exact hx.symm.le

Result:
no goals

Proof state:
case pos
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : r = 0
⊢ 0 ≤ x

Tactic:
simp [hr'] at hx ⊢

Result:
case pos
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hr' : r = 0
hx : x = 0
⊢ 0 ≤ x

Proof state:
case neg
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : ¬r = 0
⊢ 0 ≤ x

Tactic:
lift r to ℝˣ using IsUnit.mk0 r hr'

Result:
case neg.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : x ∈ spectrum ℝ (↑r • a)
hr' : ¬↑r = 0
⊢ 0 ≤ x

Proof state:
case neg.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬↑r = 0
⊢ (↑r)⁻¹ • 0 ≤ (↑r)⁻¹ • x

Tactic:
simpa [Units.smul_def] using ha _ hx

Result:
no goals

Proof state:
case neg.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬↑r = 0
⊢ 0 ≤ x

Tactic:
refine le_of_smul_le_smul_left ?_ (inv_pos.mpr <| lt_of_le_of_ne hr <| ne_comm.mpr hr')

Result:
case neg.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬↑r = 0
⊢ (↑r)⁻¹ • 0 ≤ (↑r)⁻¹ • x

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
⊢ ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x

Tactic:
nontriviality A

Result:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
⊢ ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
⊢ 0 ≤ x

Tactic:
by_cases hr' : r = 0

Result:
case pos
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : r = 0
⊢ 0 ≤ x

case neg
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : ¬r = 0
⊢ 0 ≤ x

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ
hr : 0 ≤ r
⊢ SpectrumRestricts (r • a) ⇑ContinuousMap.realToNNReal

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha ⊢

Result:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
⊢ ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x

Proof state:
case neg.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : x ∈ spectrum ℝ (↑r • a)
hr' : ¬↑r = 0
⊢ 0 ≤ x

Tactic:
rw [← Units.smul_def, spectrum.unit_smul_eq_smul, Set.mem_smul_set_iff_inv_smul_mem] at hx

Result:
case neg.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬↑r = 0
⊢ 0 ≤ x