awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ l.MemBaseSet I c r (π.filter p)
have refine : ∀ (hD : l.bDistortion = true),
  ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.filter p).iUnion ∧ π'.distortion ≤ c
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ l.MemBaseSet I c r (π.filter p)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ l.MemBaseSet I c r (π.filter p)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ l.MemBaseSet I c r (π.filter p)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ l.MemBaseSet I c r (π.filter p)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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)
have refine_1 : ∀ (hD : l.bDistortion = true), (π.biUnionTagged πi).distortion ≤ c
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 => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ l.MemBaseSet I c r (π.biUnionTagged πi)
have refine_2 : ∀ (hD : l.bDistortion = true),
  ∃ (π' : Prepartition I), π'.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c
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 => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ (π.biUnionTagged πi).distortion ≤ c
have refine_1 : ∀ b ∈ π.boxes, (πi b).distortion ≤ c
Tactic: rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
have refine_2 : π.compl.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion
Tactic: refine ⟨_, ?_, hc hD⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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
⊢ π.compl.iUnion = (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion
have refine_2 : (↑I : Set (ι → ℝ)) \ (π.biUnion fun (J : Box ι) ↦ (πi J).toPrepartition).iUnion =
  (↑I : Set (ι → ℝ)) \ (π.biUnionTagged πi).iUnion
Tactic: rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ (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}
have 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}
Tactic: have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ Tendsto (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J) (toFilteriUnion (l := l) I ⊤)
    (toFilteriUnion (l := l) J (Prepartition.single J I h))
have 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))
Tactic: simp only [toFilteriUnion, tendsto_iSup]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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 π₀)
have refine : Filter.map (⇑(embedBox I J h) : (a : TaggedPrepartition I) → TaggedPrepartition J) (l.toFilterDistortioniUnion I c ⊤) ≤
  l.toFilterDistortioniUnion J (max c π₀.compl.distortion) π₀
Tactic: refine le_iSup_of_le (max c π₀.compl.distortion) ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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) π₀
have 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)
Tactic: refine ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff
    (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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)
have 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)
Tactic: refine ⟨r, hr, fun π hπ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (hypothesis)
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) ⊤} π
⊢ 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)
have hπ₁ : l.MemBaseSet I c r π ∧ π.iUnion = (↑I : Set (ι → ℝ))
Tactic: rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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)
have refine_1 : l.bDistortion = true →
  ∃ (π' : Prepartition J),
    π'.iUnion =
        (↑J : Set (ι → ℝ)) \
          TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) ∧
      π'.distortion ≤ max c π₀.compl.distortion
Tactic: refine ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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 (ι → ℝ))
refine_1 :
  l.bDistortion = true →
    ∃ (π' : Prepartition J),
      π'.iUnion =
          (↑J : Set (ι → ℝ)) \
            TaggedPrepartition.iUnion (I := J)
              ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) ∧
        π'.distortion ≤ max c π₀.compl.distortion
⊢ 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)
have refine_2 : TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) = π₀.iUnion
Tactic: refine ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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 (ι → ℝ))
h_1 : l.bDistortion = true
⊢ ∃ (π' : Prepartition J),
    π'.iUnion =
        (↑J : Set (ι → ℝ)) \
          TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) ∧
      π'.distortion ≤ max c π₀.compl.distortion
have refine_1 : (↑J : Set (ι → ℝ)) \ π₀.iUnion =
  (↑J : Set (ι → ℝ)) \
    TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)
Tactic: refine ⟨_, π₀.iUnion_compl.trans ?_, le_max_right _ _⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
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 (ι → ℝ))
h_1 : l.bDistortion = true
⊢ (↑J : Set (ι → ℝ)) \ π₀.iUnion =
    (↑J : Set (ι → ℝ)) \
      TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)
have refine_1 : π₀.iUnion = TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
have rcases : ∀ (π : TaggedPrepartition I) (hle : π.toPrepartition ≤ π₀) (hH : π.IsHenstock) (hr : π.IsSubordinate r)
  (hd : π.distortion = π₀.distortion) (hU : π.iUnion = π₀.iUnion),
  ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
Tactic: rcases π₀.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r with ⟨π, hle, hH, hr, hd, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Filter (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : π.IsHenstock
hr : π.IsSubordinate r
hd : π.distortion = π₀.distortion
hU : π.iUnion = π₀.iUnion
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
have refine : l.bDistortion = true → π₀.compl.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
Tactic: refine ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, ?_, hc₂⟩⟩, ⟨hle, hU⟩⟩