awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
calc_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.boxes), (↑J : WithTop (Box ι)) ≤ I₀
calc_2 : ∀ (J : Box ι) (hJ : J ∈ π₂.boxes), (↑J : WithTop (Box ι)) ≤ I₀
⊢ Eq.{u_2 + 1} (α := M) (∑ J ∈ π₁.boxes, (f : (a : Box ι) → M) J) (∑ J ∈ π₂.boxes, (f : (a : Box ι) → M) J)

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 _ _)

Premises used: BoxIntegral.Prepartition.sum_biUnion_boxes, BoxIntegral.Prepartition.boxes, BoxIntegral.BoxAdditiveMap.sum_partition_boxes, BoxIntegral.Prepartition.biUnion, Eq.symm, BoxIntegral.Prepartition.splitMany, 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
J : Box ι
hJ : J ∈ π₁.boxes
⊢ (↑J : WithTop (Box ι)) ≤ I₀

Tactic:
(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI

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
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
J : Box ι
hJ : J ∈ π₂.boxes
⊢ (↑J : WithTop (Box ι)) ≤ I₀

Tactic:
(WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI

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
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
J : Box ι
hJ : J ∈ π₁.boxes
⊢ (↑J : WithTop (Box ι)) ≤ I₀

Tactic:
exacts [(WithTop.coe_le_coe.2 <| π₁.le_of_mem hJ).trans hI,
    (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI]

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
I₀ : WithTop (Box ι)
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ι →ᵇᵃ[I₀] ℝ
I : Box ι
x : E
⊢ (((f.toSMul : (a : Box ι) → E →L[ℝ] E) I : E →L[ℝ] E) : (a : E) → E) x =
    HSMul.hSMul (α := ℝ) ((f : (a : Box ι) → ℝ) I : ℝ) x

Tactic:
rfl

Premises used: 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : (↑J : WithTop (Box (Fin (n + 1)))) ≤ (↑I₀ : WithTop (Box (Fin (n + 1))))
j : Fin (n + 1)
x : ℝ
rw :
  ∀ (hJ : J ≤ I₀) {j : Fin (n + 1)} {x : ℝ},
    x ∈ Set.Ioo (J.lower j) (J.upper j) →
      HAdd.hAdd (α := G)
          (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
            (J.splitLower j x))
          (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
            (J.splitUpper j x)) =
        (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J
⊢ x ∈ Set.Ioo (J.lower j) (J.upper j) →
    HAdd.hAdd (α := G)
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitLower j x))
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitUpper j x)) =
      (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J

Tactic:
rw [WithTop.coe_le_coe] at hJ

Premises used: 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 : Box ι
i_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
⊢ x ∈ Set.Ioo (J.lower j) (J.upper j) →
    HAdd.hAdd (α := G)
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitLower j x))
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitUpper j x)) =
      (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J

Tactic:
i.succAboveCases (fun hx => ?_) (fun j hx => ?_) j

Premises used: Fin.succAboveCases
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
refine_1 :
  ∀ (hx : x ∈ Set.Ioo (J.lower i) (J.upper i)),
    HAdd.hAdd (α := G)
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitLower i x))
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitUpper i x)) =
      (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J
refine_2 :
  ∀ (j : Fin n) (hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))),
    HAdd.hAdd (α := G)
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitLower (i.succAbove j) x))
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitUpper (i.succAbove j) x)) =
      (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J
⊢ x ∈ Set.Ioo (J.lower j) (J.upper j) →
    HAdd.hAdd (α := G)
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitLower j x))
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitUpper j x)) =
      (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J

Tactic:
refine i.succAboveCases (fun hx => ?_) (fun j hx => ?_) j
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (J.lower i) (J.upper i)
refine_1 :
  f x
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) } -
        f (J.lower i)
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) } +
      (f (J.upper i)
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) } -
        f x
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) }) =
    f (J.upper i)
        { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
          lower_lt_upper := ⋯ : Box (Fin n) } -
      f (J.lower i)
        { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
          lower_lt_upper := ⋯ : Box (Fin n) }
⊢ HAdd.hAdd (α := G)
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitLower i x))
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitUpper i x)) =
    (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J

Tactic:
simp only [Box.splitLower_def hx, Box.splitUpper_def hx, update_self, ← WithBot.some_eq_coe,
          Option.elim', Box.face, Function.comp_def, update_of_ne (Fin.succAbove_ne _ _)]

Premises used: Iff.mpr, BoxIntegral.Box.splitLower_def, Option.elim', BoxIntegral.Box.face, BoxIntegral.Box.splitUpper_def, Fin.succAbove_ne, BoxIntegral.Box.upper, Function.comp_def, BoxIntegral.Box.lower, And.right, Function.forall_update_iff, And.left, WithBot.some_eq_coe, And.intro, LT.lt, BoxIntegral.Box.lower_lt_upper, Function.update_self, Function.update_of_ne
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (J.lower i) (J.upper i)
⊢ f x
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) } -
        f (J.lower i)
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) } +
      (f (J.upper i)
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) } -
        f x
          { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
            lower_lt_upper := ⋯ : Box (Fin n) }) =
    f (J.upper i)
        { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
          lower_lt_upper := ⋯ : Box (Fin n) } -
      f (J.lower i)
        { lower := fun (x : Fin n) ↦ J.lower (i.succAbove x), upper := fun (x : Fin n) ↦ J.upper (i.succAbove x),
          lower_lt_upper := ⋯ : Box (Fin n) }

Tactic:
abel
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j_1 : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
⊢ (↑(J.face i) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))

Tactic:
have : (J.face i : WithTop (Box (Fin n))) ≤ I₀.face i :=
          WithTop.coe_le_coe.2 (face_mono hJ i)
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j_1 : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : (↑(J.face i) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))
refine_2 :
  ∀
    (hJ :
      Subset (α := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ))
        (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Icc (I₀.lower i) (I₀.upper i) :
          Set ((i : Fin (n + 1)) → ℝ)))
    {j : Fin (n + 1)} {x : ℝ} (j : Fin n) (hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j)))
    (this : (↑(J.face i) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))),
    HAdd.hAdd (α := G)
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitLower (i.succAbove j) x))
        (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
          (J.splitUpper (i.succAbove j) x)) =
      (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J
⊢ HAdd.hAdd (α := G)
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitLower (i.succAbove j) x))
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitUpper (i.succAbove j) x)) =
    (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J

Tactic:
rw [le_iff_Icc, @Box.Icc_eq_pi _ I₀] at hJ

Premises used: BoxIntegral.Box.le_iff_Icc, BoxIntegral.Box.Icc_eq_pi
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ :
  Subset (α := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ))
    (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Icc (I₀.lower i) (I₀.upper i) :
      Set ((i : Fin (n + 1)) → ℝ))
j_1 : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : (↑(J.face i) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))
refine_2 :
  HAdd.hAdd (α := G)
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitLower (i.succAbove j) x))
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitUpper (i.succAbove j) x)) =
    HAdd.hAdd (α := G)
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.upper i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitLower j x))
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.upper i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitUpper j x)) -
      HAdd.hAdd (α := G)
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.lower i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitLower j x))
        (Option.elim' 0
          (⇑(fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J.lower i) ⋯)) :
            (a : Box (Fin n)) → G)
          ((J.face i).splitUpper j x))
⊢ HAdd.hAdd (α := G)
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitLower (i.succAbove j) x))
      (Option.elim' 0 (fun (J : Box (Fin (n + 1))) ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i))
        (J.splitUpper (i.succAbove j) x)) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)

Tactic:
rw [hf _ (hJ J.upper_mem_Icc _ trivial), hf _ (hJ J.lower_mem_Icc _ trivial),
          ← (fb _).map_split_add this j x, ← (fb _).map_split_add this j x]

Premises used: BoxIntegral.BoxAdditiveMap.map_split_add, BoxIntegral.Box.upper_mem_Icc, trivial, BoxIntegral.Box.lower_mem_Icc
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ :
  Subset (α := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ))
    (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Icc (I₀.lower i) (I₀.upper i) :
      Set ((i : Fin (n + 1)) → ℝ))
j_1 : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : (↑(J.face i) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))
⊢ x ∈ Set.Ioo ((J.face i).lower j) ((J.face i).upper j)

Tactic:
have hx' : x ∈ Ioo ((J.face i).lower j) ((J.face i).upper j) := hx
-- 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_1 : ι
G : Type u
inst_2 : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : (↑(Set.Icc (I₀.lower i) (I₀.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I₀.face i) : WithTop (Box (Fin n)))] G
hf :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)),
    f x J = (fb (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) x hx) : (a : Box (Fin n)) → G) J
J : Box (Fin (n + 1))
hJ :
  Subset (α := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ))
    (Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Icc (I₀.lower i) (I₀.upper i) :
      Set ((i : Fin (n + 1)) → ℝ))
j_1 : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : (↑(J.face i) : WithTop (Box (Fin n))) ≤ (↑(I₀.face i) : WithTop (Box (Fin n)))
hx' : x ∈ Set.Ioo ((J.face i).lower j) ((J.face i).upper j)
⊢ f (J.upper i)
          { lower := J.lower ∘ i.succAbove, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.upper ∘ i.succAbove) j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.upper i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.lower ∘ i.succAbove) j x, upper := J.upper ∘ i.succAbove,
            lower_lt_upper := ⋯ : Box (Fin n) } -
      (f (J.lower i)
          { lower := J.lower ∘ i.succAbove, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.upper ∘ i.succAbove) j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.lower i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.lower ∘ i.succAbove) j x, upper := J.upper ∘ i.succAbove,
            lower_lt_upper := ⋯ : Box (Fin n) }) =
    f (J.upper i)
          { lower := (J.face i).lower, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).upper j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.upper i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).lower j x, upper := (J.face i).upper,
            lower_lt_upper := ⋯ : Box (Fin n) } -
      (f (J.lower i)
          { lower := (J.face i).lower, upper := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).upper j x,
            lower_lt_upper := ⋯ : Box (Fin n) } +
        f (J.lower i)
          { lower := update (β := fun (a : Fin n) ↦ ℝ) (J.face i).lower j x, upper := (J.face i).upper,
            lower_lt_upper := ⋯ : Box (Fin n) })

Tactic:
simp only [Box.face]

Premises used: BoxIntegral.Box.face
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Basic
Goal:
ι : Type u_1
I J : Box ι
π : Prepartition I
⊢ J ∈ π.boxes ↔ J ∈ π

Tactic:
Iff.rfl

Premises used: Iff.rfl