awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (ι → ℝ))
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
refine_2 :
  TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) =
    π₀.iUnion
⊢ 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 ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩
-- 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 (ι → ℝ))
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

Tactic:
⟨_, π₀.iUnion_compl.trans ?_, le_max_right _ _⟩

Premises used: le_max_right, BoxIntegral.Prepartition.iUnion_compl, And.intro, Exists.intro, Eq.trans
-- 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 (ι → ℝ))
h_1 : l.bDistortion = true
refine_1 :
  (↑J : Set (ι → ℝ)) \ π₀.iUnion =
    (↑J : Set (ι → ℝ)) \
      TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)
⊢ ∃ (π' : 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 ⟨_, π₀.iUnion_compl.trans ?_, le_max_right _ _⟩
-- 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 (ι → ℝ))
h_1 : l.bDistortion = true
refine_1 :
  π₀.iUnion =
    TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)
⊢ (↑J : Set (ι → ℝ)) \ π₀.iUnion =
    (↑J : Set (ι → ℝ)) \
      TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)

Tactic:
congr 1
-- 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 (ι → ℝ))
h_1 : l.bDistortion = true
⊢ π₀.iUnion =
    TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)

Tactic:
(Prepartition.iUnion_single h).trans hπ.2.symm

Premises used: And.right, Eq.symm, Eq.trans, BoxIntegral.Prepartition.iUnion_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
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
⊢ π₀.iUnion =
    TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π)

Tactic:
exact (Prepartition.iUnion_single h).trans hπ.2.symm

Premises used: And.right, Eq.symm, Eq.trans, BoxIntegral.Prepartition.iUnion_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
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = (↑I : Set (ι → ℝ))
⊢ TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) =
    π₀.iUnion

Tactic:
hπ.2.trans (Prepartition.iUnion_single _).symm

Premises used: Set.Mem, setOf, BoxIntegral.TaggedPrepartition.iUnion, And.right, Eq.symm, Eq.trans, BoxIntegral.Prepartition.iUnion_single, BoxIntegral.Prepartition.iUnion
-- 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 (ι → ℝ))
⊢ TaggedPrepartition.iUnion (I := J) ((embedBox I J h : (a : TaggedPrepartition I) → TaggedPrepartition J) π) =
    π₀.iUnion

Tactic:
exact hπ.2.trans (Prepartition.iUnion_single _).symm

Premises used: And.right, Eq.symm, Eq.trans, BoxIntegral.Prepartition.iUnion_single
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
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)
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
⊢ ∃ (π : 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⟩

Premises used: BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
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

Tactic:
⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, ?_, hc₂⟩⟩, ⟨hle, hU⟩⟩

Premises used: BoxIntegral.IntegrationParams.MemBaseSet.mk, BoxIntegral.Prepartition.compl, Eq.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
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
refine : l.bDistortion = true → π₀.compl.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion

Tactic:
refine ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, ?_, hc₂⟩⟩, ⟨hle, hU⟩⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
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
h : l.bDistortion = true
⊢ π₀.compl.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion

Tactic:
Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl

Premises used: BoxIntegral.Prepartition.compl_congr, Eq.rec, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.Prepartition.iUnion_compl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
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
h : l.bDistortion = true
⊢ π₀.compl.iUnion = (↑I : Set (ι → ℝ)) \ π.iUnion

Tactic:
exact Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : I.distortion ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
rw :
  ∀ (hc : Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊤ ≤ c) (r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.IsPartition
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
rw [← Prepartition.distortion_top] at hc

Premises used: BoxIntegral.Prepartition.distortion_top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊤ ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ Prepartition.distortion.{u_1} (ι := ι) (I := I) (Prepartition.compl ⊤) ≤ c

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊤ ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ Prepartition.distortion.{u_1} (ι := ι) (I := I) (Prepartition.compl ⊤) ≤ c

Tactic:
have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : Prepartition.distortion.{u_1} (ι := ι) (I := I) ⊤ ≤ c
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hc' : Prepartition.distortion.{u_1} (ι := ι) (I := I) (Prepartition.compl ⊤) ≤ c
⊢ ∃ (π : TaggedPrepartition I), l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r

Premises used: BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq, Top.top, BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
⊢ (l.toFilterDistortioniUnion I c π₀).NeBot

Tactic:
((l.hasBasis_toFilterDistortion I _).inf_principal _).neBot_iff.2
    fun {r} _ => (l.exists_memBaseSet_le_iUnion_eq π₀ hc₁ hc₂ r).imp fun _ hπ => ⟨hπ.1, hπ.2.2⟩

Premises used: Iff.mpr, BoxIntegral.IntegrationParams.toFilterDistortioniUnion, Filter.HasBasis.neBot_iff, Exists.imp, BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion, And.intro, Filter.HasBasis.inf_principal, BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J : Box ι
c c₁ c₂ : ℝ≥0
l_1 l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π π₁ π₂ : TaggedPrepartition I_1
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ (l.toFilterDistortioniUnion I (max π₀.distortion π₀.compl.distortion) π₀).NeBot

Tactic:
l.toFilterDistortioniUnion_neBot I π₀ (le_max_left _ _) (le_max_right _ _)

Premises used: le_max_right, BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot, le_max_left
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J : Box ι
c c₁ c₂ : ℝ≥0
l_1 l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π π₁ π₂ : TaggedPrepartition I_1
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
l : IntegrationParams
I : Box ι
⊢ (l.toFilterDistortion I I.distortion).NeBot

Tactic:
simpa using (l.toFilterDistortioniUnion_neBot' I ⊤).mono inf_le_left

Premises used: BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot', Filter.NeBot.mono, inf_le_left, Top.top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J : Box ι
c c₁ c₂ : ℝ≥0
l_1 l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π π₁ π₂ : TaggedPrepartition I_1
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
l : IntegrationParams
I : Box ι
⊢ (l.toFilter I).NeBot

Tactic:
(l.toFilterDistortion_neBot I).mono <| le_iSup _ _

Premises used: Filter.NeBot.mono, le_iSup, BoxIntegral.IntegrationParams.toFilterDistortion_neBot
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
I_1 J : Box ι
c c₁ c₂ : ℝ≥0
l_1 l₁ l₂ : IntegrationParams
r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π π₁ π₂ : TaggedPrepartition I_1
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ (toFilteriUnion (l := l) I π₀).NeBot

Tactic:
(l.toFilterDistortioniUnion_neBot' I π₀).mono <|
    le_iSup (fun c => l.toFilterDistortioniUnion I c π₀) _

Premises used: BoxIntegral.IntegrationParams.toFilterDistortioniUnion, BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot', Filter.NeBot.mono, le_iSup
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Filter
Goal:
ι : Type u_1
inst : Fintype ι
l : IntegrationParams
I : Box ι
⊢ ∀ᶠ (π : TaggedPrepartition I) in toFilteriUnion (l := l) I ⊤, π.IsPartition

Tactic:
eventually_iSup.2 fun _ =>
    eventually_inf_principal.2 <|
      Eventually.of_forall fun π h =>
        π.isPartition_iff_iUnion_eq.2 (h.trans Prepartition.iUnion_top)

Premises used: Filter.eventually_inf_principal, Iff.mpr, BoxIntegral.IntegrationParams.toFilteriUnion, Filter.Eventually.of_forall, Filter.eventually_iSup, BoxIntegral.Prepartition.iUnion_top, BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
μ : Measure (ι → ℝ)
inst : IsLocallyFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
show μ (Icc I.lower I.upper) < ∞ from I.isCompact_Icc.measure_lt_top

Premises used: BoxIntegral.Box.isCompact_Icc, setOf, Set.Icc, IsCompact.measure_lt_top
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
μ : Measure (ι → ℝ)
inst : IsLocallyFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono <| coe_subset_Icc).trans_lt (I.measure_Icc_lt_top μ)

Premises used: BoxIntegral.Box.measure_Icc_lt_top, MeasureTheory.measure_mono, BoxIntegral.Box.coe_subset_Icc, LE.le.trans_lt
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Countable ι
rw : MeasurableSet.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))
⊢ MeasurableSet (↑I : Set (ι → ℝ))

Tactic:
rw [coe_eq_pi]

Premises used: BoxIntegral.Box.coe_eq_pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Countable ι
⊢ MeasurableSet.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))

Tactic:
MeasurableSet.univ_pi fun i => measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasurableSet.univ_pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Countable ι
⊢ MeasurableSet.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))

Tactic:
exact MeasurableSet.univ_pi fun i => measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasurableSet.univ_pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Countable ι
⊢ MeasurableSet.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
_root_.measurableSet_Icc

Premises used: setOf, Set.Icc, measurableSet_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Countable ι
⊢ MeasurableSet.{u_1} (α := ι → ℝ) ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
MeasurableSet.univ_pi fun _ => _root_.measurableSet_Ioo

Premises used: setOf, measurableSet_Ioo, Set.pi, MeasurableSet.univ_pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
rw :
  (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =ᶠ[ae (F := Measure (ι → ℝ)) volume]
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I
⊢ (↑I : Set (ι → ℝ)) =ᶠ[ae (F := Measure (ι → ℝ)) volume] (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I

Tactic:
rw [coe_eq_pi]

Premises used: BoxIntegral.Box.coe_eq_pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
⊢ (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =ᶠ[ae (F := Measure (ι → ℝ)) volume]
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I

Tactic:
Measure.univ_pi_Ioc_ae_eq_Icc

Premises used: MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc, setOf, Set.Icc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
⊢ (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =ᶠ[ae (F := Measure (ι → ℝ)) volume]
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I

Tactic:
exact Measure.univ_pi_Ioc_ae_eq_Icc

Premises used: MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
I : Box ι
inst : Fintype ι
⊢ (ae (F := Measure (ι → ℝ)) volume).EventuallyEq (β := Prop) ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I)
    ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)

Tactic:
Measure.univ_pi_Ioo_ae_eq_Icc

Premises used: MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc, Set.Mem, setOf, Set.Icc, Set.pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
rw :
  ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π, (↑J : Set (ι → ℝ)))) =
    ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))
⊢ ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) π.iUnion) =
    ∑ x ∈ π.boxes, ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑x : Set (ι → ℝ)))

Tactic:
rw [← ENNReal.toReal_sum (fun J _ => (J.measure_coe_lt_top μ).ne), π.iUnion_def]

Premises used: BoxIntegral.Prepartition.iUnion_def, ENNReal.toReal_sum
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
simp :
  ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π.boxes, (↑J : Set (ι → ℝ)))) =
    ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))
⊢ ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π, (↑J : Set (ι → ℝ)))) =
    ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))

Tactic:
simp only [← mem_boxes]

Premises used: BoxIntegral.Prepartition.mem_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
rw : ∀ b ∈ π.boxes, MeasurableSet (↑b : Set (ι → ℝ))
⊢ ENNReal.toReal ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (⋃ J ∈ π.boxes, (↑J : Set (ι → ℝ)))) =
    ENNReal.toReal (∑ a ∈ π.boxes, (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑a : Set (ι → ℝ)))

Tactic:
rw [measure_biUnion_finset π.pairwiseDisjoint]

Premises used: BoxIntegral.Prepartition.pairwiseDisjoint, MeasureTheory.measure_biUnion_finset
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
⊢ ∀ b ∈ π.boxes, MeasurableSet (↑b : Set (ι → ℝ))

Tactic:
fun J _ => J.measurableSet_coe

Premises used: BoxIntegral.Box.measurableSet_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
⊢ ∀ b ∈ π.boxes, MeasurableSet (↑b : Set (ι → ℝ))

Tactic:
exact fun J _ => J.measurableSet_coe
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Finite ι
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
J : Box ι
h : (↑J : WithTop (Box ι)) ≤ ⊤
π : Prepartition J
hπ : π.IsPartition
rw : μ.real π.iUnion = μ.real (↑J : Set (ι → ℝ))
rw₁ rw₂ : μ.real (↑J : Set (ι → ℝ)) = μ.real (↑J : Set (ι → ℝ))
⊢ ∑ Ji ∈ π.boxes, μ.real (↑Ji : Set (ι → ℝ)) = μ.real (↑J : Set (ι → ℝ))

Tactic:
rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]

Premises used: BoxIntegral.Prepartition.measure_iUnion_toReal, BoxIntegral.Prepartition.IsPartition.iUnion_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
rw :
  Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑I : Set (ι → ℝ)) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₁ :
  Measure.real.{u_1} (α := ι → ℝ) (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ))
      (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i)) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₂ :
  ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
        (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₃ rw₄ : Eq (α := ℝ) (∏ i : ι, (I.upper i - I.lower i)) (∏ i : ι, (I.upper i - I.lower i))
⊢ Eq (α := ℝ) ((Measure.toBoxAdditive volume : (a : Box ι) → ℝ) I : ℝ) (∏ i : ι, (I.upper i - I.lower i) : ℝ)

Tactic:
rw [Measure.toBoxAdditive_apply, coe_eq_pi, measureReal_def,
    Real.volume_pi_Ioc_toReal I.lower_le_upper]

Premises used: Real.volume_pi_Ioc_toReal, BoxIntegral.Box.lower_le_upper, MeasureTheory.Measure.toBoxAdditive_apply, BoxIntegral.Box.coe_eq_pi, MeasureTheory.measureReal_def
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
rw :
  ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
        (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (I.lower i) (I.upper i))) =
    ∏ i : ι, (I.upper i - I.lower i)
rw₁ rw₂ : Eq (α := ℝ) (∏ i : ι, (I.upper i - I.lower i)) (∏ i : ι, (I.upper i - I.lower i))
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ))) =
    ∏ i : ι, (I.upper i - I.lower i)

Tactic:
rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]

Premises used: Real.volume_pi_Ioc_toReal, BoxIntegral.Box.lower_le_upper, BoxIntegral.Box.coe_eq_pi
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Measure
Goal:
n : ℕ
i : Fin (n + 1)
I : Box (Fin (n + 1))
⊢ (∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i) =
    ∏ j : Fin (n + 1), (I.upper j - I.lower j)

Tactic:
simp only [face_lower, face_upper, Fin.prod_univ_succAbove _ i, mul_comm]

Premises used: BoxIntegral.Box.face_lower, Fin.prod_univ_succAbove, BoxIntegral.Box.face_upper, mul_comm