ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
          (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Set.Ioc (lower I x) (upper I x) ∧ ((lower I x + upper I x) / 2 < y x ↔ x ∈ s)
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ y ∈ splitCenterBox I s ↔ y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
simp only [splitCenterBox, mem_def, ← forall_and]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
        (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
          (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Set.Ioc (lower I x) (upper I x) ∧ ((lower I x + upper I x) / 2 < y x ↔ x ∈ s)
refine' forall_congr' fun i ↦ _
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (if i ∈ s then (lower I i + upper I i) / 2 else lower I i)
        (if i ∈ s then upper I i else (lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
        (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
dsimp only [Set.piecewise]
case inl
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Set.Ioc ((lower I i + upper I i) / 2) (upper I i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ (lower I i + upper I i) / 2 < y i

case inr
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : ¬i ∈ s
⊢ y i ∈ Set.Ioc (lower I i) ((lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ y i ≤ (lower I i + upper I i) / 2
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (if i ∈ s then (lower I i + upper I i) / 2 else lower I i)
        (if i ∈ s then upper I i else (lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
split_ifs with hs <;> simp only [hs, iff_true_iff, iff_false_iff, not_lt]
no goals
case inl
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Set.Ioc ((lower I i + upper I i) / 2) (upper I i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ (lower I i + upper I i) / 2 < y i

case inr
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : ¬i ∈ s
⊢ y i ∈ Set.Ioc (lower I i) ((lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ y i ≤ (lower I i + upper I i) / 2
exacts [⟨fun H ↦ ⟨⟨(left_lt_add_div_two.2 (I.lower_lt_upper i)).trans H.1, H.2⟩, H.1⟩,
    fun H ↦ ⟨H.2, H.1.2⟩⟩,
  ⟨fun H ↦ ⟨⟨H.1, H.2.trans (add_div_two_lt_right.2 (I.lower_lt_upper i)).le⟩, H.2⟩,
    fun H ↦ ⟨H.1.1, H.2⟩⟩]