[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitLower I i x) = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
rw [splitLower, coe_mk']
[GOAL]
ι : Type u_1
M : Type u_2
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}
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
M : Type u_2
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}
[PROOFSTEP]
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]
[GOAL]
case h
ι : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [and_comm (a := y i ≤ x), Pi.le_def]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitLower I i x) ⊆ ↑↑I
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ splitLower I i x = ⊥ ↔ x ≤ lower I i
[PROOFSTEP]
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ (min x (upper I i) ≤ lower I i ∨ ∃ x x_1, upper I x ≤ lower I x) ↔ x ≤ lower I i
[PROOFSTEP]
simp [(I.lower_lt_upper _).not_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ splitLower I i x = ↑I ↔ upper I i ≤ x
[PROOFSTEP]
simp [splitLower, update_eq_iff]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (lower I i) (upper I i)
h' : optParam (∀ (j : ι), lower I j < update I.upper i x j) (_ : ∀ (x_1 : ι), lower I x_1 < update I.upper i x x_1)
⊢ splitLower I i x = ↑{ lower := I.lower, upper := update I.upper i x, lower_lt_upper := h' }
[PROOFSTEP]
simp only [splitLower, mk'_eq_coe, min_eq_left h.2.le, update]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitUpper I i x) = ↑I ∩ {y | x < y i}
[PROOFSTEP]
rw [splitUpper, coe_mk']
[GOAL]
ι : Type u_1
M : Type u_2
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}
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
M : Type u_2
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}
[PROOFSTEP]
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]
[GOAL]
case h
ι : Type u_1
M : Type u_2
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
[PROOFSTEP]
exact and_comm
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitUpper I i x) ⊆ ↑↑I
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ splitUpper I i x = ⊥ ↔ upper I i ≤ x
[PROOFSTEP]
rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ (upper I i ≤ max x (lower I i) ∨ ∃ x x_1, upper I x ≤ lower I x) ↔ upper I i ≤ x
[PROOFSTEP]
simp [(I.lower_lt_upper _).not_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ splitUpper I i x = ↑I ↔ x ≤ lower I i
[PROOFSTEP]
simp [splitUpper, update_eq_iff]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (lower I i) (upper I i)
h' : optParam (∀ (j : ι), update I.lower i x j < upper I j) (_ : ∀ (x_1 : ι), update I.lower i x x_1 < upper I x_1)
⊢ splitUpper I i x = ↑{ lower := update I.lower i x, upper := I.upper, lower_lt_upper := h' }
[PROOFSTEP]
simp only [splitUpper, mk'_eq_coe, max_eq_left h.1.le, update]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (splitLower I i x) (splitUpper I i x)
[PROOFSTEP]
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
[PROOFSTEP]
refine' (Disjoint.inf_left' _ _).inf_right' _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint {y | y i ≤ x} {y | x < y i}
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → ¬a ∈ {y | x < y i}
[PROOFSTEP]
exact fun y (hle : y i ≤ x) hlt => not_lt_of_le hle hlt
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ splitLower I i x ≠ splitUpper I i x
[PROOFSTEP]
cases' le_or_lt x (I.lower i) with h
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ splitLower I i x ≠ splitUpper I i x
[PROOFSTEP]
rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ ⊥ ≠ ↑I
[PROOFSTEP]
exact WithBot.bot_ne_coe
[GOAL]
case inr
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ splitUpper I i x
[PROOFSTEP]
refine' (disjoint_splitLower_splitUpper I i x).ne _
[GOAL]
case inr
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ ⊥
[PROOFSTEP]
rwa [Ne.def, splitLower_eq_bot, not_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (J : WithBot (Box ι)), J ∈ {Box.splitLower I i x, Box.splitUpper I i x} → J ≤ ↑I
[PROOFSTEP]
simp only [Finset.mem_insert, Finset.mem_singleton]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (J : WithBot (Box ι)), J = Box.splitLower I i x ∨ J = Box.splitUpper I i x → J ≤ ↑I
[PROOFSTEP]
rintro J (rfl | rfl)
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Box.splitLower I i x ≤ ↑I
case inr ι : Type u_1 M : Type u_2 n : ℕ I✝ J : Box ι i✝ : ι x✝ : ℝ I : Box ι i : ι x : ℝ ⊢ Box.splitUpper I i x ≤ ↑I
[PROOFSTEP]
exacts [Box.splitLower_le, Box.splitUpper_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Set.Pairwise (↑{Box.splitLower I i x, Box.splitUpper I i x}) Disjoint
[PROOFSTEP]
simp only [Finset.coe_insert, Finset.coe_singleton, true_and_iff, Set.mem_singleton_iff,
  pairwise_insert_of_symmetric symmetric_disjoint, pairwise_singleton]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (b : WithBot (Box ι)), b = Box.splitUpper I i x → Box.splitLower I i x ≠ b → Disjoint (Box.splitLower I i x) b
[PROOFSTEP]
rintro J rfl -
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (Box.splitLower I i x) (Box.splitUpper I i x)
[PROOFSTEP]
exact I.disjoint_splitLower_splitUpper i x
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ ↑J = Box.splitLower I i x ∨ ↑J = Box.splitUpper I i x
[PROOFSTEP]
simp [split]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ ↑J = ↑I ∩ {y | y i ≤ x} ∨ ↑J = ↑I ∩ {y | x < y i}
[PROOFSTEP]
simp [mem_split_iff, ← Box.withBotCoe_inj]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Prepartition.iUnion (split I i x) = ↑I
[PROOFSTEP]
simp [split, ← inter_union_distrib_left, ← setOf_or, le_or_lt]
[GOAL]
ι : Type u_1
M✝ : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J in (split I i x).boxes, f J = Option.elim' 0 f (Box.splitLower I i x) + Option.elim' 0 f (Box.splitUpper I i x)
[PROOFSTEP]
rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
⊢ split I i x = ⊤
[PROOFSTEP]
refine' ((isPartitionTop I).eq_of_boxes_subset fun J hJ => _).symm
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
J : Box ι
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split I i x).boxes
[PROOFSTEP]
rcases mem_top.1 hJ with rfl
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes
[PROOFSTEP]
clear hJ
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ J ∈ (split J i x).boxes
[PROOFSTEP]
rw [mem_boxes, mem_split_iff]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
rw [mem_Ioo, not_and_or, not_lt, not_lt] at h 
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : x ≤ Box.lower J i ∨ Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
cases h <;> [right; left]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : x ≤ Box.lower J i ∨ Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
cases h
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ Box.lower J i
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
right
[GOAL]
case inr
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
left
[GOAL]
case inl.h
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ Box.lower J i
⊢ ↑J = Box.splitUpper J i x
[PROOFSTEP]
rwa [eq_comm, Box.splitUpper_eq_self]
[GOAL]
case inr.h
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x
[PROOFSTEP]
rwa [eq_comm, Box.splitLower_eq_self]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
⊢ ↑J = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
refine' (mem_split_iff'.1 h₁).resolve_right fun H => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
[PROOFSTEP]
rw [← Box.mem_coe, H] at h₂ 
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
[PROOFSTEP]
exact h₃.not_lt h₂.2
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
⊢ ↑J = ↑I ∩ {y | x < y i}
[PROOFSTEP]
refine' (mem_split_iff'.1 h₁).resolve_left fun H => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False
[PROOFSTEP]
rw [← Box.mem_coe, H] at h₂ 
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False
[PROOFSTEP]
exact h₃.not_le h₂.2
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
⊢ restrict (split J i x) I = split I i x
[PROOFSTEP]
refine' ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
⊢ (restrict (split J i x) I).boxes ⊆ (split I i x).boxes
[PROOFSTEP]
simp only [Finset.subset_iff, mem_boxes, mem_restrict', exists_prop, mem_split_iff']
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
[PROOFSTEP]
have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => (inter_subset_left _ _).trans h
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
[PROOFSTEP]
rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩ <;> [left; right]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
[PROOFSTEP]
rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩
[GOAL]
case intro.intro.inl
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | y i ≤ x}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x} ∨ ↑J₁ = ↑I ∩ {y | x < y i}
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | x < y i}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x} ∨ ↑J₁ = ↑I ∩ {y | x < y i}
[PROOFSTEP]
right
[GOAL]
case intro.intro.inl.h
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | y i ≤ x}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]
[GOAL]
case intro.intro.inr.h
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | x < y i}
⊢ ↑J₁ = ↑I ∩ {y | x < y i}
[PROOFSTEP]
simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.fst p.snd
[PROOFSTEP]
rw [splitMany, Finset.inf_insert, inf_comm, splitMany]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s : Finset (ι × ℝ)
⊢ IsPartition (splitMany I ∅)
[PROOFSTEP]
simp only [splitMany_empty, isPartitionTop]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s✝ : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
x✝ : ¬a ∈ s
hs : IsPartition (splitMany I s)
⊢ IsPartition (splitMany I (insert a s))
[PROOFSTEP]
simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = biUnion π fun J => splitMany J s
[PROOFSTEP]
induction' s using Finset.induction_on with p s _ ihp
[GOAL]
case empty
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = biUnion π fun J => splitMany J ∅
[PROOFSTEP]
simp
[GOAL]
case insert
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬p ∈ s
ihp : π ⊓ splitMany I s = biUnion π fun J => splitMany J s
⊢ π ⊓ splitMany I (insert p s) = biUnion π fun J => splitMany J (insert p s)
[PROOFSTEP]
simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
H : ∀ (i : ι), {(i, Box.lower J i), (i, Box.upper J i)} ⊆ s
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
⊢ Js ≤ J
[PROOFSTEP]
simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H 
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
⊢ Js ≤ J
[PROOFSTEP]
rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩
[GOAL]
case intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
⊢ Js ≤ J
[PROOFSTEP]
refine' fun y hy i => ⟨_, _⟩
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ Box.lower J i < y i
[PROOFSTEP]
rcases splitMany_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩
[GOAL]
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
⊢ Box.lower J i < y i
[PROOFSTEP]
have := Hle hxs
[GOAL]
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
[PROOFSTEP]
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1] at Hle 
[GOAL]
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : ↑Js ⊆ ↑I ∩ {y | Box.lower J i < y i}
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
[PROOFSTEP]
exact (Hle hy).2
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
[GOAL]
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
have := Hle hxs
[GOAL]
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle 
[GOAL]
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : ↑Js ⊆ ↑I ∩ {y | y i ≤ Box.upper J i}
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
exact (Hle hy).2
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
[PROOFSTEP]
refine'
  eventually_atTop.2
    ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)}, fun t ht I J hJ J' hJ' =>
      not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => _) hJ'⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : t ≥ Finset.biUnion s fun J => Finset.biUnion Finset.univ fun i => {(i, Box.lower J i), (i, Box.upper J i)}
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, Box.lower J i), (i, Box.upper J i)} ⊆ t
[PROOFSTEP]
exact fun p hp => ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
[PROOFSTEP]
refine' (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
⊢ π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
[PROOFSTEP]
refine' le_antisymm ((biUnion_le_iff _).2 fun J hJ => _) (le_inf (fun J hJ => _) (filter_le _ _))
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ restrict (splitMany I t) J ≤ restrict (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π) J
[PROOFSTEP]
refine' ofWithBot_mono _
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    J_1 ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (splitMany I t).boxes →
      J_1 ≠ ⊥ →
        ∃ J',
          J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π).boxes ∧
            J_1 ≤ J'
[PROOFSTEP]
simp only [Finset.mem_image, exists_prop, mem_boxes, mem_filter]
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    (∃ a, a ∈ splitMany I t ∧ ↑J ⊓ ↑a = J_1) →
      J_1 ≠ ⊥ → ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ J_1 ≤ J'
[PROOFSTEP]
rintro _ ⟨J₁, h₁, rfl⟩ hne
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ ↑J ⊓ ↑J₁ ≤ J'
[PROOFSTEP]
refine' ⟨_, ⟨J₁, ⟨h₁, Subset.trans _ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ↑J₁ ⊆ ↑J
[PROOFSTEP]
exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
[PROOFSTEP]
rw [mem_filter] at hJ 
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
[PROOFSTEP]
rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
[PROOFSTEP]
refine' ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 _⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ Set.Nonempty (↑J' ∩ ↑J)
[PROOFSTEP]
exact ⟨J.upper, hmem, J.upper_mem⟩
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
⊢ ∃ s, splitMany I s ≤ π
[PROOFSTEP]
refine' (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ splitMany I s ≤ π
[PROOFSTEP]
rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs 
[GOAL]
case hp
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ ↑I
⊢ ∀ (J : Box ι), J ∈ splitMany I s → ↑J ⊆ ↑I
[PROOFSTEP]
exact fun J hJ => le_of_mem _ hJ
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
[PROOFSTEP]
rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
[PROOFSTEP]
use(splitMany I s).filter fun J => ¬(J : Set (ι → ℝ)) ⊆ π.iUnion
[GOAL]
case h
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ Prepartition.iUnion (filter (splitMany I s) fun J => ¬↑J ⊆ Prepartition.iUnion π) = ↑I \ Prepartition.iUnion π
[PROOFSTEP]
simp [← hs]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ compl π₁ = compl π₂
[PROOFSTEP]
dsimp only [compl]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) =
    Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂)
[PROOFSTEP]
congr 1
[GOAL]
case e_p
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ (fun π' => Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) = fun π' =>
    Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
h : IsPartition π
⊢ compl π = ⊥
[PROOFSTEP]
rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]
