[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π : TaggedPrepartition I
x : ι → ℝ
⊢ x ∈ 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 ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ j, x ∈ ↑x✝
[PROOFSTEP]
rw [Box.mem_coe, mem_toPrepartition, exists_prop]
[GOAL]
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' = TaggedPrepartition.tag (πi J) J'
[PROOFSTEP]
rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']
[GOAL]
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' =
    TaggedPrepartition.tag (πi (biUnionIndex π (fun J => (πi J).toPrepartition) J')) J'
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), J ∈ biUnionTagged π πi → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
simp only [mem_biUnionTagged]
[GOAL]
ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
refine' ⟨fun H J hJ J' hJ' => _, fun H J' ⟨J, hJ, hJ'⟩ => _⟩
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
rw [← π.tag_biUnionTagged hJ hJ']
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
[PROOFSTEP]
exact H J' ⟨J, hJ, hJ'⟩
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
[PROOFSTEP]
rw [π.tag_biUnionTagged hJ hJ']
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
exact H J hJ J' hJ'
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
⊢ J ∈ infPrepartition π₁ π₂.toPrepartition ↔ J ∈ infPrepartition π₂ π₁.toPrepartition
[PROOFSTEP]
simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
x : ι → ℝ
⊢ Finset.card (Finset.filter (fun J => tag π J = x) π.boxes) ≤
    Finset.card (Finset.filter (fun J => x ∈ ↑Box.Icc J) π.boxes)
[PROOFSTEP]
refine' Finset.card_le_of_subset fun J hJ => _
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
x : ι → ℝ
J : Box ι
hJ : J ∈ Finset.filter (fun J => tag π J = x) π.boxes
⊢ J ∈ Finset.filter (fun J => x ∈ ↑Box.Icc J) π.boxes
[PROOFSTEP]
rw [Finset.mem_filter] at hJ ⊢
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ tag π J = x
⊢ J ∈ π.boxes ∧ x ∈ ↑Box.Icc J
[PROOFSTEP]
rcases hJ with ⟨hJ, rfl⟩
[GOAL]
case intro
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
J : Box ι
hJ : J ∈ π.boxes
⊢ J ∈ π.boxes ∧ tag π J ∈ ↑Box.Icc J
[PROOFSTEP]
exact ⟨hJ, h J hJ⟩
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : x ∈ ↑Box.Icc I
⊢ (∀ (J' : Box ι), J' ∈ single I J hJ x h → p (tag (single I J hJ x h) J') J') ↔ p x J
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
⊢ Finset.piecewise π₁.boxes π₁.tag π₂.tag J ∈ ↑Box.Icc I
[PROOFSTEP]
dsimp only [Finset.piecewise]
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
⊢ (if J ∈ π₁.boxes then tag π₁ J else tag π₂ J) ∈ ↑Box.Icc I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
h✝ : J ∈ π₁.boxes
⊢ tag π₁ J ∈ ↑Box.Icc I
case neg
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
h✝ : ¬J ∈ π₁.boxes
⊢ tag π₂ J ∈ ↑Box.Icc I
[PROOFSTEP]
exacts [π₁.tag_mem_Icc J, π₂.tag_mem_Icc J]
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
⊢ IsSubordinate (TaggedPrepartition.disjUnion π₁ π₂ h) r
[PROOFSTEP]
refine' fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => _) fun hJ => _
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
[PROOFSTEP]
rw [disjUnion_tag_of_mem_left _ hJ]
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₁ J) ↑(r (tag π₁ J))
[PROOFSTEP]
exact h₁ _ hJ
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
[PROOFSTEP]
rw [disjUnion_tag_of_mem_right _ hJ]
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₂ J) ↑(r (tag π₂ J))
[PROOFSTEP]
exact h₂ _ hJ
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
⊢ IsHenstock (TaggedPrepartition.disjUnion π₁ π₂ h)
[PROOFSTEP]
refine' fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => _) fun hJ => _
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc J
[PROOFSTEP]
rw [disjUnion_tag_of_mem_left _ hJ]
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag π₁ J ∈ ↑Box.Icc J
[PROOFSTEP]
exact h₁ _ hJ
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc J
[PROOFSTEP]
rw [disjUnion_tag_of_mem_right _ hJ]
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag π₂ J ∈ ↑Box.Icc J
[PROOFSTEP]
exact h₂ _ hJ
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
I J : Box ι
h : I ≤ J
⊢ Injective fun π =>
    {
      toPrepartition :=
        { boxes := π.boxes, le_of_mem' := (_ : ∀ (J' : Box ι), J' ∈ π.boxes → J' ≤ J),
          pairwiseDisjoint := (_ : Set.Pairwise (↑π.boxes) (Disjoint on Box.toSet)) },
      tag := π.tag, tag_mem_Icc := (_ : ∀ (J_1 : Box ι), tag π J_1 ∈ ↑Box.Icc J) }
[PROOFSTEP]
rintro ⟨⟨b₁, h₁le, h₁d⟩, t₁, ht₁⟩ ⟨⟨b₂, h₂le, h₂d⟩, t₂, ht₂⟩ H
[GOAL]
case mk.mk.mk.mk
ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
I J : Box ι
h : I ≤ J
t₁ : Box ι → ι → ℝ
ht₁ : ∀ (J : Box ι), t₁ J ∈ ↑Box.Icc I
b₁ : Finset (Box ι)
h₁le : ∀ (J : Box ι), J ∈ b₁ → J ≤ I
h₁d : Set.Pairwise (↑b₁) (Disjoint on Box.toSet)
t₂ : Box ι → ι → ℝ
ht₂ : ∀ (J : Box ι), t₂ J ∈ ↑Box.Icc I
b₂ : Finset (Box ι)
h₂le : ∀ (J : Box ι), J ∈ b₂ → J ≤ I
h₂d : Set.Pairwise (↑b₂) (Disjoint on Box.toSet)
H :
  (fun π =>
        {
          toPrepartition :=
            { boxes := π.boxes, le_of_mem' := (_ : ∀ (J' : Box ι), J' ∈ π.boxes → J' ≤ J),
              pairwiseDisjoint := (_ : Set.Pairwise (↑π.boxes) (Disjoint on Box.toSet)) },
          tag := π.tag, tag_mem_Icc := (_ : ∀ (J_1 : Box ι), tag π J_1 ∈ ↑Box.Icc J) })
      { toPrepartition := { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d }, tag := t₁,
        tag_mem_Icc := ht₁ } =
    (fun π =>
        {
          toPrepartition :=
            { boxes := π.boxes, le_of_mem' := (_ : ∀ (J' : Box ι), J' ∈ π.boxes → J' ≤ J),
              pairwiseDisjoint := (_ : Set.Pairwise (↑π.boxes) (Disjoint on Box.toSet)) },
          tag := π.tag, tag_mem_Icc := (_ : ∀ (J_1 : Box ι), tag π J_1 ∈ ↑Box.Icc J) })
      { toPrepartition := { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d }, tag := t₂, tag_mem_Icc := ht₂ }
⊢ { toPrepartition := { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d }, tag := t₁, tag_mem_Icc := ht₁ } =
    { toPrepartition := { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d }, tag := t₂, tag_mem_Icc := ht₂ }
[PROOFSTEP]
simpa using H
