awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s \ (s ∩ v)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine measure_eq_measure_of_null_diff s.inter_subset_left ?_ |>.symm
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s \ (s ∩ v)) : ℝ≥0∞) (0 : ℝ≥0∞)
have h : LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ vᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [diff_self_inter, Set.diff_eq, ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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∞) (s ∩ vᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have h : LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) vᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: grw [s.inter_subset_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
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
⊢ HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))
have this : 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 (μ := μ)] }
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (hypothesis)
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))
⊢ HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))
have this₁ : IsFiniteMeasure (μ.restrict (↑I : Set (ι → ℝ)))
Tactic: have : IsFiniteMeasure (μ.restrict I) :=
      isFiniteMeasure_of_le _ (μ.restrict_mono Box.coe_subset_Icc le_rfl)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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 (ι → ℝ)))
⊢ HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))
have h : ∀ (C : ℝ)
  (hC :
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C),
  HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))
Tactic: obtain ⟨C, hC⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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 (ι → ℝ)))
have h : ∃ v ∈ ae (μ.restrict (↑I : Set (ι → ℝ))), ∀ y ∈ v, ‖f y‖ ≤ C
Tactic: refine .of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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
⊢ ∃ v ∈ ae (μ.restrict (↑I : Set (ι → ℝ))), ∀ y ∈ v, ‖f y‖ ≤ C
have w : Set (ι → ℝ)
Tactic: use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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 (ι → ℝ)
⊢ ∃ v ∈ ae (μ.restrict (↑I : Set (ι → ℝ))), ∀ y ∈ v, ‖f y‖ ≤ C
have left : (↑I : Set (ι → ℝ)) ∈ ae (μ.restrict (↑I : Set (ι → ℝ)))
Tactic: use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Integrability (goal)
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 (ι → ℝ)))
⊢ ∃ v ∈ ae (μ.restrict (↑I : Set (ι → ℝ))), ∀ y ∈ v, ‖f y‖ ≤ C
have right : ∀ y ∈ (↑I : Set (ι → ℝ)), ‖f y‖ ≤ C
Tactic: use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
⊢ { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' : ι →ᵇᵃ[I₀] M } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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 : ℝ
⊢ 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
have 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
Tactic: rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
⊢ 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
have 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))
Tactic: rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
⊢ ι →ᵇᵃ[I₀] M
have refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
Tactic: refine ⟨f, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
⊢ ∑ J ∈ (splitMany I (insert a s)).boxes, f J = f I
have 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)
Tactic: rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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)
have insert : ∀ (J' : Box ι) (hJ' : J' ∈ (splitMany I s).boxes), ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
Tactic: refine Finset.sum_congr rfl fun J' hJ' => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
have pos : ∀ (h : a.2 ∈ Set.Ioo (J'.lower a.1) (J'.upper a.1)), ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
Tactic: by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
pos : ∀ (h : a.2 ∈ Set.Ioo (J'.lower a.1) (J'.upper a.1)), ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
have neg : ∀ (h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)), ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
Tactic: by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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_1 : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∈ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
have pos : Option.elim' 0 f (J'.splitLower a.1 a.2) + Option.elim' 0 f (J'.splitUpper a.1 a.2) = f J'
Tactic: rw [sum_split_boxes]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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_1 : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
have neg : ∑ J' ∈ boxes (I := J') ⊤, f J' = f J'
Tactic: rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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_1 : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
neg : ∑ J' ∈ boxes (I := J') ⊤, f J' = f J'
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
have neg₁ : ∑ J' ∈ {J'}, f J' = f J'
Tactic: rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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_1 : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
neg : ∑ J' ∈ boxes (I := J') ⊤, f J' = f J'
neg₁ : ∑ J' ∈ {J'}, f J' = f J'
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
have neg₂ : f J' = f J'
Tactic: rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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₀
s : Finset (ι × ℝ)
⊢ ∑ J ∈ (splitMany I s).boxes, f J = f I
have empty : ∑ J ∈ (splitMany I ∅).boxes, f J = f I
Tactic: induction s using Finset.induction_on with
    | empty => simp
    | insert a s _ ihs =>
      rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
      refine Finset.sum_congr rfl fun J' hJ' => ?_
      by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
      · rw [sum_split_boxes]
        exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
      · rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (goal)
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₀
s : Finset (ι × ℝ)
empty : ∑ J ∈ (splitMany I ∅).boxes, f J = f I
⊢ ∑ J ∈ (splitMany I s).boxes, f J = f I
have insert : ∀ (a : ι × ℝ) (s : Finset (ι × ℝ)),
  a ∉ s → ∀ (ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I), ∑ J ∈ (splitMany I (insert a s)).boxes, f J = f I
Tactic: induction s using Finset.induction_on with
    | empty => simp
    | insert a s _ ihs =>
      rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
      refine Finset.sum_congr rfl fun J' hJ' => ?_
      by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
      · rw [sum_split_boxes]
        exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
      · rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (hypothesis)
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
⊢ ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
have hf₁ : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
Tactic: replace hf (I : Box ι) (hI : ↑I ≤ I₀) (s) : ∑ J ∈ (splitMany I s).boxes, f J = f I := by
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s _ ihs =>
      rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
      refine Finset.sum_congr rfl fun J' hJ' => ?_
      by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
      · rw [sum_split_boxes]
        exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
      · rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
Cleared hypotheses: hf