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