-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
/-- The `CStarAlgebra.spectralOrder` on a C⋆-algebra is a `StarOrderedRing`. -/
lemma CStarAlgebra.spectralOrderedRing : @StarOrderedRing A _ (CStarAlgebra.spectralOrder A) _ :=
  let _ := CStarAlgebra.spectralOrder A
  { le_iff

Proof state:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
a✝ : Nontrivial A
⊢ IsSelfAdjoint 0 ∧ ∀ x ∈ spectrum ℝ ↑0, 0 ≤ x

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.mem
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x : A
hx : x ∈ Set.range fun s => star s * s
⊢ IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal

Tactic:
obtain ⟨s, rfl⟩ := hx

Result:
case mpr.intro.intro.mem.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ IsSelfAdjoint ((fun s => star s * s) s) ∧ QuasispectrumRestricts ((fun s => star s * s) s) ⇑ContinuousMap.realToNNReal

Proof state:
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ (fun s => star s * s) s = s * s

Tactic:
simp [hs₁.star_eq, sq]

Result:
no goals

Proof state:
case mp.intro.intro.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ s * s ∈ AddSubmonoid.closure (Set.range fun s => star s * s)

Tactic:
exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq, sq]⟩

Result:
no goals

Proof state:
case mpr.intro.intro.mul
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hx : IsSelfAdjoint ↑x ∧ SpectrumRestricts ↑x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint ↑y ∧ SpectrumRestricts ↑y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint ↑(x + y) ∧ SpectrumRestricts ↑(x + y) ⇑ContinuousMap.realToNNReal

Tactic:
rw [Unitization.inr_add]

Result:
case mpr.intro.intro.mul
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hx : IsSelfAdjoint ↑x ∧ SpectrumRestricts ↑x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint ↑y ∧ SpectrumRestricts ↑y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (↑x + ↑y) ∧ SpectrumRestricts (↑x + ↑y) ⇑ContinuousMap.realToNNReal

Proof state:
case mp.intro.intro.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p

Tactic:
refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩

Result:
case mp.intro.intro.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ s * s ∈ AddSubmonoid.closure (Set.range fun s => star s * s)

Proof state:
case mpr
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x y : A
⊢ (∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p) → x ≤ y

Tactic:
rintro ⟨p, hp, rfl⟩

Result:
case mpr.intro.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ x ≤ x + p