awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (J' : Box ι) (hJ' : J' ∈ (splitMany I s).boxes), ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
⊢ 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:
refine Finset.sum_congr rfl fun J' hJ' => ?_

Premises used: Finset.sum_congr, rfl
-- 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
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'
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'
⊢ ∑ 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)

Premises used: BoxIntegral.Box.upper, Prod.fst, BoxIntegral.Box.lower, Prod.snd, Set.Ioo
-- 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_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)
pos : Option.elim' 0 f (J'.splitLower a.1 a.2) + Option.elim' 0 f (J'.splitUpper a.1 a.2) = f J'
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'

Tactic:
rw [sum_split_boxes]

Premises used: BoxIntegral.Prepartition.sum_split_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₀_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)
⊢ Option.elim' 0 f (J'.splitLower a.1 a.2) + Option.elim' 0 f (J'.splitUpper a.1 a.2) = f J'

Tactic:
hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, LE.le.trans, WithTop.coe_le_coe
-- 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_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)
⊢ Option.elim' 0 f (J'.splitLower a.1 a.2) + Option.elim' 0 f (J'.splitUpper a.1 a.2) = f J'

Tactic:
exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h

Premises used: Iff.mpr, BoxIntegral.Prepartition.le_of_mem, LE.le.trans, WithTop.coe_le_coe
-- 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_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'
neg₂ neg₃ : f J' = f J'
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'

Tactic:
rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]

Premises used: BoxIntegral.Prepartition.top_boxes, Finset.sum_singleton, BoxIntegral.Prepartition.split_of_notMem_Ioo
-- 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₀
s : Finset (ι × ℝ)
empty : ∑ J ∈ (splitMany I ∅).boxes, f J = f I
insert :
  ∀ (a : ι × ℝ) (s : Finset (ι × ℝ)),
    a ∉ s → ∀ (ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I), ∑ J ∈ (splitMany I (Insert.insert a s)).boxes, f J = f I
⊢ ∑ J ∈ (splitMany I 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]

Premises used: BoxIntegral.Prepartition.top_boxes, BoxIntegral.Prepartition.sum_biUnion_boxes, Insert.insert, BoxIntegral.Prepartition.inf_split, Finset.sum_singleton, BoxIntegral.Prepartition.biUnion_boxes, BoxIntegral.Prepartition.splitMany_insert, BoxIntegral.Prepartition.sum_split_boxes, Finset.sum_congr, rfl
-- 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
⊢ ∀ (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]
-- 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 ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀

Tactic:
have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
-- 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 ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀
rcases : ∀ (s : Finset (ι × ℝ)) (hs : splitMany I s ≤ π), ∑ Ji ∈ π.boxes, f Ji = f I
⊢ ∑ Ji ∈ π.boxes, f Ji = f I

Tactic:
rcases hπ.exists_splitMany_le with ⟨s, hs⟩

Premises used: BoxIntegral.Prepartition.IsPartition.exists_splitMany_le
-- 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 ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
rw : Eq.{u_2 + 1} (α := M) (∑ Ji ∈ π.boxes, f Ji) (∑ J ∈ π.boxes, ∑ J' ∈ (splitMany J s).boxes, f J')
⊢ ∑ Ji ∈ π.boxes, f Ji = f I

Tactic:
rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]

Premises used: BoxIntegral.Prepartition.sum_biUnion_boxes, inf_of_le_right, BoxIntegral.Prepartition.biUnion_boxes, BoxIntegral.Prepartition.inf_splitMany
-- 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 ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ Eq.{u_2 + 1} (α := M) (∑ Ji ∈ π.boxes, f Ji) (∑ J ∈ π.boxes, ∑ J' ∈ (splitMany J s).boxes, f J')

Tactic:
Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm

Premises used: Eq.symm, Finset.sum_congr, rfl
-- 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 ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, (↑J : WithTop (Box ι)) ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ Eq.{u_2 + 1} (α := M) (∑ Ji ∈ π.boxes, f Ji) (∑ J ∈ π.boxes, ∑ J' ∈ (splitMany J s).boxes, f J')

Tactic:
exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm

Premises used: Eq.symm, Finset.sum_congr, rfl
-- 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 : ι →ᵇᵃ[I₀] M
g : M →+ N
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
simp_rw :
  Eq.{u_3 + 1} (α := N) (∑ x ∈ π.boxes, (g : (a : M) → N) ((f : (a : Box ι) → M) x : M) : N)
    ((g : (a : M) → N) ((f : (a : Box ι) → M) I : M) : N)
simp_rw₁ :
  Eq.{u_3 + 1} (α := N) ((g : (a : M) → N) (∑ x ∈ π.boxes, (f : (a : Box ι) → M) x) : N)
    ((g : (a : M) → N) ((f : (a : Box ι) → M) I : M) : N)
⊢ Eq.{u_3 + 1} (α := N)
    (∑ Ji ∈ π.boxes, comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑g : (a : M) → N) (⇑f : (a : Box ι) → M) Ji)
    (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑g : (a : M) → N) (⇑f : (a : Box ι) → M) I)

Tactic:
simp_rw [comp, ← map_sum, f.sum_partition_boxes hI hπ]

Premises used: Function.comp, map_sum, BoxIntegral.BoxAdditiveMap.sum_partition_boxes
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
rcases :
  ∀ (s : Finset (ι × ℝ))
    (hs :
      ∀ (π : Prepartition I),
        Membership.mem (γ := Set (Prepartition I)) {π₁, π₂} π →
          π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion),
    Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)

Tactic:
rcases exists_splitMany_inf_eq_filter_of_finite {π₁, π₂} ((finite_singleton _).insert _) with
    ⟨s, hs⟩

Premises used: Insert.insert, BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite, Set.Finite.insert, Singleton.singleton, Set.finite_singleton
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    Membership.mem (γ := Set (Prepartition I)) {π₁, π₂} π →
      π ⊓ splitMany I s = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
⊢ ∀ (π : Prepartition I),
    Membership.mem (γ := Set (Prepartition I)) {π₁, π₂} π →
      (π.biUnion fun (J : Box ι) ↦ splitMany J s) =
        (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion

Tactic:
simp only [inf_splitMany] at hs

Premises used: BoxIntegral.Prepartition.inf_splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    Membership.mem (γ := Set (Prepartition I)) {π₁, π₂} π →
      (π.biUnion fun (J : Box ι) ↦ splitMany J s) =
        (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
⊢ (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₁.iUnion

Tactic:
rcases hs _ (Or.inl rfl), hs _ (Or.inr rfl) with ⟨h₁, h₂⟩

Premises used: Or.inl, Or.inr, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs :
  ∀ (π : Prepartition I),
    Membership.mem (γ := Set (Prepartition I)) {π₁, π₂} π →
      (π.biUnion fun (J : Box ι) ↦ splitMany J s) =
        (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π.iUnion
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₁.iUnion
⊢ (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion

Tactic:
rcases hs _ (Or.inl rfl), hs _ (Or.inr rfl) with ⟨h₁, h₂⟩

Premises used: Or.inl, Or.inr, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₁.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
⊢ (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion

Tactic:
rw [h] at h₁
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₁.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
h₃ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
⊢ (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion

Tactic:
rw [h] at h₁
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J)
    (∑ J ∈ π₁.boxes, ∑ J' ∈ (splitMany J s).boxes, (f : (a : Box ι) → M) J')

Tactic:
Finset.sum_congr rfl fun J hJ => (f.sum_partition_boxes ?_ (isPartition_splitMany _ _)).symm

Premises used: BoxIntegral.BoxAdditiveMap.sum_partition_boxes, Eq.symm, Finset.sum_congr, rfl, BoxIntegral.Prepartition.isPartition_splitMany
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, ∑ J' ∈ (splitMany J s).boxes, (f : (a : Box ι) → M) J')
    (∑ J ∈ (π₁.biUnion fun (J : Box ι) ↦ splitMany J s).boxes, (f : (a : Box ι) → M) J)

Tactic:
(sum_biUnion_boxes _ _ _).symm

Premises used: Multiset.toFinset, BoxIntegral.Prepartition.sum_biUnion_boxes, Finset.biUnion, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
rw :
  Eq.{u_2 + 1} (α := M)
    (∑ J ∈ ((splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion).boxes, (f : (a : Box ι) → M) J)
    (∑ J ∈ (π₂.biUnion fun (J : Box ι) ↦ splitMany J s).boxes, (f : (a : Box ι) → M) J)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := M)
    (∑ J ∈ ((splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion).boxes, (f : (a : Box ι) → M) J)
    (∑ J ∈ ((splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion).boxes, (f : (a : Box ι) → M) J)
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ (π₁.biUnion fun (J : Box ι) ↦ splitMany J s).boxes, (f : (a : Box ι) → M) J)
    (∑ J ∈ (π₂.biUnion fun (J : Box ι) ↦ splitMany J s).boxes, (f : (a : Box ι) → M) J)

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ (π₂.biUnion fun (J : Box ι) ↦ splitMany J s).boxes, (f : (a : Box ι) → M) J)
    (∑ J ∈ π₂.boxes, ∑ J' ∈ (splitMany J s).boxes, (f : (a : Box ι) → M) J')

Tactic:
sum_biUnion_boxes _ _ _

Premises used: Multiset.toFinset, BoxIntegral.Prepartition.sum_biUnion_boxes, Finset.biUnion
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Additive
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ :
  (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
h₂ :
  (π₂.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₂.boxes, ∑ J' ∈ (splitMany J s).boxes, (f : (a : Box ι) → M) J')
    (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)

Tactic:
Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _)

Premises used: BoxIntegral.BoxAdditiveMap.sum_partition_boxes, Finset.sum_congr, rfl, BoxIntegral.Prepartition.isPartition_splitMany