[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
⊢ Henstock ≤ Riemann
[PROOFSTEP]
trivial
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
⊢ Henstock ≤ McShane
[PROOFSTEP]
trivial
[GOAL]
ι✝ : Type u_1
inst✝ : Fintype ι✝
I J : Box ι✝
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ : IntegrationParams
ι : Type u_2
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ RCond l r
[PROOFSTEP]
simp [RCond, hl]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
wlog hc : c₁ ≤ c₂ with H
[GOAL]
case inr
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
H :
  ∀ {ι : Type u_1} [inst : Fintype ι] {I : Box ι} {J : Box ι} {c : ℝ≥0} {c₁ c₂ : ℝ≥0} {r : (ι → ℝ) → ↑(Set.Ioi 0)}
    {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π : TaggedPrepartition I} {π₁ π₂ : TaggedPrepartition I} {l : IntegrationParams}
    {l₁ l₂ : IntegrationParams},
    MemBaseSet l I c₁ r₁ π₁ →
      MemBaseSet l I c₂ r₂ π₂ →
        TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂ →
          c₁ ≤ c₂ →
            ∃ π,
              Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
                (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧
                  (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
hc : ¬c₁ ≤ c₂
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
simpa [hU, _root_.and_comm] using @H _ _ I J c c₂ c₁ r r₂ r₁ π π₂ π₁ _ l₂ l₁ h₂ h₁ hU.symm (le_of_not_le hc)
[GOAL]
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
by_cases hD : (l.bDistortion : Prop)
[GOAL]
case pos
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
hD : l.bDistortion = true
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
rcases h₁.4 hD with ⟨π, hπU, hπc⟩
[GOAL]
case pos.intro.intro
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
hD : l.bDistortion = true
π : Prepartition I
hπU : Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁
hπc : Prepartition.distortion π ≤ c₁
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
exact ⟨π, hπU, fun _ => hπc, fun _ => hπc.trans hc⟩
[GOAL]
case neg
ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ : IntegrationParams
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
h₁ : MemBaseSet l I c₁ r₁ π₁
h₂ : MemBaseSet l I c₂ r₂ π₂
hU : TaggedPrepartition.iUnion π₁ = TaggedPrepartition.iUnion π₂
hc : c₁ ≤ c₂
hD : ¬l.bDistortion = true
⊢ ∃ π,
    Prepartition.iUnion π = ↑I \ TaggedPrepartition.iUnion π₁ ∧
      (l.bDistortion = true → Prepartition.distortion π ≤ c₁) ∧ (l.bDistortion = true → Prepartition.distortion π ≤ c₂)
[PROOFSTEP]
exact ⟨π₁.toPrepartition.compl, π₁.toPrepartition.iUnion_compl, fun h => (hD h).elim, fun h => (hD h).elim⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ₁ : MemBaseSet l I c r₁ π₁
hle : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → r₂ x ≤ r₁ x
π₂ : Prepartition I
hU : Prepartition.iUnion π₂ = ↑I \ TaggedPrepartition.iUnion π₁
hc : l.bDistortion = true → Prepartition.distortion π₂ ≤ c
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion ⊥ = ↑I \ TaggedPrepartition.iUnion (unionComplToSubordinate π₁ π₂ hU r₂) ∧
    Prepartition.distortion ⊥ ≤ c
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
⊢ MemBaseSet l I c r (TaggedPrepartition.filter π p)
[PROOFSTEP]
refine'
  ⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1, fun hD =>
    (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => _⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
set π₂ := π.filter fun J => ¬p J
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
have : Disjoint π₁.iUnion π₂.iUnion := by simpa [hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
⊢ Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
[PROOFSTEP]
simpa [hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
refine' ⟨π₁.disjUnion π₂.toPrepartition this, _, _⟩
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ Prepartition.iUnion (Prepartition.disjUnion π₁ π₂.toPrepartition this) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by simp [*]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this✝ : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
this :
  ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
⊢ Prepartition.iUnion (Prepartition.disjUnion π₁ π₂.toPrepartition this✝) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
simp [*]
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
have h : (π.filter p).iUnion ⊆ π.iUnion := biUnion_subset_biUnion_left (Finset.filter_subset _ _)
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
⊢ ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) =
    ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.refine'_1.h
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
⊢ x ∈
      ↑I \ TaggedPrepartition.iUnion π ∪
        TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ↔
    x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
fconstructor
[GOAL]
case intro.intro.refine'_1.h.mp
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
⊢ x ∈
      ↑I \ TaggedPrepartition.iUnion π ∪
        TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) →
    x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
[GOAL]
case intro.intro.refine'_1.h.mp.inl.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxπ : ¬x ∈ TaggedPrepartition.iUnion π
⊢ x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
case intro.intro.refine'_1.h.mp.inr.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxπ : x ∈ TaggedPrepartition.iUnion π
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
⊢ x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
[GOAL]
case intro.intro.refine'_1.h.mpr
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
⊢ x ∈ ↑I \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) →
    x ∈
      ↑I \ TaggedPrepartition.iUnion π ∪
        TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
rintro ⟨hxI, hxp⟩
[GOAL]
case intro.intro.refine'_1.h.mpr.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
⊢ x ∈
    ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
by_cases hxπ : x ∈ π.iUnion
[GOAL]
case pos
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
hxπ : x ∈ TaggedPrepartition.iUnion π
⊢ x ∈
    ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
case neg
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
h : TaggedPrepartition.iUnion (TaggedPrepartition.filter π p) ⊆ TaggedPrepartition.iUnion π
x : ι → ℝ
hxI : x ∈ ↑I
hxp : ¬x ∈ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
hxπ : ¬x ∈ TaggedPrepartition.iUnion π
⊢ x ∈
    ↑I \ TaggedPrepartition.iUnion π ∪
      TaggedPrepartition.iUnion π \ TaggedPrepartition.iUnion (TaggedPrepartition.filter π p)
[PROOFSTEP]
exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
⊢ Prepartition.distortion (Prepartition.disjUnion π₁ π₂.toPrepartition this) ≤ c
[PROOFSTEP]
have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
hπ : MemBaseSet l I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : Prepartition.iUnion π₁ = ↑I \ TaggedPrepartition.iUnion π
hc : Prepartition.distortion π₁ ≤ c
π₂ : TaggedPrepartition I := TaggedPrepartition.filter π fun J => ¬p J
this✝ : Disjoint (Prepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
this : distortion (TaggedPrepartition.filter π fun J => ¬p J) ≤ c
⊢ Prepartition.distortion (Prepartition.disjUnion π₁ π₂.toPrepartition this✝) ≤ c
[PROOFSTEP]
simpa [hc]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
⊢ MemBaseSet l I c r (Prepartition.biUnionTagged π πi)
[PROOFSTEP]
refine'
  ⟨TaggedPrepartition.isSubordinate_biUnionTagged.2 fun J hJ => (h J hJ).1, fun hH =>
    TaggedPrepartition.isHenstock_biUnionTagged.2 fun J hJ => (h J hJ).2 hH, fun hD => _, fun hD => _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ distortion (Prepartition.biUnionTagged π πi) ≤ c
[PROOFSTEP]
rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∀ (b : Box ι), b ∈ π.boxes → distortion (πi b) ≤ c
[PROOFSTEP]
exact fun J hJ => (h J hJ).3 hD
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi) ∧
      Prepartition.distortion π' ≤ c
[PROOFSTEP]
refine' ⟨_, _, hc hD⟩
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ Prepartition.iUnion (Prepartition.compl π) = ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
[PROOFSTEP]
rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l l₁ l₂ : IntegrationParams
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ (J : Box ι), J ∈ π → MemBaseSet l J c r (πi J)
hp : ∀ (J : Box ι), J ∈ π → IsPartition (πi J)
hc : l.bDistortion = true → Prepartition.distortion (Prepartition.compl π) ≤ c
hD : l.bDistortion = true
⊢ ↑I \ Prepartition.iUnion (Prepartition.biUnion π fun J => (πi J).toPrepartition) =
    ↑I \ TaggedPrepartition.iUnion (Prepartition.biUnionTagged π πi)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁✝ π₂✝ : TaggedPrepartition I✝
l✝ l₁ l₂ : IntegrationParams
I : Box ι
l : IntegrationParams
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ toFilteriUnion l I π₁ = toFilteriUnion l I π₂
[PROOFSTEP]
simp only [toFilteriUnion, toFilterDistortioniUnion, h]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ HasBasis (toFilteriUnion l I π₀) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
π₀ : Prepartition I
this :
  ∀ (c : ℝ≥0),
    HasBasis (toFilterDistortioniUnion l I c π₀) (RCond l) fun r =>
      {π | MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
⊢ HasBasis (toFilteriUnion l I π₀) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
simpa only [setOf_and, setOf_exists] using hasBasis_iSup this
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
⊢ HasBasis (toFilteriUnion l I ⊤) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ IsPartition π}
[PROOFSTEP]
simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using l.hasBasis_toFilteriUnion I ⊤
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
⊢ HasBasis (toFilter l I) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r => {π | ∃ c, MemBaseSet l I c (r c) π}
[PROOFSTEP]
simpa only [setOf_exists] using hasBasis_iSup (l.hasBasis_toFilterDistortion I)
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
⊢ Tendsto (↑(embedBox I J h)) (toFilteriUnion l I ⊤) (toFilteriUnion l J (Prepartition.single J I h))
[PROOFSTEP]
simp only [toFilteriUnion, tendsto_iSup]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
⊢ ∀ (i : ℝ≥0),
    Tendsto (↑(embedBox I J h)) (toFilterDistortioniUnion l I i ⊤)
      (⨆ (c : ℝ≥0), toFilterDistortioniUnion l J c (Prepartition.single J I h))
[PROOFSTEP]
intro c
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
⊢ Tendsto (↑(embedBox I J h)) (toFilterDistortioniUnion l I c ⊤)
    (⨆ (c : ℝ≥0), toFilterDistortioniUnion l J c (Prepartition.single J I h))
[PROOFSTEP]
set π₀ := Prepartition.single J I h
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Tendsto (↑(embedBox I J h)) (toFilterDistortioniUnion l I c ⊤) (⨆ (c : ℝ≥0), toFilterDistortioniUnion l J c π₀)
[PROOFSTEP]
refine' le_iSup_of_le (max c π₀.compl.distortion) _
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Filter.map (↑(embedBox I J h)) (toFilterDistortioniUnion l I c ⊤) ≤
    toFilterDistortioniUnion l J (max c (Prepartition.distortion (Prepartition.compl π₀))) π₀
[PROOFSTEP]
refine'
  ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => _
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
⊢ ∃ ia,
    RCond l ia ∧
      ∀ (x : TaggedPrepartition I),
        x ∈ {π | MemBaseSet l I c ia π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion ⊤} →
          ↑(embedBox I J h) x ∈
            {π |
              MemBaseSet l J (max c (Prepartition.distortion (Prepartition.compl π₀))) r π ∧
                TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
refine' ⟨r, hr, fun π hπ => _⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : π ∈ {π | MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion ⊤}
⊢ ↑(embedBox I J h) π ∈
    {π |
      MemBaseSet l J (max c (Prepartition.distortion (Prepartition.compl π₀))) r π ∧
        TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ 
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
⊢ ↑(embedBox I J h) π ∈
    {π |
      MemBaseSet l J (max c (Prepartition.distortion (Prepartition.compl π₀))) r π ∧
        TaggedPrepartition.iUnion π = Prepartition.iUnion π₀}
[PROOFSTEP]
refine' ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
x✝ : l.bDistortion = true
⊢ ∃ π',
    Prepartition.iUnion π' = ↑J \ TaggedPrepartition.iUnion (↑(embedBox I J h) π) ∧
      Prepartition.distortion π' ≤ max c (Prepartition.distortion (Prepartition.compl π₀))
[PROOFSTEP]
refine' ⟨_, π₀.iUnion_compl.trans _, le_max_right _ _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
x✝ : l.bDistortion = true
⊢ ↑J \ Prepartition.iUnion π₀ = ↑J \ TaggedPrepartition.iUnion (↑(embedBox I J h) π)
[PROOFSTEP]
congr 1
[GOAL]
case refine'_1.e_a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion π₀ = TaggedPrepartition.iUnion (↑(embedBox I J h) π)
[PROOFSTEP]
exact (Prepartition.iUnion_single h).trans hπ.2.symm
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c✝ c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : RCond l r
π : TaggedPrepartition I
hπ : MemBaseSet l I c r π ∧ TaggedPrepartition.iUnion π = ↑I
⊢ TaggedPrepartition.iUnion (↑(embedBox I J h) π) = Prepartition.iUnion π₀
[PROOFSTEP]
exact hπ.2.trans (Prepartition.iUnion_single _).symm
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
π₀ : Prepartition I
hc₁ : Prepartition.distortion π₀ ≤ c
hc₂ : Prepartition.distortion (Prepartition.compl π₀) ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ π.toPrepartition ≤ π₀ ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
[PROOFSTEP]
rcases π₀.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r with ⟨π, hle, hH, hr, hd, hU⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
π₀ : Prepartition I
hc₁ : Prepartition.distortion π₀ ≤ c
hc₂ : Prepartition.distortion (Prepartition.compl π₀) ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : IsHenstock π
hr : IsSubordinate π r
hd : distortion π = Prepartition.distortion π₀
hU : TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
⊢ ∃ π, MemBaseSet l I c r π ∧ π.toPrepartition ≤ π₀ ∧ TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
[PROOFSTEP]
refine' ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, _, hc₂⟩⟩, ⟨hle, hU⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π✝ π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ l : IntegrationParams
π₀ : Prepartition I
hc₁ : Prepartition.distortion π₀ ≤ c
hc₂ : Prepartition.distortion (Prepartition.compl π₀) ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : IsHenstock π
hr : IsSubordinate π r
hd : distortion π = Prepartition.distortion π₀
hU : TaggedPrepartition.iUnion π = Prepartition.iUnion π₀
x✝ : l.bDistortion = true
⊢ Prepartition.iUnion (Prepartition.compl π₀) = ↑I \ TaggedPrepartition.iUnion π
[PROOFSTEP]
exact Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Box.distortion I ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
[PROOFSTEP]
rw [← Prepartition.distortion_top] at hc 
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
[PROOFSTEP]
have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ Prepartition.distortion (Prepartition.compl ⊤) ≤ c
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : Prepartition.distortion (Prepartition.compl ⊤) ≤ c
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
[PROOFSTEP]
simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
⊢ NeBot (toFilterDistortion l I (Box.distortion I))
[PROOFSTEP]
simpa using (l.toFilterDistortioniUnion_neBot' I ⊤).mono inf_le_left
