-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
/-- The set of nonnegative elements in a C⋆-algebra is closed. -/
lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a}

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed (Unitization.inr '' {a | 0 ≤ a})

Tactic:
convert this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range

Result:
case h.e'_3
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ Unitization.inr '' {a | 0 ≤ a} = {a | 0 ≤ a} ∩ Set.range Unitization.inr

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
x : A
h : ↑x = a
⊢ 0 ≤ x ↔ 0 ≤ a

Tactic:
simp [← h]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ IsClosed ({a | IsSelfAdjoint a} ∩ {a | ‖(algebraMap ℝ (Unitization ℂ A)) ↑‖a‖₊ - a‖₊ ≤ ‖a‖₊})

Tactic:
refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_

Result:
case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous star

case refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous fun a => a

case refine_3
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous fun a => ‖(algebraMap ℝ (Unitization ℂ A)) ↑‖a‖₊ - a‖₊

case refine_4
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous nnnorm

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed {a | 0 ≤ a}

Tactic:
rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed (Unitization.inr '' {a | 0 ≤ a})

Proof state:
case h.e'_3
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ Unitization.inr '' {a | 0 ≤ a} = {a | 0 ≤ a} ∩ Set.range Unitization.inr

Tactic:
ext a

Result:
case h.e'_3.h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
⊢ a ∈ Unitization.inr '' {a | 0 ≤ a} ↔ a ∈ {a | 0 ≤ a} ∩ Set.range Unitization.inr

Proof state:
case h.e'_3.h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
⊢ a ∈ Unitization.inr '' {a | 0 ≤ a} ↔ a ∈ {a | 0 ≤ a} ∩ Set.range Unitization.inr

Tactic:
simp only [Set.mem_image, Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_range, ← exists_and_left]

Result:
case h.e'_3.h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
⊢ (∃ x, 0 ≤ x ∧ ↑x = a) ↔ ∃ x, 0 ≤ a ∧ ↑x = a

Proof state:
case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous star

case refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous fun a => a

case refine_3
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous fun a => ‖(algebraMap ℝ (Unitization ℂ A)) ↑‖a‖₊ - a‖₊

case refine_4
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous nnnorm

Tactic:
all_goals fun_prop

Result:
no goals

Proof state:
case h.e'_3.h.a.h.e'_2.h.a
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
x : A
⊢ 0 ≤ x ∧ ↑x = a ↔ 0 ≤ a ∧ ↑x = a

Tactic:
exact and_congr_left fun h ↦ by simp [← h]

Result:
no goals

Proof state:
case refine_4
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Continuous nnnorm

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.e'_3.h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
⊢ (∃ x, 0 ≤ x ∧ ↑x = a) ↔ ∃ x, 0 ≤ a ∧ ↑x = a

Tactic:
congr! 2 with x

Result:
case h.e'_3.h.a.h.e'_2.h.a
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
a : Unitization ℂ A
x : A
⊢ 0 ≤ x ∧ ↑x = a ↔ 0 ≤ a ∧ ↑x = a