awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
⊢ ∑ Ji ∈ π.boxes, f Ji = f I
have Hle : ∀ 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
-- 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 ι) (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₀
⊢ ∑ Ji ∈ π.boxes, f Ji = f I
have rcases : ∀ (s : Finset (ι × ℝ)) (hs : splitMany I s ≤ π), ∑ Ji ∈ π.boxes, f Ji = f I
Tactic: rcases hπ.exists_splitMany_le with ⟨s, hs⟩
-- 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 ι) (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 ≤ π
⊢ ∑ Ji ∈ π.boxes, f Ji = f I
have rw : Eq.{u_2 + 1} (α := M) (∑ Ji ∈ π.boxes, f Ji) (∑ J ∈ π.boxes, ∑ J' ∈ (splitMany J s).boxes, f J')
Tactic: rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, 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 : 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: classical
  refine ⟨f, ?_⟩
  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]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
-- 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
refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
⊢ ι →ᵇᵃ[I₀] M
have refine₁ : ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
  (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
Tactic: classical
  refine ⟨f, ?_⟩
  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]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
Cleared hypotheses: hf
-- 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
refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₁ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₂ :
  ∀ (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), ∑ Ji ∈ π.boxes, f Ji = f I
⊢ ι →ᵇᵃ[I₀] M
have refine₃ : ∀ (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₀), ∑ Ji ∈ π.boxes, f Ji = f I
Tactic: classical
  refine ⟨f, ?_⟩
  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]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
Cleared hypotheses: hf
-- 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
refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₁ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₂ :
  ∀ (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), ∑ Ji ∈ π.boxes, f Ji = f I
refine₃ :
  ∀ (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₀), ∑ Ji ∈ π.boxes, f Ji = f I
⊢ ι →ᵇᵃ[I₀] M
have refine₄ : ∀ (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 ≤ π), ∑ Ji ∈ π.boxes, f Ji = f I
Tactic: classical
  refine ⟨f, ?_⟩
  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]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
Cleared hypotheses: hf
-- 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
refine : ∀ (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₁ :
  ∀ (hf : ∀ (I : Box ι) (hI : (↑I : WithTop (Box ι)) ≤ I₀) (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I)
    (J : Box ι), (↑J : WithTop (Box ι)) ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J
refine₂ :
  ∀ (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), ∑ Ji ∈ π.boxes, f Ji = f I
refine₃ :
  ∀ (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₀), ∑ Ji ∈ π.boxes, f Ji = f I
refine₄ :
  ∀ (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 ≤ π),
    ∑ Ji ∈ π.boxes, f Ji = f I
⊢ ι →ᵇᵃ[I₀] M
have refine₅ : ∀ (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: classical
  refine ⟨f, ?_⟩
  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]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
Cleared hypotheses: hf
-- 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_1 : Box ι
i : ι
f : ι →ᵇᵃ[I₀] M
g : M →+ N
I : Box ι
hI : (↑I : WithTop (Box ι)) ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ 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)
have 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)
Tactic: simp_rw [comp, ← map_sum, f.sum_partition_boxes hI 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_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)
⊢ 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)
have 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)
Tactic: simp_rw [comp, ← map_sum, f.sum_partition_boxes hI 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 ι
inst_1 : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : (↑I : WithTop (Box ι)) ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)
have 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)
Tactic: rcases exists_splitMany_inf_eq_filter_of_finite {π₁, π₂} ((finite_singleton _).insert _) with
    ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)
have 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
Tactic: simp only [inf_splitMany] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)
have h₁ : (π₁.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₂⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)
have h₂ : (π₂.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₂⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Additive (hypothesis)
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, (f : (a : Box ι) → M) J)
have h₃ : (π₁.biUnion fun (J : Box ι) ↦ splitMany J s) = (splitMany I s).filter fun (J : Box ι) ↦ (↑J : Set (ι → ℝ)) ⊆ π₂.iUnion
Tactic: rw [h] at h₁
Cleared hypotheses: h₁, 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 ι
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 ∈ (π₂.biUnion fun (J : Box ι) ↦ splitMany J s).boxes, (f : (a : Box ι) → M) J)
have 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)
Tactic: rw [h₁, 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 ι
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)
⊢ 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)
have 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)
Tactic: rw [h₁, 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 ι
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, (f : (a : Box ι) → M) J)
have calc_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.boxes), (↑J : WithTop (Box ι)) ≤ I₀
Tactic: calc
    ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₁.boxes, ∑ J' ∈ (splitMany J s).boxes, f J' :=
      Finset.sum_congr rfl fun J hJ => (f.sum_partition_boxes ?_ (isPartition_splitMany _ _)).symm
    _ = ∑ J ∈ (π₁.biUnion fun J => splitMany J s).boxes, f J := (sum_biUnion_boxes _ _ _).symm
    _ = ∑ J ∈ (π₂.biUnion fun J => splitMany J s).boxes, f J := by rw [h₁, h₂]
    _ = ∑ J ∈ π₂.boxes, ∑ J' ∈ (splitMany J s).boxes, f J' := sum_biUnion_boxes _ _ _
    _ = ∑ J ∈ π₂.boxes, f J :=
      Finset.sum_congr rfl fun J hJ => f.sum_partition_boxes ?_ (isPartition_splitMany _ _)