-- 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
⊢ f + p ^ 2 = g

Tactic:
rwa [add_comm, ← eq_sub_iff_add_eq]

Result:
no goals

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

Tactic:
intro 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 : f ≤ g
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), g = f + p

Proof state:
case mpr.intro.intro.one
𝕜 : 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
⊢ IsPositive 0

Tactic:
exact isPositive_zero

Result:
no goals

Proof state:
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 ^ 2 ∈ AddSubmonoid.closure (Set.range fun s => star s * s)

Tactic:
exact AddSubmonoid.subset_closure ⟨p, by simp only [hp₁.star_eq, sq]⟩

Result:
no goals

Proof state:
case mpr.intro.intro.mem
𝕜 : 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 x✝ : H →L[𝕜] H
hf : x✝ ∈ Set.range fun s => star s * s
⊢ x✝.IsPositive

Tactic:
obtain ⟨f, rfl⟩ := hf

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

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

Tactic:
refine ⟨p ^ 2, ?_, by symm; rwa [add_comm, ← eq_sub_iff_add_eq]⟩

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 ^ 2 ∈ AddSubmonoid.closure (Set.range fun s => star s * s)