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 π₀
ι : 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 π₀
rcases π₀.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r with ⟨π, hle, hH, hr, hd, hU⟩
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 π
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 π₀
refine' ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, _, hc₂⟩⟩, ⟨hle, hU⟩⟩
no goals
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 π
exact Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl