-- Mathlib/Analysis/InnerProductSpace/StarOrder.lean
/-- Because this takes `ContinuousFunctionalCalculus ℝ IsSelfAdjoint` as an argument, and for
the moment we only have this for `𝕜 := ℂ`, this is not registered as an instance. -/
lemma instStarOrderedRingRCLike
    [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : (H →L[𝕜] H) → Prop)] :
    StarOrderedRing (H →L[𝕜] H) where
  le_iff f g

Proof state:
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p ^ 2 = g - f
⊢ (fun s => star s * s) p = p ^ 2

Tactic:
simp only [hp₁.star_eq, sq]

Result:
no goals

Proof state:
case mpr.intro.intro.mem.intro
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f✝ p f : H →L[𝕜] H
⊢ ((fun s => star s * s) f).IsPositive

Tactic:
simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f

Result:
no goals

Proof state:
case mpr
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
⊢ (∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p) → f ≤ g

Tactic:
rintro ⟨p, hp, rfl⟩

Result:
case mpr.intro.intro
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f p : H →L[𝕜] H
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ f ≤ f + p

Proof state:
case mp
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p

Tactic:
obtain ⟨p, hp₁, -, hp₃⟩ :=
  CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts h.1 h.spectrumRestricts

Result:
case mp.intro.intro.intro
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p ^ 2 = g - f
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p

Proof state:
case mpr.intro.intro
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f p : H →L[𝕜] H
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ f ≤ f + p

Tactic:
rw [le_def, add_sub_cancel_left]

Result:
case mpr.intro.intro
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f p : H →L[𝕜] H
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ p.IsPositive

Proof state:
case mpr.intro.intro.mul
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f✝ p f g : H →L[𝕜] H
hx✝ : f ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hy✝ : g ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hf : f.IsPositive
hg : g.IsPositive
⊢ (f + g).IsPositive

Tactic:
exact hf.add hg

Result:
no goals

Proof state:
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
⊢ f ≤ g ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
⊢ f ≤ g → ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p

case mpr
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
⊢ (∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p) → f ≤ g

Proof state:
case mpr.intro.intro
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f p : H →L[𝕜] H
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ p.IsPositive

Tactic:
induction hp using AddSubmonoid.closure_induction with
| mem _ hf =>
  obtain ⟨f, rfl⟩ := hf
  simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f
| one => exact isPositive_zero
| mul f g _ _ hf hg => exact hf.add hg

Result:
no goals

Proof state:
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p ^ 2 = g - f
⊢ g = f + p ^ 2

Tactic:
symm

Result:
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p ^ 2 = g - f
⊢ f + p ^ 2 = g

Proof state:
case mp
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : f ≤ g
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p

Tactic:
rw [le_def] at h

Result:
case mp
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p