-- 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 y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left✝ : QuasispectrumRestricts s ⇑ContinuousMap.realToNNReal
hs₂ : s * s = y - x
⊢ y = x + s * s

Tactic:
rwa [eq_sub_iff_add_eq', eq_comm] at hs₂

Result:
no goals

Proof state:
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)
⊢ IsSelfAdjoint p ∧ QuasispectrumRestricts p ⇑ContinuousMap.realToNNReal

Tactic:
induction hp using AddSubmonoid.closure_induction with
| mem x hx =>
  obtain ⟨s, rfl⟩ := hx
  refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
  rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
    SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
  exact spectrum_star_mul_self_nonneg
| one =>
  rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
  nontriviality A
  simp
| mul x y _ _ hx hy =>
  simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
    quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
  rw [Unitization.inr_add]
  exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩

Result:
no goals

Proof state:
case mpr.intro.intro.mem.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ ∀ x ∈ spectrum ℝ (star ↑s * ↑s), 0 ≤ x

Tactic:
exact spectrum_star_mul_self_nonneg

Result:
no goals

Proof state:
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

Tactic:
refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩

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

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 ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint y ∧ QuasispectrumRestricts y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (x + y) ∧ QuasispectrumRestricts (x + y) ⇑ContinuousMap.realToNNReal

Tactic:
simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
  quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢

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 mpr.intro.intro.one
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ ∀ x ∈ spectrum ℝ ↑0, 0 ≤ x

Tactic:
nontriviality A

Result:
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

Proof state:
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

Tactic:
simp only [spectralOrder, add_sub_cancel_left]

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)
⊢ IsSelfAdjoint p ∧ QuasispectrumRestricts p ⇑ContinuousMap.realToNNReal

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

Tactic:
obtain ⟨s, hs₁, _, hs₂⟩ :=
  CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.2

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
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p

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

Tactic:
intro h

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

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:
exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩

Result:
no goals

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

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
  SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]

Result:
case mpr.intro.intro.mem.intro
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ ∀ x ∈ spectrum ℝ (star ↑s * ↑s), 0 ≤ x

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

Tactic:
constructor

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

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

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

Tactic:
intro x y

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

Proof state:
case mpr.intro.intro.one
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ QuasispectrumRestricts 0 ⇑ContinuousMap.realToNNReal

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]

Result:
case mpr.intro.intro.one
A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ ∀ x ∈ spectrum ℝ ↑0, 0 ≤ x