awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
calc_1 : ∀ (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)
have calc_2 : ∀ (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 _ _)
-- 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_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 : ℝ
⊢ 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
have 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
Tactic: rw [WithTop.coe_le_coe] at hJ
Cleared hypotheses: hJ, j, x
-- 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_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
have 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
Tactic: refine i.succAboveCases (fun hx => ?_) (fun j hx => ?_) j
-- 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_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
⊢ 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
have 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
Tactic: refine i.succAboveCases (fun hx => ?_) (fun j hx => ?_) j
-- 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_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)
⊢ 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
have 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : Box (Fin n) }
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 _ _)]
-- 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_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))
⊢ 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
have this : (↑(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)
-- 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_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)))
⊢ 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
have 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
Tactic: rw [le_iff_Icc, @Box.Icc_eq_pi _ I₀] at hJ
Cleared hypotheses: hJ, j_1, x, j, hx, this
-- 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_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)))
⊢ 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)
have 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) sorry)) :
          (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) sorry)) :
          (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) sorry)) :
          (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) sorry)) :
          (a : Box (Fin n)) → G)
        ((J.face i).splitUpper j x))
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]
-- 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_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)))
⊢ 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))
have hx' : 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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ ∀ (a b : Prepartition I), a ≤ b → b ≤ a → a = b
have suffices : ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes
Tactic: suffices ∀ {π₁ π₂ : Prepartition I}, π₁ ≤ π₂ → π₂ ≤ π₁ → π₁.boxes ⊆ π₂.boxes from
      fun π₁ π₂ h₁ h₂ => injective_boxes (Subset.antisymm (this h₁ h₂) (this h₂ h₁))
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
⊢ J ∈ π₂.boxes
have rcases : ∀ (J' : Box ι) (hJ' : J' ∈ π₂) (hle : J ≤ J'), J ∈ π₂.boxes
Tactic: rcases h₁ hJ with ⟨J', hJ', hle⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
⊢ J ∈ π₂.boxes
have rcases : ∀ (J'' : Box ι) (hJ'' : J'' ∈ π₁) (hle' : J' ≤ J''), J ∈ π₂.boxes
Tactic: rcases h₂ hJ' with ⟨J'', hJ'', hle'⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
J'' : Box ι
hJ'' : J'' ∈ π₁
hle' : J' ≤ J''
⊢ J ∈ π₂.boxes
have hJ''₁ : J ∈ π₁
Tactic: obtain rfl : J = J'' := π₁.eq_of_le hJ hJ'' (hle.trans hle')
Cleared hypotheses: J'', hJ'', hle'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
J'' : Box ι
hJ'' : J'' ∈ π₁
hle' : J' ≤ J''
hJ''₁ : J ∈ π₁
⊢ J ∈ π₂.boxes
have hle'₁ : J' ≤ J
Tactic: obtain rfl : J = J'' := π₁.eq_of_le hJ hJ'' (hle.trans hle')
Cleared hypotheses: J'', hJ'', hle'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I J_1 J₁ J₂ : Box ι
π π₁_1 π₂_1 : Prepartition I
x : ι → ℝ
π₁ π₂ : Prepartition I
h₁ : π₁ ≤ π₂
h₂ : π₂ ≤ π₁
J : Box ι
hJ : J ∈ π₁.boxes
J' : Box ι
hJ' : J' ∈ π₂
hle : J ≤ J'
hJ'' : J ∈ π₁
hle' : J' ≤ J
⊢ J ∈ π₂.boxes
have obtain : ∀ (hJ : J' ∈ π₁.boxes) (hle : J' ≤ J') (hJ'' : J' ∈ π₁) (hle' : J' ≤ J'), J' ∈ π₂.boxes
Tactic: obtain rfl : J' = J := le_antisymm ‹_› ‹_›
Cleared hypotheses: J, hJ, hle, hJ'', hle'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
this : ∀ (i : ι), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
⊢ J₁ = J₂
have choose : ∀ (y : (i : ι) → ℝ) (hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (J₁.lower i) (J₁.upper i))
  (hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (J₂.lower i) (J₂.upper i)), J₁ = J₂
Tactic: choose y hy₁ hy₂ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
⊢ J₁ = J₂
have suffices : ∀ (i : ι), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
Tactic: suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty by
    choose y hy₁ hy₂ using this
    exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (hypothesis)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
H : Eq.{u_1 + 1} (α := Set ι) {i : ι | J₁.lower i = x i} {i : ι | J₂.lower i = x i}
i : ι
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have H₁ : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
Tactic: simp only [Set.ext_iff, mem_setOf] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₁ : Set (ι → ℝ)) x
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J₂ : Set (ι → ℝ)) x
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
have inl : ∀ (hi₁ : J₁.lower i = x i), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
Tactic: rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁