ι : 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))
ι : 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))
simp only [toFilteriUnion, tendsto_iSup]
ι : 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))
ι : 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))
intro c
ι : 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 π₀)
ι : 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))
set π₀ := Prepartition.single J I h
ι : 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 π₀))) π₀
ι : 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 π₀)
refine' le_iSup_of_le (max c π₀.compl.distortion) _
ι : 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 π₀}
ι : 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 π₀))) π₀
refine' ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff
  (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => _
ι : 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 π₀}
ι : 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 π₀}
refine' ⟨r, hr, fun π hπ => _⟩
ι : 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 π₀}
ι : 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 π₀}
rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ
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 π₀))

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 π₀
ι : 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 π₀}
refine' ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => _⟩, _⟩
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) π)
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 π₀))
refine' ⟨_, π₀.iUnion_compl.trans _, le_max_right _ _⟩
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) π)
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) π)
congr 1
no goals
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) π)
exact (Prepartition.iUnion_single h).trans hπ.2.symm
no goals
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 π₀
exact hπ.2.trans (Prepartition.iUnion_single _).symm