ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ (match ⊥ with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty ↑⊥
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ Option.isSome ⊥ = true ↔ Set.Nonempty ↑⊥
erw [Option.isSome]
no goals
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ (match ⊥ with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty ↑⊥
simp
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
⊢ (match ↑I with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty ↑↑I
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
⊢ Option.isSome ↑I = true ↔ Set.Nonempty ↑↑I
erw [Option.isSome]
no goals
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
⊢ (match ↑I with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty ↑↑I
simp [I.nonempty_coe]