-- Mathlib/Topology/ContinuousMap/StarOrdered.lean
lemma starOrderedRing_of_sqrt {R : Type*} [PartialOrder R] [NonUnitalRing R] [StarRing R]
    [StarOrderedRing R] [TopologicalSpace R] [ContinuousStar R] [IsTopologicalRing R]
    (sqrt : R → R) (h_continuousOn : ContinuousOn sqrt {x : R | 0 ≤ x})
    (h_sqrt : ∀ x, 0 ≤ x → star (sqrt x) * sqrt x = x) : StarOrderedRing C(α, R) :=
  StarOrderedRing.of_nonneg_iff' add_le_add_left fun f ↦ by
    constructor
    · intro hf
      use (mk _ h_continuousOn.restrict).comp ⟨_, map_continuous f |>.codRestrict (by exact hf ·)⟩
      ext x
      exact h_sqrt (f x) (hf x) |>.symm
    · rintro ⟨f, rfl⟩
      rw [ContinuousMap.le_def]
      exact fun x ↦ star_mul_self_nonneg (f x)

Proof state:
case mpr
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ (∃ s, f = star s * s) → 0 ≤ f

Tactic:
rintro ⟨f, rfl⟩

Result:
case mpr.intro
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ 0 ≤ star f * f

Proof state:
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ 0 ≤ f ↔ ∃ s, f = star s * s

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ 0 ≤ f → ∃ s, f = star s * s

case mpr
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ (∃ s, f = star s * s) → 0 ≤ f

Proof state:
case mp
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ 0 ≤ f → ∃ s, f = star s * s

Tactic:
intro hf

Result:
case mp
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
hf : 0 ≤ f
⊢ ∃ s, f = star s * s

Proof state:
case mpr.intro
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ ∀ (a : α), 0 a ≤ (star f * f) a

Tactic:
exact fun x ↦ star_mul_self_nonneg (f x)

Result:
no goals

Proof state:
case h.h
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
hf : 0 ≤ f
x : α
⊢ f x =
    (star
          ({ toFun := {x | 0 ≤ x}.restrict sqrt, continuous_toFun := ⋯ }.comp
            { toFun := Set.codRestrict ⇑f {x | 0 ≤ x} ⋯, continuous_toFun := ⋯ }) *
        { toFun := {x | 0 ≤ x}.restrict sqrt, continuous_toFun := ⋯ }.comp
          { toFun := Set.codRestrict ⇑f {x | 0 ≤ x} ⋯, continuous_toFun := ⋯ })
      x

Tactic:
exact h_sqrt (f x) (hf x) |>.symm

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ 0 ≤ star f * f

Tactic:
rw [ContinuousMap.le_def]

Result:
case mpr.intro
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
⊢ ∀ (a : α), 0 a ≤ (star f * f) a

Proof state:
case h
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
hf : 0 ≤ f
⊢ f =
    star
        ({ toFun := {x | 0 ≤ x}.restrict sqrt, continuous_toFun := ⋯ }.comp
          { toFun := Set.codRestrict ⇑f {x | 0 ≤ x} ⋯, continuous_toFun := ⋯ }) *
      { toFun := {x | 0 ≤ x}.restrict sqrt, continuous_toFun := ⋯ }.comp
        { toFun := Set.codRestrict ⇑f {x | 0 ≤ x} ⋯, continuous_toFun := ⋯ }

Tactic:
ext x

Result:
case h.h
α : Type u_1
inst✝⁷ : TopologicalSpace α
R : Type u_2
inst✝⁶ : PartialOrder R
inst✝⁵ : NonUnitalRing R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousStar R
inst✝ : IsTopologicalRing R
sqrt : R → R
h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}
h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x
f : C(α, R)
hf : 0 ≤ f
x : α
⊢ f x =
    (star
          ({ toFun := {x | 0 ≤ x}.restrict sqrt, continuous_toFun := ⋯ }.comp
            { toFun := Set.codRestrict ⇑f {x | 0 ≤ x} ⋯, continuous_toFun := ⋯ }) *
        { toFun := {x | 0 ≤ x}.restrict sqrt, continuous_toFun := ⋯ }.comp
          { toFun := Set.codRestrict ⇑f {x | 0 ≤ x} ⋯, continuous_toFun := ⋯ })
      x