ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (Set.pi univ fun i_1 => Ioc (update I.lower i (max x (lower I i)) i_1) (upper I i_1)) = ↑I ∩ {y | x < y i}
ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitUpper I i x) = ↑I ∩ {y | x < y i}
rw [splitUpper, coe_mk']
case h
ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (y ∈ Set.pi univ fun i_1 => Ioc (update I.lower i (max x (lower I i)) i_1) (upper I i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}
ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (Set.pi univ fun i_1 => Ioc (update I.lower i (max x (lower I i)) i_1) (upper I i_1)) = ↑I ∩ {y | x < y i}
ext y
case h
ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (x < y i ∧ (∀ (b : ι), lower I b < y b) ∧ ∀ (x : ι), y x ≤ upper I x) ↔
    ((∀ (x : ι), lower I x < y x) ∧ ∀ (x : ι), y x ≤ upper I x) ∧ x < y i
case h
ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (y ∈ Set.pi univ fun i_1 => Ioc (update I.lower i (max x (lower I i)) i_1) (upper I i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
  forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
  and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
no goals
case h
ι : Type u_1
M : Type ?u.11166
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (x < y i ∧ (∀ (b : ι), lower I b < y b) ∧ ∀ (x : ι), y x ≤ upper I x) ↔
    ((∀ (x : ι), lower I x < y x) ∧ ∀ (x : ι), y x ≤ upper I x) ∧ x < y i
exact and_comm