awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞)
    ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ v) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞)
    ((μ.restrict v : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [μ.restrict_apply hs]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞)
    ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ v) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.restrict v : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
repeat rw [μ.restrict_apply hs]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h : μ.measureOf s = (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ v)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞)
    ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ v) : ℝ≥0∞)

Tactic:
apply le_of_le_of_eq <| μ.mono s.inter_subset_left

Premises used: le_of_le_of_eq, MeasureTheory.OuterMeasure.mono, Set.inter_subset_left, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ.measureOf s = (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ v)

Tactic:
measure_eq_measure_of_null_diff s.inter_subset_left ?_ |>.symm

Premises used: Set.inter_subset_left, MeasureTheory.measure_eq_measure_of_null_diff, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s \ (s ∩ v)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.measureOf s = (μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ v)

Tactic:
refine measure_eq_measure_of_null_diff s.inter_subset_left ?_ |>.symm

Premises used: Set.inter_subset_left, MeasureTheory.measure_eq_measure_of_null_diff, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h : LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ vᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s \ (s ∩ v)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [diff_self_inter, Set.diff_eq, ← nonpos_iff_eq_zero]

Premises used: Set.diff_self_inter, Set.diff_eq, nonpos_iff_eq_zero
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h : LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) vᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ vᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
grw [s.inter_subset_right]

Premises used: Set.inter_subset_right
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) vᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hc.le

Premises used: Set.Mem, setOf, Eq.le
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) vᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hc.le

Premises used: Eq.le
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) : (a : Set (ι → ℝ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
simp [I.isCompact_Icc.measure_lt_top (μ := μ)]

Premises used: BoxIntegral.Box.isCompact_Icc, IsCompact.measure_lt_top
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ IsFiniteMeasure (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I))

Tactic:
have : IsFiniteMeasure (μ.restrict (Box.Icc I)) :=
      { measure_univ_lt_top := by simp [I.isCompact_Icc.measure_lt_top (μ := μ)] }
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IsFiniteMeasure (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I))
⊢ IsFiniteMeasure (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
have : IsFiniteMeasure (μ.restrict I) :=
      isFiniteMeasure_of_le _ (μ.restrict_mono Box.coe_subset_Icc le_rfl)
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this_1 : IsFiniteMeasure (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I))
this : IsFiniteMeasure (μ.restrict (↑I : Set (ι → ℝ)))
h :
  ∀ (C : ℝ)
    (hC :
      ∀ (x : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C),
    HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))
⊢ HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
obtain ⟨C, hC⟩ := hb
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this_1 : IsFiniteMeasure (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I))
this : IsFiniteMeasure (μ.restrict (↑I : Set (ι → ℝ)))
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
⊢ HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
.of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)

Premises used: Iff.mpr, MeasureTheory.HasFiniteIntegral.of_bounded, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this_1 : IsFiniteMeasure (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I))
this : IsFiniteMeasure (μ.restrict (↑I : Set (ι → ℝ)))
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
h : ∃ v ∈ ae (μ.restrict (↑I : Set (ι → ℝ))), ∀ y ∈ v, ‖f y‖ ≤ C
⊢ HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
refine .of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this_1 : IsFiniteMeasure (μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I))
this : IsFiniteMeasure (μ.restrict (↑I : Set (ι → ℝ)))
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
w : Set (ι → ℝ)
left : (↑I : Set (ι → ℝ)) ∈ ae (μ.restrict (↑I : Set (ι → ℝ)))
right : ∀ y ∈ (↑I : Set (ι → ℝ)), ‖f y‖ ≤ C
⊢ ∃ v ∈ ae (μ.restrict (↑I : Set (ι → ℝ))), ∀ y ∈ v, ‖f y‖ ≤ C

Tactic:
use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)

Premises used: BoxIntegral.Box.measurableSet_coe, BoxIntegral.Box.coe_subset_Icc, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
f g : ι →ᵇᵃ[I₀] M
h : f.toFun = g.toFun
mk :
  ∀ (toFun : Box ι → M)
    (sum_partition_boxes' :
      ∀ (J : Box ι),
        (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J)
    (h : { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M }.toFun = g.toFun),
    { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
g : ι →ᵇᵃ[I₀] M
toFun : Box ι → M
sum_partition_boxes' :
  ∀ (J : Box ι),
    (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J
h : { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M }.toFun = g.toFun
mk :
  ∀ (toFun_1 : Box ι → M)
    (sum_partition_boxes'_1 :
      ∀ (J : Box ι),
        (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun_1 Ji = toFun_1 J)
    (h :
      { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M }.toFun =
        { toFun := toFun_1, sum_partition_boxes' := sum_partition_boxes'_1 : ι →ᵇᵃ[I₀] M }.toFun),
    { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M } =
      { toFun := toFun_1, sum_partition_boxes' := sum_partition_boxes'_1 }
⊢ { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
toFun : Box ι → M
sum_partition_boxes' :
  ∀ (J : Box ι),
    (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J
toFun_1 : Box ι → M
sum_partition_boxes'_1 :
  ∀ (J : Box ι),
    (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun_1 Ji = toFun_1 J
h :
  { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M }.toFun =
    { toFun := toFun_1, sum_partition_boxes' := sum_partition_boxes'_1 : ι →ᵇᵃ[I₀] M }.toFun
⊢ { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M } =
    { toFun := toFun_1, sum_partition_boxes' := sum_partition_boxes'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
f : Box ι → M
h : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
⊢ (⇑{ toFun := f, sum_partition_boxes' := h : ι →ᵇᵃ[I₀] M } : (a : Box ι) → M) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
⊢ Injective (β := (x : Box ι) → M) fun (f : ι →ᵇᵃ[I₀] M) (x : Box ι) ↦ (f : (a : Box ι) → M) x

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
f g : ι →ᵇᵃ[I₀] M
⊢ Eq (α := (a : Box ι) → M) (⇑f : (a : Box ι) → M) (⇑g : (a : Box ι) → M) ↔ f = g

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
h : π.IsPartition
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π.boxes, (f : (a : Box ι) → M) J : M) ((f : (a : Box ι) → M) I : M)

Tactic:
f.sum_partition_boxes' I hI π h

Premises used: BoxIntegral.BoxAdditiveMap.sum_partition_boxes'
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀ : WithTop (Box ι)
I_1 : Box ι
i : ι
f g : ι →ᵇᵃ[I₀] M
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes,
      HAdd.hAdd (α := (a : Box ι) → M) (β := (a : Box ι) → M) (⇑f : (a : Box ι) → M) (⇑g : (a : Box ι) → M) Ji =
    HAdd.hAdd (α := (a : Box ι) → M) (β := (a : Box ι) → M) (⇑f : (a : Box ι) → M) (⇑g : (a : Box ι) → M) I

Tactic:
simp only [Pi.add_apply, sum_add_distrib, sum_partition_boxes _ hI hπ]

Premises used: Finset.sum_add_distrib, Pi.add_apply, BoxIntegral.BoxAdditiveMap.sum_partition_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀ : WithTop (Box ι)
I_1 : Box ι
i : ι
R : Type u_4
inst_2 : Monoid R
inst_3 : DistribMulAction R M
r : R
f : ι →ᵇᵃ[I₀] M
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, HSMul.hSMul (β := (a : Box ι) → M) r (⇑f : (a : Box ι) → M) Ji =
    HSMul.hSMul (β := (a : Box ι) → M) r (⇑f : (a : Box ι) → M) I

Tactic:
simp only [Pi.smul_apply, ← smul_sum, sum_partition_boxes _ hI hπ]

Premises used: BoxIntegral.BoxAdditiveMap.sum_partition_boxes, Finset.smul_sum, Pi.smul_apply
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
i : ι
x : ℝ
rw :
  HAdd.hAdd (α := M) (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitLower i x))
      (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitUpper i x)) =
    ∑ J ∈ (split I i x).boxes, (f : (a : Box ι) → M) J
rw₁ rw₂ :
  HAdd.hAdd (α := M) (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitLower i x))
      (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitUpper i x)) =
    HAdd.hAdd (α := M) (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitLower i x))
      (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitUpper i x))
⊢ HAdd.hAdd (α := M) (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitLower i x))
      (Option.elim' 0 (⇑f : (a : Box ι) → M) (I.splitUpper i x)) =
    (f : (a : Box ι) → M) I

Tactic:
rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]

Premises used: BoxIntegral.BoxAdditiveMap.sum_partition_boxes, BoxIntegral.Prepartition.sum_split_boxes, BoxIntegral.Prepartition.isPartitionSplit
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀_1 : WithTop (Box ι)
I : Box ι
i : ι
inst_2 : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    (↑I : WithTop (Box ι)) ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
⊢ ι →ᵇᵃ[I₀] M

Tactic:
refine ⟨f, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀_1 : WithTop (Box ι)
I_1 : Box ι
i : ι
inst_2 : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    (↑I : WithTop (Box ι)) ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
⊢ ∑ J ∈ (splitMany I ∅).boxes, f J = f I

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀_1 : WithTop (Box ι)
I_1 : Box ι
i : ι
inst_2 : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    (↑I : WithTop (Box ι)) ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
h : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
insert :
  Eq.{u_2 + 1} (α := M) (∑ J ∈ (splitMany I s).boxes, ∑ J' ∈ (split J a.1 a.2).boxes, f J')
    (∑ J ∈ (splitMany I s).boxes, f J)
⊢ ∑ J ∈ (splitMany I (Insert.insert a s)).boxes, f J = f I

Tactic:
rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]

Premises used: BoxIntegral.Prepartition.sum_biUnion_boxes, BoxIntegral.Prepartition.inf_split, BoxIntegral.Prepartition.biUnion_boxes, BoxIntegral.Prepartition.splitMany_insert
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
I₀_1 : WithTop (Box ι)
I_1 : Box ι
i : ι
inst_2 : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    (↑I : WithTop (Box ι)) ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
h : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ (splitMany I s).boxes, ∑ J' ∈ (split J a.1 a.2).boxes, f J')
    (∑ J ∈ (splitMany I s).boxes, f J)

Tactic:
Finset.sum_congr rfl fun J' hJ' => ?_

Premises used: Finset.sum_congr, rfl