-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem biUnionTagged_memBaseSet {π : Prepartition I} {πi : ∀ J, TaggedPrepartition J}
    (h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)) (hp : ∀ J ∈ π, (πi J).IsPartition)
    (hc : l.bDistortion → π.compl.distortion ≤ c) : l.MemBaseSet I c r (π.biUnionTagged πi)

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ∃ π', π'.iUnion = ↑I \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c

Tactic:
refine ⟨_, ?_, hc hD⟩

Result:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ π.compl.iUnion = ↑I \ (π.biUnionTagged πi).iUnion

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ↑I \ (π.biUnion fun J => (πi J).toPrepartition).iUnion = ↑I \ (π.biUnionTagged πi).iUnion

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
⊢ l.MemBaseSet I c r (π.biUnionTagged πi)

Tactic:
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 => ?_⟩

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ (π.biUnionTagged πi).distortion ≤ c

case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ∃ π', π'.iUnion = ↑I \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ π.compl.iUnion = ↑I \ (π.biUnionTagged πi).iUnion

Tactic:
rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]

Result:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ↑I \ (π.biUnion fun J => (πi J).toPrepartition).iUnion = ↑I \ (π.biUnionTagged πi).iUnion

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ (π.biUnionTagged πi).distortion ≤ c

Tactic:
rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ∀ b ∈ π.boxes, (πi b).distortion ≤ c

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ∀ b ∈ π.boxes, (πi b).distortion ≤ c

Tactic:
exact fun J hJ => (h J hJ).3 hD

Result:
no goals