[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ Injective boxes
[PROOFSTEP]
rintro ⟨s₁, h₁, h₁'⟩ ⟨s₂, h₂, h₂'⟩ (rfl : s₁ = s₂)
[GOAL]
case mk.mk
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
s₁ : Finset (Box ι)
h₁ : ∀ (J : Box ι), J ∈ s₁ → J ≤ I
h₁' : Set.Pairwise (↑s₁) (Disjoint on Box.toSet)
h₂ : ∀ (J : Box ι), J ∈ s₁ → J ≤ I
h₂' : Set.Pairwise (↑s₁) (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
I✝ J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I✝
x : ι → ℝ
I J : Box ι
h : J ≤ I
⊢ ∀ (J_1 : Box ι), J_1 ∈ {J} → J_1 ≤ I
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
I✝ J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I✝
x : ι → ℝ
I J : Box ι
h : J ≤ I
⊢ Set.Pairwise (↑{J}) (Disjoint on Box.toSet)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ ∀ (a b : Prepartition I), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
suffices : ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
this : ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes
⊢ ∀ (a b : Prepartition I), a ≤ b → b ≤ a → a = b
case this
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes
[PROOFSTEP]
exact fun π₁ π₂ h₁ h₂ => injective_boxes (Subset.antisymm (this h₁ h₂) (this h₂ h₁))
[GOAL]
case this
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes
[PROOFSTEP]
intro π₁ π₂ h₁ h₂ J hJ
[GOAL]
case this
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
⊢ J ∈ π₂.boxes
[PROOFSTEP]
rcases h₁ hJ with ⟨J', hJ', hle⟩
[GOAL]
case this.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
⊢ J ∈ π₂.boxes
[PROOFSTEP]
rcases h₂ hJ' with ⟨J'', hJ'', hle'⟩
[GOAL]
case this.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
J'' : Box ι
hJ'' : J'' ∈ π₁
hle' : J' ≤ J''
⊢ J ∈ π₂.boxes
[PROOFSTEP]
obtain rfl : J = J''
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
J'' : Box ι
hJ'' : J'' ∈ π₁
hle' : J' ≤ J''
⊢ J = J''
case this.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
hJ'' : J ∈ π₁
hle' : J' ≤ J
⊢ J ∈ π₂.boxes
[PROOFSTEP]
exact π₁.eq_of_le hJ hJ'' (hle.trans hle')
[GOAL]
case this.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
hJ'' : J ∈ π₁
hle' : J' ≤ J
⊢ J ∈ π₂.boxes
[PROOFSTEP]
obtain rfl : J' = J
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
hJ'' : J ∈ π₁
hle' : J' ≤ J
⊢ J' = J
case this.intro.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J' : Box ι
hJ' : J' ∈ π₂
hJ : J' ∈ π₁.boxes
hle : J' ≤ J'
hJ'' : J' ∈ π₁
hle' : J' ≤ J'
⊢ J' ∈ π₂.boxes
[PROOFSTEP]
exact le_antisymm ‹_› ‹_›
[GOAL]
case this.intro.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J' : Box ι
hJ' : J' ∈ π₂
hJ : J' ∈ π₁.boxes
hle : J' ≤ J'
hJ'' : J' ∈ π₁
hle' : J' ≤ J'
⊢ J' ∈ π₂.boxes
[PROOFSTEP]
assumption
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
π : Prepartition I
J : Box ι
hJ : J ∈ π
⊢ I ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
⊢ InjOn (fun J => {i | Box.lower J i = x i}) {J | J ∈ π ∧ x ∈ ↑Box.Icc J}
[PROOFSTEP]
rintro J₁ ⟨h₁, hx₁⟩ J₂ ⟨h₂, hx₂⟩ (H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i})
[GOAL]
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
⊢ J₁ = J₂
[PROOFSTEP]
suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty
  by
  choose y hy₁ hy₂ using this
  exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
this : ∀ (i : ι), Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
⊢ J₁ = J₂
[PROOFSTEP]
choose y hy₁ hy₂ using this
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
y : ι → ℝ
hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i)
hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i)
⊢ J₁ = J₂
[PROOFSTEP]
exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
[GOAL]
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
⊢ ∀ (i : ι), Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
intro i
[GOAL]
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
i : ι
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
simp only [Set.ext_iff, mem_setOf] at H 
[GOAL]
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
cases' (hx₁.1 i).eq_or_lt with hi₁ hi₁
[GOAL]
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
have hi₂ : J₂.lower i = x i := (H _).1 hi₁
[GOAL]
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
⊢ x i < Box.upper J₁ i
[PROOFSTEP]
simpa only [hi₁] using J₁.lower_lt_upper i
[GOAL]
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
⊢ x i < Box.upper J₂ i
[PROOFSTEP]
simpa only [hi₂] using J₂.lower_lt_upper i
[GOAL]
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
H₂ : x i < Box.upper J₂ i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
rw [Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]
[GOAL]
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
H₂ : x i < Box.upper J₂ i
⊢ x i < Box.upper J₁ i ⊓ Box.upper J₂ i
[PROOFSTEP]
exact lt_min H₁ H₂
[GOAL]
case intro.intro.inr
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i < x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
[GOAL]
case intro.intro.inr
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i < x i
hi₂ : Box.lower J₂ i < x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
[PROOFSTEP]
exact ⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ card (filter (fun J => x ∈ ↑Box.Icc J) π.boxes) ≤ 2 ^ Fintype.card ι
[PROOFSTEP]
rw [← Fintype.card_set]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ card (filter (fun J => x ∈ ↑Box.Icc J) π.boxes) ≤ Fintype.card (Set ι)
[PROOFSTEP]
refine' Finset.card_le_card_of_inj_on (fun J : Box ι => {i | J.lower i = x i}) (fun _ _ => Finset.mem_univ _) _
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ ∀ (a₁ : Box ι),
    a₁ ∈ filter (fun J => x ∈ ↑Box.Icc J) π.boxes →
      ∀ (a₂ : Box ι),
        a₂ ∈ filter (fun J => x ∈ ↑Box.Icc J) π.boxes →
          (fun J => {i | Box.lower J i = x i}) a₁ = (fun J => {i | Box.lower J i = x i}) a₂ → a₁ = a₂
[PROOFSTEP]
simpa only [Finset.mem_filter] using π.injOn_setOf_mem_Icc_setOf_lower_eq x
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ x ∈ Prepartition.iUnion π ↔ ∃ J, J ∈ π ∧ x ∈ J
[PROOFSTEP]
convert Set.mem_iUnion₂
[GOAL]
case h.e'_2.h.e'_2.h.a
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ j, x ∈ ↑x✝
[PROOFSTEP]
rw [Box.mem_coe, exists_prop]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
h : J ≤ I
⊢ Prepartition.iUnion (single I J h) = ↑J
[PROOFSTEP]
simp [iUnion_def]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ Prepartition.iUnion ⊤ = ↑I
[PROOFSTEP]
simp [Prepartition.iUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ Prepartition.iUnion π₁ = ∅ ↔ π₁ = ⊥
[PROOFSTEP]
simp [← injective_boxes.eq_iff, Finset.ext_iff, Prepartition.iUnion, imp_false]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ π₁ ≤ π₂ ↔
    (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ π₁ ≤ π₂ →
    (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
[PROOFSTEP]
refine' fun H => ⟨fun J hJ J' hJ' Hne => _, iUnion_mono H⟩
[GOAL]
case mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : Set.Nonempty (↑J ∩ ↑J')
⊢ J ≤ J'
[PROOFSTEP]
rcases H hJ with ⟨J'', hJ'', Hle⟩
[GOAL]
case mp.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : Set.Nonempty (↑J ∩ ↑J')
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
⊢ J ≤ J'
[PROOFSTEP]
rcases Hne with ⟨x, hx, hx'⟩
[GOAL]
case mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
x : ι → ℝ
hx : x ∈ ↑J
hx' : x ∈ ↑J'
⊢ J ≤ J'
[PROOFSTEP]
rwa [π₂.eq_of_mem_of_mem hJ' hJ'' hx' (Hle hx)]
[GOAL]
case mpr
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂ →
    π₁ ≤ π₂
[PROOFSTEP]
rintro ⟨H, HU⟩ J hJ
[GOAL]
case mpr.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
HU : Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₁
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
[PROOFSTEP]
simp only [Set.subset_def, mem_iUnion] at HU 
[GOAL]
case mpr.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J, J ∈ π₁ ∧ x ∈ J) → ∃ J, J ∈ π₂ ∧ x ∈ J
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
[PROOFSTEP]
rcases HU J.upper ⟨J, hJ, J.upper_mem⟩ with ⟨J₂, hJ₂, hx⟩
[GOAL]
case mpr.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J, J ∈ π₁ ∧ x ∈ J) → ∃ J, J ∈ π₂ ∧ x ∈ J
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hx : J.upper ∈ J₂
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
[PROOFSTEP]
exact ⟨J₂, hJ₂, H _ hJ _ hJ₂ ⟨_, J.upper_mem, hx⟩⟩
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ Finset.biUnion π.boxes fun J => (πi J).boxes
⊢ J ≤ I
[PROOFSTEP]
simp only [Finset.mem_biUnion, exists_prop, mem_boxes] at hJ 
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : ∃ a, a ∈ π ∧ J ∈ πi a
⊢ J ≤ I
[PROOFSTEP]
rcases hJ with ⟨J', hJ', hJ⟩
[GOAL]
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J J' : Box ι
hJ' : J' ∈ π
hJ : J ∈ πi J'
⊢ J ≤ I
[PROOFSTEP]
exact ((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
⊢ Set.Pairwise (↑(Finset.biUnion π.boxes fun J => (πi J).boxes)) (Disjoint on Box.toSet)
[PROOFSTEP]
simp only [Set.Pairwise, Finset.mem_coe, Finset.mem_biUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
⊢ ∀ ⦃x : Box ι⦄,
    (∃ a, a ∈ π.boxes ∧ x ∈ (πi a).boxes) →
      ∀ ⦃y : Box ι⦄, (∃ a, a ∈ π.boxes ∧ y ∈ (πi a).boxes) → x ≠ y → (Disjoint on Box.toSet) x y
[PROOFSTEP]
rintro J₁' ⟨J₁, hJ₁, hJ₁'⟩ J₂' ⟨J₂, hJ₂, hJ₂'⟩ Hne
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
⊢ (Disjoint on Box.toSet) J₁' J₂'
[PROOFSTEP]
rw [Function.onFun, Set.disjoint_left]
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ ↑J₁' → ¬a ∈ ↑J₂'
[PROOFSTEP]
rintro x hx₁ hx₂
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ ↑J₁'
hx₂ : x ∈ ↑J₂'
⊢ False
[PROOFSTEP]
apply Hne
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ ↑J₁'
hx₂ : x ∈ ↑J₂'
⊢ J₁' = J₂'
[PROOFSTEP]
obtain rfl : J₁ = J₂
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' J₂ : Box ι
hJ₂ : J₂ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₂).boxes
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ ↑J₁'
hx₂ : x ∈ ↑J₂'
⊢ J₁ = J₂
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' : Box ι
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ ↑J₁'
hx₂ : x ∈ ↑J₂'
hJ₂ : J₁ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₁).boxes
⊢ J₁' = J₂'
[PROOFSTEP]
exact π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂)
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi : (J : Box ι) → Prepartition J
J₁' J₁ : Box ι
hJ₁ : J₁ ∈ π.boxes
hJ₁' : J₁' ∈ (πi J₁).boxes
J₂' : Box ι
Hne : J₁' ≠ J₂'
x : ι → ℝ
hx₁ : x ∈ ↑J₁'
hx₂ : x ∈ ↑J₂'
hJ₂ : J₁ ∈ π.boxes
hJ₂' : J₂' ∈ (πi J₁).boxes
⊢ J₁' = J₂'
[PROOFSTEP]
exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ J ∈ biUnion π πi ↔ ∃ J', J' ∈ π ∧ J ∈ πi J'
[PROOFSTEP]
simp [biUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ (biUnion π fun x => ⊤) = π
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
J✝ : Box ι
⊢ (J✝ ∈ biUnion π fun x => ⊤) ↔ J✝ ∈ π
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : π₁ = π₂
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
⊢ biUnion π₁ πi₁ = biUnion π₂ πi₂
[PROOFSTEP]
subst π₂
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
⊢ biUnion π₁ πi₁ = biUnion π₁ πi₂
[PROOFSTEP]
ext J
[GOAL]
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ J ∈ biUnion π₁ πi₁ ↔ J ∈ biUnion π₁ πi₂
[PROOFSTEP]
simp only [mem_biUnion]
[GOAL]
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J', J' ∈ π₁ ∧ J ∈ πi₁ J') ↔ ∃ J', J' ∈ π₁ ∧ J ∈ πi₂ J'
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J', J' ∈ π₁ ∧ J ∈ πi₁ J') → ∃ J', J' ∈ π₁ ∧ J ∈ πi₂ J'
[PROOFSTEP]
exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩
[GOAL]
case h.mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J', J' ∈ π₁ ∧ J ∈ πi₂ J') → ∃ J', J' ∈ π₁ ∧ J ∈ πi₁ J'
[PROOFSTEP]
exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
⊢ Prepartition.iUnion (biUnion π πi) = ⋃ (J : Box ι) (_ : J ∈ π), Prepartition.iUnion (πi J)
[PROOFSTEP]
simp [Prepartition.iUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ ∑ J in Finset.biUnion π.boxes fun J => (πi J).boxes, f J = ∑ J in π.boxes, ∑ J' in (πi J).boxes, f J'
[PROOFSTEP]
refine' Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => _
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ ↑π.boxes
J₂ : Box ι
h₂ : J₂ ∈ ↑π.boxes
hne : J₁ ≠ J₂
J' : Box ι
h₁' : J' ∈ (fun J => (πi J).boxes) J₁
h₂' : J' ∈ (fun J => (πi J).boxes) J₂
⊢ False
[PROOFSTEP]
exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ biUnionIndex π πi J ∈ π
[PROOFSTEP]
rw [biUnionIndex, dif_pos hJ]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J') ∈ π
[PROOFSTEP]
exact (π.mem_biUnion.1 hJ).choose_spec.1
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
⊢ biUnionIndex π πi J ≤ I
[PROOFSTEP]
by_cases hJ : J ∈ π.biUnion πi
[GOAL]
case pos
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ biUnion π πi
⊢ biUnionIndex π πi J ≤ I
[PROOFSTEP]
exact π.le_of_mem (π.biUnionIndex_mem hJ)
[GOAL]
case neg
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : ¬J ∈ biUnion π πi
⊢ biUnionIndex π πi J ≤ I
[PROOFSTEP]
rw [biUnionIndex, dif_neg hJ]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ J ∈ πi (biUnionIndex π πi J)
[PROOFSTEP]
convert (π.mem_biUnion.1 hJ).choose_spec.2
[GOAL]
case h.e'_2.h.e'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ biUnionIndex π πi J = Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J')
[PROOFSTEP]
exact dif_pos hJ
[GOAL]
case h.e'_3.e'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
e_2✝ : Prepartition (biUnionIndex π πi J) = Prepartition (Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J'))
⊢ biUnionIndex π πi J = Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J')
[PROOFSTEP]
exact dif_pos hJ
[GOAL]
case h.e'_5.e'_1
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
e_2✝ : Prepartition (biUnionIndex π πi J) = Prepartition (Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J'))
⊢ biUnionIndex π πi J = Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J')
[PROOFSTEP]
exact dif_pos hJ
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
⊢ (biUnion π fun J => biUnion (πi J) (πi' J)) = biUnion (biUnion π πi) fun J => πi' (biUnionIndex π πi J) J
[PROOFSTEP]
ext J
[GOAL]
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (J ∈ biUnion π fun J => biUnion (πi J) (πi' J)) ↔ J ∈ biUnion (biUnion π πi) fun J => πi' (biUnionIndex π πi J) J
[PROOFSTEP]
simp only [mem_biUnion, exists_prop]
[GOAL]
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1) ↔
    ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1) →
    ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
[PROOFSTEP]
rintro ⟨J₁, hJ₁, J₂, hJ₂, hJ⟩
[GOAL]
case h.mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
[PROOFSTEP]
refine' ⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, _⟩
[GOAL]
case h.mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ J ∈ πi' (biUnionIndex π πi J₂) J₂
[PROOFSTEP]
rwa [π.biUnionIndex_of_mem hJ₁ hJ₂]
[GOAL]
case h.mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J') →
    ∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1
[PROOFSTEP]
rintro ⟨J₁, ⟨J₂, hJ₂, hJ₁⟩, hJ⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (biUnionIndex π πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ ∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1
[PROOFSTEP]
refine' ⟨J₂, hJ₂, J₁, hJ₁, _⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (biUnionIndex π πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ J ∈ πi' J₂ J₁
[PROOFSTEP]
rwa [π.biUnionIndex_of_mem hJ₂ hJ₁] at hJ 
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
J : Box ι
hJ : J ∈ ↑eraseNone boxes
⊢ J ≤ I
[PROOFSTEP]
rw [mem_eraseNone] at hJ 
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
J : Box ι
hJ : some J ∈ boxes
⊢ J ≤ I
[PROOFSTEP]
simpa only [WithBot.some_eq_coe, WithBot.coe_le_coe] using le_of_mem _ hJ
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
J₁ : Box ι
h₁ : J₁ ∈ ↑(↑eraseNone boxes)
J₂ : Box ι
h₂ : J₂ ∈ ↑(↑eraseNone boxes)
hne : J₁ ≠ J₂
⊢ (Disjoint on Box.toSet) J₁ J₂
[PROOFSTEP]
simp only [mem_coe, mem_eraseNone] at h₁ h₂ 
[GOAL]
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
J₁ J₂ : Box ι
hne : J₁ ≠ J₂
h₁ : some J₁ ∈ boxes
h₂ : some J₂ ∈ boxes
⊢ (Disjoint on Box.toSet) J₁ J₂
[PROOFSTEP]
exact Box.disjoint_coe.1 (pairwise_disjoint h₁ h₂ (mt Option.some_inj.1 hne))
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
⊢ Prepartition.iUnion (ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
[PROOFSTEP]
suffices ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by simpa [ofWithBot, Prepartition.iUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
this : ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
⊢ Prepartition.iUnion (ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
[PROOFSTEP]
simpa [ofWithBot, Prepartition.iUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
⊢ ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
[PROOFSTEP]
simp only [← Box.biUnion_coe_eq_coe, @iUnion_comm _ _ (Box ι), @iUnion_comm _ _ (@Eq _ _ _), iUnion_iUnion_eq_right]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
[PROOFSTEP]
have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
  simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
J : Box ι
hJ : ↑J ∈ boxes
⊢ ∃ J', J' ∈ π ∧ J ≤ J'
[PROOFSTEP]
simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J', J' ∈ π ∧ J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
[PROOFSTEP]
simpa [ofWithBot, le_def]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
⊢ π ≤ ofWithBot boxes le_of_mem pairwise_disjoint
[PROOFSTEP]
intro J hJ
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
[PROOFSTEP]
rcases H J hJ with ⟨J', J'mem, hle⟩
[GOAL]
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : ↑J ≤ J'
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
[PROOFSTEP]
lift J' to Box ι using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle
[GOAL]
case intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : ↑J' ∈ boxes
hle : ↑J ≤ ↑J'
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
[PROOFSTEP]
exact ⟨J', mem_ofWithBot.2 J'mem, WithBot.coe_le_coe.1 hle⟩
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
J' : WithBot (Box ι)
hJ' : J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes
⊢ J' ≤ ↑J
[PROOFSTEP]
rcases Finset.mem_image.1 hJ' with ⟨J', -, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J' : Box ι
hJ' : ↑J ⊓ ↑J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes
⊢ ↑J ⊓ ↑J' ≤ ↑J
[PROOFSTEP]
exact inf_le_left
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
⊢ Set.Pairwise (↑(Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes)) Disjoint
[PROOFSTEP]
simp only [Set.Pairwise, onFun, Finset.mem_coe, Finset.mem_image]
[GOAL]
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
⊢ ∀ ⦃x : WithBot (Box ι)⦄,
    (∃ a, a ∈ π.boxes ∧ ↑J ⊓ ↑a = x) → ∀ ⦃y : WithBot (Box ι)⦄, (∃ a, a ∈ π.boxes ∧ ↑J ⊓ ↑a = y) → x ≠ y → Disjoint x y
[PROOFSTEP]
rintro _ ⟨J₁, h₁, rfl⟩ _ ⟨J₂, h₂, rfl⟩ Hne
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : ↑J ⊓ ↑J₁ ≠ ↑J ⊓ ↑J₂
⊢ Disjoint (↑J ⊓ ↑J₁) (↑J ⊓ ↑J₂)
[PROOFSTEP]
have : J₁ ≠ J₂ := by
  rintro rfl
  exact Hne rfl
[GOAL]
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : ↑J ⊓ ↑J₁ ≠ ↑J ⊓ ↑J₂
⊢ J₁ ≠ J₂
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
I J✝ J₁✝ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ h₂ : J₁ ∈ π.boxes
Hne : ↑J ⊓ ↑J₁ ≠ ↑J ⊓ ↑J₁
⊢ False
[PROOFSTEP]
exact Hne rfl
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J J₁ : Box ι
h₁ : J₁ ∈ π.boxes
J₂ : Box ι
h₂ : J₂ ∈ π.boxes
Hne : ↑J ⊓ ↑J₁ ≠ ↑J ⊓ ↑J₂
this : J₁ ≠ J₂
⊢ Disjoint (↑J ⊓ ↑J₁) (↑J ⊓ ↑J₂)
[PROOFSTEP]
exact ((Box.disjoint_coe.2 <| π.disjoint_coe_of_mem h₁ h₂ this).inf_left' _).inf_right' _
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ J₁ ∈ restrict π J ↔ ∃ J', J' ∈ π ∧ ↑J₁ = ↑J ⊓ ↑J'
[PROOFSTEP]
simp [restrict, eq_comm]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ J₁ ∈ restrict π J ↔ ∃ J', J' ∈ π ∧ ↑J₁ = ↑J ∩ ↑J'
[PROOFSTEP]
simp only [mem_restrict, ← Box.withBotCoe_inj, Box.coe_inf, Box.coe_coe]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ restrict π₁ J ≤ restrict π₂ J
[PROOFSTEP]
refine' ofWithBot_mono fun J₁ hJ₁ hne => _
[GOAL]
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : J₁ ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₁.boxes
hne : J₁ ≠ ⊥
⊢ ∃ J', J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes ∧ J₁ ≤ J'
[PROOFSTEP]
rw [Finset.mem_image] at hJ₁ 
[GOAL]
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a, a ∈ π₁.boxes ∧ ↑J ⊓ ↑a = J₁
hne : J₁ ≠ ⊥
⊢ ∃ J', J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes ∧ J₁ ≤ J'
[PROOFSTEP]
rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes ∧ ↑J ⊓ ↑J₁ ≤ J'
[PROOFSTEP]
rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hle : J₁ ≤ J₂
⊢ ∃ J', J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes ∧ ↑J ⊓ ↑J₁ ≤ J'
[PROOFSTEP]
exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
h : I ≤ J
⊢ (restrict π J).boxes = π.boxes
[PROOFSTEP]
simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
h : I ≤ J
⊢ Finset.biUnion (Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes) Option.toFinset = π.boxes
[PROOFSTEP]
refine' Finset.image_biUnion.trans _
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
h : I ≤ J
⊢ (Finset.biUnion π.boxes fun a => Option.toFinset (↑J ⊓ ↑a)) = π.boxes
[PROOFSTEP]
refine' (Finset.biUnion_congr rfl _).trans Finset.biUnion_singleton_eq_self
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
h : I ≤ J
⊢ ∀ (a : Box ι), a ∈ π.boxes → Option.toFinset (↑J ⊓ ↑a) = {a}
[PROOFSTEP]
intro J' hJ'
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ Option.toFinset (↑J ⊓ ↑J') = {J'}
[PROOFSTEP]
rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ ↑J' ≤ ↑J
[PROOFSTEP]
exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ Prepartition.iUnion (restrict π J) = ↑J ∩ Prepartition.iUnion π
[PROOFSTEP]
simp [restrict, ← inter_iUnion, ← iUnion_def]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ restrict (biUnion π πi) J = πi J
[PROOFSTEP]
refine' (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => _) _).symm
[GOAL]
case refine'_1
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ (restrict (biUnion π πi) J).boxes
[PROOFSTEP]
refine' (mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right _).symm⟩
[GOAL]
case refine'_1
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ ↑J₁ ≤ ↑J
[PROOFSTEP]
exact WithBot.coe_le_coe.2 (le_of_mem _ h₁)
[GOAL]
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ Prepartition.iUnion (restrict (biUnion π πi) J) ⊆ Prepartition.iUnion (πi J)
[PROOFSTEP]
simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]
[GOAL]
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ∀ (x : ι → ℝ), (x ∈ ↑J ∧ ∃ i i_1, x ∈ Prepartition.iUnion (πi i)) → x ∈ Prepartition.iUnion (πi J)
[PROOFSTEP]
rintro x ⟨hxJ, J₁, h₁, hx⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ Prepartition.iUnion (πi J₁)
⊢ x ∈ Prepartition.iUnion (πi J)
[PROOFSTEP]
obtain rfl : J = J₁
[GOAL]
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ Prepartition.iUnion (πi J₁)
⊢ J = J₁
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ Prepartition.iUnion (πi J)
⊢ x ∈ Prepartition.iUnion (πi J)
[PROOFSTEP]
exact π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ Prepartition.iUnion (πi J)
⊢ x ∈ Prepartition.iUnion (πi J)
[PROOFSTEP]
exact hx
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ biUnion π πi ≤ π' ↔ ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ biUnion π πi ≤ π' → ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
[PROOFSTEP]
intro H J hJ
[GOAL]
case mpr
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J) → biUnion π πi ≤ π'
[PROOFSTEP]
intro H J hJ
[GOAL]
case mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : biUnion π πi ≤ π'
J : Box ι
hJ : J ∈ π
⊢ πi J ≤ restrict π' J
[PROOFSTEP]
rw [← π.restrict_biUnion πi hJ]
[GOAL]
case mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : biUnion π πi ≤ π'
J : Box ι
hJ : J ∈ π
⊢ restrict (biUnion π πi) J ≤ restrict π' J
[PROOFSTEP]
exact restrict_mono H
[GOAL]
case mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J : Box ι
hJ : J ∈ biUnion π πi
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
[PROOFSTEP]
rw [mem_biUnion] at hJ 
[GOAL]
case mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J : Box ι
hJ : ∃ J', J' ∈ π ∧ J ∈ πi J'
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
[PROOFSTEP]
rcases hJ with ⟨J₁, h₁, hJ⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
[PROOFSTEP]
rcases H J₁ h₁ hJ with ⟨J₂, h₂, Hle⟩
[GOAL]
case mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ restrict π' J₁
Hle : J ≤ J₂
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
[PROOFSTEP]
rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, H⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H✝ : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ restrict π' J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : ↑J₂ = ↑J₁ ⊓ ↑J₃
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
[PROOFSTEP]
exact ⟨J₃, h₃, Hle.trans <| WithBot.coe_le_coe.1 <| H.trans_le inf_le_right⟩
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π' ≤ biUnion π πi ↔ π' ≤ π ∧ ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
[PROOFSTEP]
refine' ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun J hJ => _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ biUnion π πi
J : Box ι
hJ : J ∈ π
⊢ restrict π' J ≤ πi J
[PROOFSTEP]
rw [← π.restrict_biUnion πi hJ]
[GOAL]
case refine'_1
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ biUnion π πi
J : Box ι
hJ : J ∈ π
⊢ restrict π' J ≤ restrict (biUnion π πi) J
[PROOFSTEP]
exact restrict_mono H
[GOAL]
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J) → π' ≤ biUnion π πi
[PROOFSTEP]
rintro ⟨H, Hi⟩ J' hJ'
[GOAL]
case refine'_2.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
[PROOFSTEP]
rcases H hJ' with ⟨J, hJ, hle⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
[PROOFSTEP]
have : J' ∈ π'.restrict J := π'.mem_restrict.2 ⟨J', hJ', (inf_of_le_right <| WithBot.coe_le_coe.2 hle).symm⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ restrict π' J
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
[PROOFSTEP]
rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ restrict π' J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
[PROOFSTEP]
exact ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
⊢ J ∈ π₁ ⊓ π₂ ↔ ∃ J₁, J₁ ∈ π₁ ∧ ∃ J₂, J₂ ∈ π₂ ∧ ↑J = ↑J₁ ⊓ ↑J₂
[PROOFSTEP]
simp only [inf_def, mem_biUnion, mem_restrict]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
⊢ Prepartition.iUnion (π₁ ⊓ π₂) = Prepartition.iUnion π₁ ∩ Prepartition.iUnion π₂
[PROOFSTEP]
simp only [inf_def, iUnion_biUnion, iUnion_restrict, ← iUnion_inter, ← iUnion_def]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
p : Box ι → Prop
hp : ∀ (J : Box ι), J ∈ π → p J
⊢ filter π p = π
[PROOFSTEP]
ext J
[GOAL]
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
p : Box ι → Prop
hp : ∀ (J : Box ι), J ∈ π → p J
J : Box ι
⊢ J ∈ filter π p ↔ J ∈ π
[PROOFSTEP]
simpa using hp J
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
⊢ Prepartition.iUnion (filter π fun J => ¬p J) = Prepartition.iUnion π \ Prepartition.iUnion (filter π p)
[PROOFSTEP]
simp only [Prepartition.iUnion]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
⊢ ⋃ (J : Box ι) (_ : J ∈ filter π fun J => ¬p J), ↑J =
    (⋃ (J : Box ι) (_ : J ∈ π), ↑J) \ ⋃ (J : Box ι) (_ : J ∈ filter π p), ↑J
[PROOFSTEP]
convert (@Set.biUnion_diff_biUnion_eq _ (Box ι) π.boxes (π.filter p).boxes (↑) _).symm
[GOAL]
case h.e'_2.h.e'_3.h.pq.a.a
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
x✝ : Box ι
⊢ (x✝ ∈ filter π fun J => ¬p J) ↔ x✝ ∈ ↑π.boxes \ ↑(filter π p).boxes
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
⊢ PairwiseDisjoint (↑π.boxes ∪ ↑(filter π p).boxes) Box.toSet
[PROOFSTEP]
rw [Set.PairwiseDisjoint]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
⊢ Set.Pairwise (↑π.boxes ∪ ↑(filter π p).boxes) (Disjoint on Box.toSet)
[PROOFSTEP]
convert π.pairwiseDisjoint
[GOAL]
case h.e'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
⊢ ↑π.boxes ∪ ↑(filter π p).boxes = ↑π.boxes
[PROOFSTEP]
rw [Set.union_eq_left_iff_subset, filter_boxes, coe_filter]
[GOAL]
case h.e'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
p : Box ι → Prop
⊢ {x | x ∈ π.boxes ∧ p x} ⊆ ↑π.boxes
[PROOFSTEP]
exact fun _ ⟨h, _⟩ => h
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
α : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ ∑ y in Finset.image f π.boxes, ∑ J in (filter π fun J => f J = y).boxes, g J = ∑ J in π.boxes, g J
[PROOFSTEP]
convert sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
h : Disjoint (Prepartition.iUnion π₁) (Prepartition.iUnion π₂)
this : ∀ (J₁ : Box ι), J₁ ∈ π₁ → ∀ (J₂ : Box ι), J₂ ∈ π₂ → J₁ ≠ J₂ → Disjoint ↑J₁ ↑J₂
⊢ Set.Pairwise (↑(π₁.boxes ∪ π₂.boxes)) (Disjoint on Box.toSet)
[PROOFSTEP]
simpa [pairwise_union_of_symmetric (symmetric_disjoint.comap _), pairwiseDisjoint]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : Disjoint (Prepartition.iUnion π₁) (Prepartition.iUnion π₂)
⊢ Prepartition.iUnion (disjUnion π₁ π₂ h) = Prepartition.iUnion π₁ ∪ Prepartition.iUnion π₂
[PROOFSTEP]
simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
⊢ IsPartition π ↔ Prepartition.iUnion π = ↑I
[PROOFSTEP]
simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and_iff, Set.subset_def, mem_iUnion, Box.mem_coe]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : J ≤ I
⊢ IsPartition (single I J h) ↔ J = I
[PROOFSTEP]
simp [isPartition_iff_iUnion_eq]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : IsPartition π
hx : x ∈ I
⊢ ∃! J x_1, x ∈ J
[PROOFSTEP]
rcases h x hx with ⟨J, h, hx⟩
[GOAL]
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h✝ : IsPartition π
hx✝ : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J x_1, x ∈ J
[PROOFSTEP]
exact ExistsUnique.intro₂ J h hx fun J' h' hx' => π.eq_of_mem_of_mem h' h hx' hx
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : IsPartition π
hJ : J ≤ I
⊢ Prepartition.iUnion (restrict π J) = ↑J
[PROOFSTEP]
simp [h.iUnion_eq, hJ]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h₁ : IsPartition π₁
h₂ : IsPartition π₂
⊢ Prepartition.iUnion (π₁ ⊓ π₂) = ↑I
[PROOFSTEP]
simp [h₁.iUnion_eq, h₂.iUnion_eq]
[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : Prepartition.iUnion π₂ = ↑I \ Prepartition.iUnion π₁
⊢ Prepartition.iUnion π₁ ∪ Prepartition.iUnion π₂ = ↑I
[PROOFSTEP]
simp [h, π₁.iUnion_subset]
