-- Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean
theorem mem_splitCenterBox {s : Set ι} {y : ι → ℝ} :
    y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ i, (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s

Proof state:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Ioc (s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower i)
        (s.piecewise I.upper (fun i => (I.lower i + I.upper i) / 2) i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
dsimp only [Set.piecewise]

Result:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Ioc (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i)
        (if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Proof state:
case pos
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i

case neg
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ y i ≤ (I.lower i + I.upper i) / 2

Tactic:
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⟩⟩]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
⊢ y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s

Tactic:
simp only [splitCenterBox, mem_def, ← forall_and]

Result:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Ioc (s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower i)
          (s.piecewise I.upper (fun i => (I.lower i + I.upper i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Ioc (I.lower x) (I.upper x) ∧ ((I.lower x + I.upper x) / 2 < y x ↔ x ∈ s)

Proof state:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Ioc (s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower i)
          (s.piecewise I.upper (fun i => (I.lower i + I.upper i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Ioc (I.lower x) (I.upper x) ∧ ((I.lower x + I.upper x) / 2 < y x ↔ x ∈ s)

Tactic:
refine forall_congr' fun i ↦ ?_

Result:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Ioc (s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower i)
        (s.piecewise I.upper (fun i => (I.lower i + I.upper i) / 2) i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Proof state:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Ioc (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i)
        (if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
split_ifs with hs <;> simp only [hs, iff_true, iff_false, not_lt]

Result:
case pos
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i

case neg
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ y i ≤ (I.lower i + I.upper i) / 2