s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
⊢ z ∈ toNNReal '' s
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
⊢ OrdConnected (toNNReal '' s)
refine' ⟨ball_image_iff.2 fun x hx => ball_image_iff.2 fun y hy z hz => _⟩
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

case inr
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
⊢ z ∈ toNNReal '' s
cases' le_total y 0 with hy₀ hy₀
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : toNNReal x ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz
no goals
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : toNNReal x ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) (toNNReal ↑y)
⊢ z ∈ toNNReal '' s
case inr
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s
lift y to ℝ≥0 using hy₀
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) y
⊢ z ∈ toNNReal '' s
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) (toNNReal ↑y)
⊢ z ∈ toNNReal '' s
rw [toNNReal_coe] at hz
no goals
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) y
⊢ z ∈ toNNReal '' s
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩