ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    Set.pi univ fun i => Ioc (l i) (u i)
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ ↑(mk' l u) = Set.pi univ fun i => Ioc (l i) (u i)
rw [mk']
case inl
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑↑{ lower := l, upper := u, lower_lt_upper := h } = Set.pi univ fun i => Ioc (l i) (u i)

case inr
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ↑⊥ = Set.pi univ fun i => Ioc (l i) (u i)
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    Set.pi univ fun i => Ioc (l i) (u i)
split_ifs with h
no goals
case inl
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑↑{ lower := l, upper := u, lower_lt_upper := h } = Set.pi univ fun i => Ioc (l i) (u i)
exact coe_eq_pi _
case inr.intro
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ↑⊥ = Set.pi univ fun i => Ioc (l i) (u i)
case inr
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ↑⊥ = Set.pi univ fun i => Ioc (l i) (u i)
rcases not_forall.mp h with ⟨i, hi⟩
case inr.intro
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.271838) (u ?m.271838) = ∅

ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ι
case inr.intro
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ↑⊥ = Set.pi univ fun i => Ioc (l i) (u i)
rw [coe_bot, univ_pi_eq_empty]
no goals
case inr.intro
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.271838) (u ?m.271838) = ∅

ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ι
exact Ioc_eq_empty hi