awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
refine :
  ∀ (hD : l.bDistortion = true),
    ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
refine₁ refine₂ :
  ∀ (hD : l.bDistortion = true) (π₁ : Prepartition I) (hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion)
    (hc : π₁.distortion ≤ c),
    ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
refine₃ :
  ∀ (hD : l.bDistortion = true) (π₁ : Prepartition I) (hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion)
    (hc : π₁.distortion ≤ c),
    let π₂ := π.filter fun (J : Box ι) ↦ ¬p J;
    ∀ (this : Disjoint π₁.iUnion π₂.iUnion),
      ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
refine_1 :
  ∀ (hD : l.bDistortion = true) (π₁ : Prepartition I) (hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion)
    (hc : π₁.distortion ≤ c),
    let π₂ := π.filter fun (J : Box ι) ↦ ¬p J;
    ∀ (this : Disjoint π₁.iUnion π₂.iUnion),
      (π₁.disjUnion π₂.toPrepartition this).iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion
refine_2 refine_2₁ :
  ∀ (hD : l.bDistortion = true) (π₁ : Prepartition I) (hπ₁U : π₁.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion)
    (hc : π₁.distortion ≤ c),
    let π₂ := π.filter fun (J : Box ι) ↦ ¬p J;
    ∀ (this : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂.toPrepartition this).distortion ≤ c
⊢ l.MemBaseSet I c r (π.filter p)

Tactic:
classical
  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 => ?_⟩
  rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
  set π₂ := π.filter fun J => ¬p J
  have : Disjoint π₁.iUnion π₂.iUnion := by
    simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
  refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
  · suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
    have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
    ext x
    fconstructor
    · rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
      exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
    · rintro ⟨hxI, hxp⟩
      by_cases hxπ : x ∈ π.iUnion
      exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]
  · have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
    simpa [hc]

Premises used: BoxIntegral.TaggedPrepartition.iUnion, BoxIntegral.TaggedPrepartition.filter, Or.inl, Not, Or.inr
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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:
⟨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 => ?_⟩

Premises used: Iff.mpr, BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, BoxIntegral.IntegrationParams.MemBaseSet.mk, BoxIntegral.IntegrationParams.MemBaseSet.isHenstock, BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged, BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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
refine_1 : ∀ (hD : l.bDistortion = true), (π.biUnionTagged πi).distortion ≤ c
refine_2 :
  ∀ (hD : l.bDistortion = true),
    ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion ∧ π'.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 => ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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
refine_1 : ∀ b ∈ π.boxes, (πi b).distortion ≤ c
⊢ (π.biUnionTagged πi).distortion ≤ c

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

Premises used: BoxIntegral.Prepartition.distortion_biUnionTagged, Finset.sup_le_iff
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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:
fun J hJ => (h J hJ).3 hD

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.distortion_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.distortion_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c

Tactic:
⟨_, ?_, hc hD⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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
refine_2 : π.compl.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion
⊢ ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c

Tactic:
refine ⟨_, ?_, hc hD⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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
refine_2 :
  (↑I : Set (ι → ℝ)) \ (π.biUnion fun (J : Box ι) ↦ (πi J).toPrepartition).iUnion =
    (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion
⊢ π.compl.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion

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

Premises used: BoxIntegral.Prepartition.iUnion_compl, BoxIntegral.Prepartition.iUnion_biUnion_partition
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : 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 : Set (ι → ℝ)) \ (π.biUnion fun (J : Box ι) ↦ (πi J).toPrepartition).iUnion =
    (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion

Tactic:
rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
l₁ l₂ : IntegrationParams
ι : Type u_2
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
h : l₁ ≤ l₂
hr : l₂.RCond r
⊢ l₁.RCond r

Tactic:
fun hR => hr (le_iff_imp.1 h.1 hR)

Premises used: Bool.le_iff_imp, BoxIntegral.IntegrationParams.RCond, And.left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
l : IntegrationParams
ι : Type u_2
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
h₁ : l.RCond r₁
h₂ : l.RCond r₂
⊢ RCond.{u_2} (ι := ι) l fun (x : ι → ℝ) ↦ Min.min (r₁ x) (r₂ x)

Tactic:
fun hR x => congr_arg₂ min (h₁ hR x) (h₂ hR x)

Premises used: BoxIntegral.IntegrationParams.RCond, Min.min, congr_arg₂
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
c₁ c₂ : ℝ≥0
l₁ l₂ : IntegrationParams
I : Box ι
h : l₁ ≤ l₂
hc : c₁ ≤ c₂
⊢ l₁.toFilterDistortion I c₁ ≤ l₂.toFilterDistortion I c₂

Tactic:
iInf_mono fun _ =>
    iInf_mono' fun hr =>
      ⟨hr.mono h, principal_mono.2 fun _ => MemBaseSet.mono I h hc fun _ _ => le_rfl⟩

Premises used: Iff.mpr, le_rfl, Filter.principal_mono, Set.Mem, iInf_mono, BoxIntegral.IntegrationParams.RCond.mono, Exists.intro, BoxIntegral.IntegrationParams.MemBaseSet.mono, iInf_mono'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
l₁ l₂ : IntegrationParams
h : l₁ ≤ l₂
⊢ l₁.toFilter I ≤ l₂.toFilter I

Tactic:
iSup_mono fun _ => toFilterDistortion_mono I h le_rfl

Premises used: le_rfl, Set.Mem, BoxIntegral.IntegrationParams.toFilterDistortion_mono, iSup_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
l₁ l₂ : IntegrationParams
h : l₁ ≤ l₂
π₀ : Prepartition I
⊢ toFilteriUnion (l := l₁) I π₀ ≤ toFilteriUnion (l := l₂) I π₀

Tactic:
iSup_mono fun _ => inf_le_inf_right _ <| toFilterDistortion_mono _ h le_rfl

Premises used: le_rfl, Set.Mem, setOf, BoxIntegral.TaggedPrepartition.iUnion, inf_le_inf_right, BoxIntegral.IntegrationParams.toFilterDistortion_mono, Filter.principal, Eq, iSup_mono, BoxIntegral.Prepartition.iUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
l : IntegrationParams
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ toFilteriUnion (l := l) I π₁ = toFilteriUnion (l := l) I π₂

Tactic:
simp only [toFilteriUnion, toFilterDistortioniUnion, h]

Premises used: BoxIntegral.IntegrationParams.toFilterDistortioniUnion, BoxIntegral.IntegrationParams.toFilteriUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
c : ℝ≥0
⊢ (l.toFilterDistortion I c).HasBasis l.RCond fun (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦
    {π : TaggedPrepartition I | l.MemBaseSet I c r π}

Tactic:
hasBasis_biInf_principal'
    (fun _ hr₁ _ hr₂ =>
      ⟨_, hr₁.min hr₂, fun _ => MemBaseSet.mono _ le_rfl le_rfl fun _ _ => min_le_left _ _,
        fun _ => MemBaseSet.mono _ le_rfl le_rfl fun _ _ => min_le_right _ _⟩)
    ⟨fun _ => ⟨1, Set.mem_Ioi.2 zero_lt_one⟩, fun _ _ => rfl⟩

Premises used: Iff.mpr, le_rfl, Set.mem_Ioi, BoxIntegral.IntegrationParams.toFilterDistortion, Subtype.mk, min_le_left, zero_lt_one, BoxIntegral.IntegrationParams.RCond.min, Filter.hasBasis_biInf_principal', And.intro, min_le_right, Exists.intro, OfNat.ofNat, BoxIntegral.IntegrationParams.MemBaseSet.mono, Min.min, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
c : ℝ≥0
π₀ : Prepartition I
⊢ (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦
    {π : TaggedPrepartition I | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}

Tactic:
(l.hasBasis_toFilterDistortion I c).inf_principal _

Premises used: BoxIntegral.IntegrationParams.toFilterDistortioniUnion, Set.Mem, setOf, Set.inter, BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion, Filter.HasBasis.inf_principal
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ ∀ (c : ℝ≥0),
    (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦
      {π : TaggedPrepartition I | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}

Tactic:
have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
this :
  ∀ (c : ℝ≥0),
    (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦
      {π : TaggedPrepartition I | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}
⊢ (toFilteriUnion (l := l) I π₀).HasBasis (fun (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦ ∀ (c : ℝ≥0), l.RCond (r c))
    fun (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}

Tactic:
simpa only [setOf_and, setOf_exists] using hasBasis_iSup this

Premises used: Set.setOf_and, Set.setOf_exists, Filter.hasBasis_iSup
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (toFilteriUnion (l := l) I ⊤).HasBasis (fun (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦ ∀ (c : ℝ≥0), l.RCond (r c))
    fun (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦
    {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π ∧ π.IsPartition}

Tactic:
simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using
    l.hasBasis_toFilteriUnion I ⊤

Premises used: BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion, BoxIntegral.Prepartition.iUnion_top, BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq, Top.top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (l.toFilter I).HasBasis (fun (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦ ∀ (c : ℝ≥0), l.RCond (r c))
    fun (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) ↦ {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π}

Tactic:
simpa only [setOf_exists] using hasBasis_iSup (l.hasBasis_toFilterDistortion I)

Premises used: Set.setOf_exists, BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion, Filter.hasBasis_iSup
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
simp :
  ∀ (i : ℝ≥0),
    Tendsto (β := TaggedPrepartition J) (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
      (l.toFilterDistortioniUnion I i ⊤) (⨆ (c : ℝ≥0), l.toFilterDistortioniUnion J c (Prepartition.single J I h))
⊢ Tendsto (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J) (toFilteriUnion (l := l) I ⊤)
    (toFilteriUnion (l := l) J (Prepartition.single J I h))

Tactic:
simp only [toFilteriUnion, tendsto_iSup]

Premises used: BoxIntegral.IntegrationParams.toFilteriUnion, Filter.tendsto_iSup
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
set :
  let π₀ := Prepartition.single J I h;
  Tendsto (β := TaggedPrepartition J) (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
    (l.toFilterDistortioniUnion I c ⊤) (⨆ (c : ℝ≥0), l.toFilterDistortioniUnion J c π₀)
⊢ Tendsto (β := TaggedPrepartition J) (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
    (l.toFilterDistortioniUnion I c ⊤) (⨆ (c : ℝ≥0), l.toFilterDistortioniUnion J c (Prepartition.single J I h))

Tactic:
set π₀ := Prepartition.single J I h

Premises used: BoxIntegral.Prepartition.single
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Tendsto (β := TaggedPrepartition J) (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
    (l.toFilterDistortioniUnion I c ⊤) (⨆ (c : ℝ≥0), l.toFilterDistortioniUnion J c π₀)

Tactic:
le_iSup_of_le (max c π₀.compl.distortion) ?_

Premises used: Set.Mem, BoxIntegral.Prepartition.compl, BoxIntegral.Prepartition.distortion, Filter.Tendsto, Max.max, le_iSup_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
refine :
  Filter.map (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
      (l.toFilterDistortioniUnion I c ⊤) ≤
    l.toFilterDistortioniUnion J (max c π₀.compl.distortion) π₀
⊢ Tendsto (β := TaggedPrepartition J) (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
    (l.toFilterDistortioniUnion I c ⊤) (⨆ (c : ℝ≥0), l.toFilterDistortioniUnion J c π₀)

Tactic:
refine le_iSup_of_le (max c π₀.compl.distortion) ?_

Premises used: BoxIntegral.Prepartition.compl, BoxIntegral.Prepartition.distortion, Max.max, le_iSup_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Filter.map (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
      (l.toFilterDistortioniUnion I c ⊤) ≤
    l.toFilterDistortioniUnion J (max c π₀.compl.distortion) π₀

Tactic:
((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff
    (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.Tendsto, BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion, Top.top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
refine :
  ∀ (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)) (hr : l.RCond r),
    ∃ (ia : (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      l.RCond ia ∧
        ∀ (x : TaggedPrepartition I),
          Membership.mem (γ := Set (TaggedPrepartition I))
              {π : TaggedPrepartition I | l.MemBaseSet I c ia π ∧ π.iUnion = Prepartition.iUnion (I := I) ⊤} x →
            Membership.mem (α := TaggedPrepartition J) (γ := Set (TaggedPrepartition J))
              {π : TaggedPrepartition J | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
              ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) x : TaggedPrepartition J)
⊢ Filter.map (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J)
      (l.toFilterDistortioniUnion I c ⊤) ≤
    l.toFilterDistortioniUnion J (max c π₀.compl.distortion) π₀

Tactic:
refine ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff
    (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion, Top.top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : l.RCond r
⊢ ∃ (ia : (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    l.RCond ia ∧
      ∀ (x : TaggedPrepartition I),
        Membership.mem (γ := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | l.MemBaseSet I c ia π ∧ π.iUnion = Prepartition.iUnion (I := I) ⊤} x →
          Membership.mem (α := TaggedPrepartition J) (γ := Set (TaggedPrepartition J))
            {π : TaggedPrepartition J | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
            ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) x : TaggedPrepartition J)

Tactic:
⟨r, hr, fun π hπ => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : l.RCond r
refine :
  ∀ (π : TaggedPrepartition I)
    (hπ :
      Membership.mem (γ := Set (TaggedPrepartition I))
        {π : TaggedPrepartition I | l.MemBaseSet I c r π ∧ π.iUnion = Prepartition.iUnion (I := I) ⊤} π),
    Membership.mem (α := TaggedPrepartition J) (γ := Set (TaggedPrepartition J))
      {π : TaggedPrepartition J | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
      ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π : TaggedPrepartition J)
⊢ ∃ (ia : (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    l.RCond ia ∧
      ∀ (x : TaggedPrepartition I),
        Membership.mem (γ := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | l.MemBaseSet I c ia π ∧ π.iUnion = Prepartition.iUnion (I := I) ⊤} x →
          Membership.mem (α := TaggedPrepartition J) (γ := Set (TaggedPrepartition J))
            {π : TaggedPrepartition J | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
            ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) x : TaggedPrepartition J)

Tactic:
refine ⟨r, hr, fun π hπ => ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : l.RCond r
π : TaggedPrepartition I
hπ :
  Membership.mem (γ := Set (TaggedPrepartition I))
    {π : TaggedPrepartition I | l.MemBaseSet I c r π ∧ π.iUnion = Prepartition.iUnion (I := I) ⊤} π
⊢ l.MemBaseSet I c r π ∧ π.iUnion = (↑I : Set (ι → ℝ))

Tactic:
rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ

Premises used: Set.mem_setOf_eq, BoxIntegral.Prepartition.iUnion_top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = (↑I : Set (ι → ℝ))
⊢ Membership.mem (α := TaggedPrepartition J) (γ := Set (TaggedPrepartition J))
    {π : TaggedPrepartition J | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
    ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π : TaggedPrepartition J)

Tactic:
⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate, BoxIntegral.IntegrationParams.MemBaseSet.mk, Set.Mem, BoxIntegral.IntegrationParams.MemBaseSet.distortion_le, setOf, BoxIntegral.Prepartition.compl, BoxIntegral.IntegrationParams.MemBaseSet.isHenstock, BoxIntegral.Prepartition.distortion, And.left, And.intro, le_max_left, le_trans