awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
e_f :
  ∀ (i : ι),
    (↑((Finset.sup Finset.univ fun (b : ι) ↦
              HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
                ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) /
            HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)
              ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) :
        ℝ) =
      (↑(HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0)
            (Finset.sup Finset.univ fun (b : ι) ↦ (Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
            ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)) :
        ℝ)
⊢ Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (i : ι) ↦
      (Finset.sup Finset.univ fun (b : ι) ↦
          HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
            ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) /
        HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)
          ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0))
    (Finset.sup Finset.univ fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0)
        (Finset.sup Finset.univ fun (b : ι) ↦ (Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
        ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0))

Tactic:
congr 1 with i
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
by_contra : ∀ (hr : ¬0 < r), False
⊢ 0 < r

Tactic:
by_contra hr
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
⊢ (J.upper i - J.lower i) / r ≤ 0

Tactic:
have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : (J.upper i - J.lower i) / r ≤ 0
⊢ I.upper i - I.lower i ≤ 0

Tactic:
rw [← h] at this
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : I.upper i - I.lower i ≤ 0
⊢ False

Tactic:
this.not_gt (sub_pos.2 <| I.lower_lt_upper i)

Premises used: Iff.mpr, sub_pos, LE.le.not_gt, BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
hr : ¬0 < r
this : I.upper i - I.lower i ≤ 0
⊢ False

Tactic:
exact this.not_gt (sub_pos.2 <| I.lower_lt_upper i)

Premises used: Iff.mpr, sub_pos, LE.le.not_gt, BoxIntegral.Box.lower_lt_upper
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
⊢ 0 < r

Tactic:
have : 0 < r := by
    by_contra hr
    have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
    rw [← h] at this
    exact this.not_gt (sub_pos.2 <| I.lower_lt_upper i)
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
⊢ Ne (α := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0) (0 : ℝ≥0)

Tactic:
have hn0 := (map_ne_zero Real.nnabs).2 this.ne'
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
hn0 : Ne (α := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0) (0 : ℝ≥0)
e_f :
  (↑(Finset.sup Finset.univ fun (a : ι) ↦
          HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper a - J.lower a) : ℝ≥0)
              ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0) /
            HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)
              ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) :
      ℝ) =
    (↑(Finset.sup Finset.univ fun (a : ι) ↦
          HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper a - J.lower a) : ℝ≥0)
            ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)) :
      ℝ)
⊢ (↑((Finset.sup Finset.univ fun (b : ι) ↦
            HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
              ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) /
          HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)
            ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0)) :
      ℝ) =
    (↑(HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0)
          (Finset.sup Finset.univ fun (b : ι) ↦ (Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper b - J.lower b) : ℝ≥0)
          ((Real.nnabs : (a : ℝ) → ℝ≥0) (J.upper i - J.lower i) : ℝ≥0)) :
      ℝ)

Tactic:
simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right₀ hn0]

Premises used: div_div_div_cancel_right₀, NNReal.finset_sup_div
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
grw :
  nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤
    (Finset.sup Finset.univ fun (i : ι) ↦ nndist I.lower I.upper / nndist (I.lower i) (I.upper i)) *
      nndist (I.lower i) (I.upper i)
grw₁ grw₂ :
  nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤
    nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i)
⊢ nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤
    I.distortion * nndist (I.lower i) (I.upper i)

Tactic:
grw [distortion, ← Finset.le_sup (Finset.mem_univ i)]

Premises used: Finset.mem_univ, BoxIntegral.Box.distortion, Finset.le_sup
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
⊢ I.lower i - I.upper i < 0

Tactic:
have A : I.lower i - I.upper i < 0 := sub_neg.2 (I.lower_lt_upper i)
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
A : I.lower i - I.upper i < 0
⊢ dist I.lower I.upper ≤ (↑I.distortion : ℝ) * (I.upper i - I.lower i)

Tactic:
simpa only [← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mul, Real.dist_eq, abs_of_neg A,
    neg_sub] using I.nndist_le_distortion_mul i

Premises used: neg_sub, abs_of_neg, BoxIntegral.Box.nndist_le_distortion_mul, dist_nndist, Real.dist_eq, NNReal.coe_mul, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ (↑c : ℝ) * (I.upper i - I.lower i)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
y : ι → ℝ
hy : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) y
ha : 0 ≤ I.upper i - I.lower i
⊢ (↑I.distortion : ℝ) * (I.upper i - I.lower i) ≤ (↑c : ℝ) * (I.upper i - I.lower i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ (↑c : ℝ) * (I.upper i - I.lower i)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
y : ι → ℝ
hy : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) y
⊢ 0 ≤ I.upper i - I.lower i

Tactic:
sub_nonneg.2 (I.lower_le_upper i)

Premises used: Iff.mpr, BoxIntegral.Box.lower_le_upper, sub_nonneg
-- Module: Mathlib.Analysis.BoxIntegral.Box.Basic
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ (↑c : ℝ) * (I.upper i - I.lower i)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x
y : ι → ℝ
hy : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) y
⊢ 0 ≤ I.upper i - I.lower i

Tactic:
exact sub_nonneg.2 (I.lower_le_upper i)

Premises used: Iff.mpr, BoxIntegral.Box.lower_le_upper, sub_nonneg
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I_1 J I : Box ι
s : Set ι
i : ι
pos : i ∈ s → (I.lower i + I.upper i) / 2 < I.upper i
neg : i ∉ s → I.lower i < (I.lower i + I.upper i) / 2
⊢ (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i) < if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2

Tactic:
split_ifs
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I_1 J I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ (I.lower i + I.upper i) / 2 < I.upper i

Tactic:
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]

Premises used: BoxIntegral.Box.lower_lt_upper, add_div_two_lt_right, left_lt_add_div_two
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I_1 J I : Box ι
s : Set ι
i : ι
h : i ∉ s
⊢ I.lower i < (I.lower i + I.upper i) / 2

Tactic:
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]

Premises used: BoxIntegral.Box.lower_lt_upper, add_div_two_lt_right, left_lt_add_div_two
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
simp :
  (∀ (i : ι),
      y i ∈
        Ioc (s.piecewise (β := fun (a : ι) ↦ ℝ) (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) I.lower i)
          (s.piecewise (β := fun (a : ι) ↦ ℝ) I.upper (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Ioc (I.lower x) (I.upper x) ∧ ((I.lower x + I.upper x) / 2 < y x ↔ x ∈ s)
⊢ y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s

Tactic:
simp only [splitCenterBox, mem_def, ← forall_and]

Premises used: BoxIntegral.Box.splitCenterBox, BoxIntegral.Box.mem_def, forall_and
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Ioc (s.piecewise (β := fun (a : ι) ↦ ℝ) (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) I.lower i)
          (s.piecewise (β := fun (a : ι) ↦ ℝ) I.upper (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Ioc (I.lower x) (I.upper x) ∧ ((I.lower x + I.upper x) / 2 < y x ↔ x ∈ s)

Tactic:
forall_congr' fun i ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
refine :
  ∀ (i : ι),
    y i ∈
        Ioc (s.piecewise (β := fun (a : ι) ↦ ℝ) (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) I.lower i)
          (s.piecewise (β := fun (a : ι) ↦ ℝ) I.upper (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) i) ↔
      y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
⊢ (∀ (i : ι),
      y i ∈
        Ioc (s.piecewise (β := fun (a : ι) ↦ ℝ) (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) I.lower i)
          (s.piecewise (β := fun (a : ι) ↦ ℝ) I.upper (fun (i : ι) ↦ (I.lower i + I.upper i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Ioc (I.lower x) (I.upper x) ∧ ((I.lower x + I.upper x) / 2 < y x ↔ x ∈ s)

Tactic:
refine forall_congr' fun i ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
pos :
  ∀ (hs : i ∈ s),
    y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
      y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
neg :
  ∀ (hs : i ∉ s),
    y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
      y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
⊢ y i ∈
      Ioc (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i)
        (if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
split_ifs with hs
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
pos :
  y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
simp only [hs, iff_true, iff_false, not_lt]

Premises used: iff_false, iff_true, not_lt
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
neg :
  y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ y i ≤ (I.lower i + I.upper i) / 2
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
simp only [hs, iff_true, iff_false, not_lt]

Premises used: iff_false, iff_true, not_lt
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i

Tactic:
⟨fun H ↦ ⟨⟨(left_lt_add_div_two.2 (I.lower_lt_upper i)).trans H.1, H.2⟩, H.1⟩,
      fun H ↦ ⟨H.2, H.1.2⟩⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Iff.intro, LT.lt.trans, BoxIntegral.Box.lower_lt_upper, left_lt_add_div_two
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ y i ≤ (I.lower i + I.upper i) / 2

Tactic:
⟨fun H ↦ ⟨⟨H.1, H.2.trans (add_div_two_lt_right.2 (I.lower_lt_upper i)).le⟩, H.2⟩,
      fun H ↦ ⟨H.1.1, H.2⟩⟩

Premises used: Iff.mpr, LT.lt.le, And.right, And.left, And.intro, Iff.intro, BoxIntegral.Box.lower_lt_upper, LE.le.trans, add_div_two_lt_right
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i

Tactic:
exacts [⟨fun H ↦ ⟨⟨(left_lt_add_div_two.2 (I.lower_lt_upper i)).trans H.1, H.2⟩, H.1⟩,
      fun H ↦ ⟨H.2, H.1.2⟩⟩,
    ⟨fun H ↦ ⟨⟨H.1, H.2.trans (add_div_two_lt_right.2 (I.lower_lt_upper i)).le⟩, H.2⟩,
      fun H ↦ ⟨H.1.1, H.2⟩⟩]
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
⊢ I.splitCenterBox s ≤ I

Tactic:
fun _ hx ↦ (mem_splitCenterBox.1 hx).1

Premises used: BoxIntegral.Box.mem_splitCenterBox, And.left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
rw : (↑(I.splitCenterBox s) : Set (ι → ℝ)) ⊓ (↑(I.splitCenterBox t) : Set (ι → ℝ)) ≤ ⊥
⊢ Disjoint (↑(I.splitCenterBox s) : Set (ι → ℝ)) (↑(I.splitCenterBox t) : Set (ι → ℝ))

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ (↑(I.splitCenterBox s) : Set (ι → ℝ))
ht : y ∈ (↑(I.splitCenterBox t) : Set (ι → ℝ))
apply : s = t
⊢ Membership.mem (γ := Set (ι → ℝ)) ⊥ y

Tactic:
apply h
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ (↑(I.splitCenterBox s) : Set (ι → ℝ))
ht : y ∈ (↑(I.splitCenterBox t) : Set (ι → ℝ))
h₁ : ∀ (i : ι), i ∈ s ↔ i ∈ t
⊢ s = t

Tactic:
ext i
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ (↑(I.splitCenterBox s) : Set (ι → ℝ))
ht : y ∈ (↑(I.splitCenterBox t) : Set (ι → ℝ))
i : ι
h₁ :
  ∀ (hs : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
    (ht : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t) (i : ι), i ∈ s ↔ i ∈ t
⊢ i ∈ s ↔ i ∈ t

Tactic:
rw [mem_coe, mem_splitCenterBox] at hs ht

Premises used: BoxIntegral.Box.mem_splitCenterBox, BoxIntegral.Box.mem_coe
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t
i : ι
h₁ : (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t
h₂ h₃ : (I.lower i + I.upper i) / 2 < y i ↔ (I.lower i + I.upper i) / 2 < y i
⊢ i ∈ s ↔ i ∈ t

Tactic:
rw [← hs.2, ← ht.2]

Premises used: And.right
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
⊢ Injective I.splitCenterBox

Tactic:
fun _ _ H ↦
  by_contra fun Hne ↦ (I.disjoint_splitCenterBox Hne).ne (nonempty_coe _).ne_empty (H ▸ rfl)

Premises used: BoxIntegral.Box.disjoint_splitCenterBox, Set.Nonempty.ne_empty, BoxIntegral.Box.splitCenterBox, Eq.rec, BoxIntegral.Box.nonempty_coe, by_contra, Disjoint.ne, Function.Injective, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
x : ι → ℝ
⊢ (∃ (s : Set ι), x ∈ I.splitCenterBox s) ↔ x ∈ I

Tactic:
⟨fun ⟨s, hs⟩ ↦ I.splitCenterBox_le s hs, fun hx ↦
    ⟨{ i | (I.lower i + I.upper i) / 2 < x i }, mem_splitCenterBox.2 ⟨hx, fun _ ↦ Iff.rfl⟩⟩⟩

Premises used: BoxIntegral.Box.splitCenterBox_le, Iff.mpr, Iff.rfl, setOf, Membership.mem, BoxIntegral.Box.upper, HDiv.hDiv, BoxIntegral.Box.mem_splitCenterBox, BoxIntegral.Box.lower, HAdd.hAdd, And.intro, LT.lt, Iff.intro, Exists.intro, OfNat.ofNat, _private.0.BoxIntegral.Box.exists_mem_splitCenterBox.match_1
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
h :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) (⋃ (s : Set ι), (↑(I.splitCenterBox s) : Set (ι → ℝ))) x ↔ x ∈ (↑I : Set (ι → ℝ))
⊢ ⋃ (s : Set ι), (↑(I.splitCenterBox s) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ))

Tactic:
ext x
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
x : ι → ℝ
⊢ Membership.mem (γ := Set (ι → ℝ)) (⋃ (s : Set ι), (↑(I.splitCenterBox s) : Set (ι → ℝ))) x ↔ x ∈ (↑I : Set (ι → ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
pos : i ∈ s → (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
neg : i ∉ s → (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Tactic:
by_cases i ∈ s
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h : i ∈ s
pos : I.upper i * 2 - (I.lower i + I.upper i) = I.upper i - I.lower i
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Tactic:
simp [field, splitCenterBox, *]

Premises used: BoxIntegral.Box.splitCenterBox
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h : i ∉ s
neg : I.lower i + I.upper i - I.lower i * 2 = I.upper i - I.lower i
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Tactic:
simp [field, splitCenterBox, *]

Premises used: BoxIntegral.Box.splitCenterBox
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ I.upper i * 2 - (I.lower i + I.upper i) = I.upper i - I.lower i

Tactic:
ring
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h : i ∉ s
⊢ I.lower i + I.upper i - I.lower i * 2 = I.upper i - I.lower i

Tactic:
ring
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
by_contra : ∀ (hpI : ¬p I), False
⊢ p I

Tactic:
by_contra hpI
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
hpI : ¬p I
⊢ ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬∀ (s : Set ι), p (J.splitCenterBox s)

Tactic:
replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
hpI : ¬p I
H_ind : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬∀ (s : Set ι), p (J.splitCenterBox s)
⊢ ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ∃ (x : Set ι), ¬p (J.splitCenterBox x)

Tactic:
simp only [not_forall] at H_ind

Premises used: Classical.not_forall
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
hpI : ¬p I
H_ind : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ∃ (x : Set ι), ¬p (J.splitCenterBox x)
choose! : ∀ (s : (J : Box ι) → Set ι) (hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))), False
⊢ False

Tactic:
choose! s hs using H_ind
-- Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
Goal:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) z →
      ∃ U ∈ 𝓝[(Box.Icc : (a : Box ι) → Set (ι → ℝ)) I] z,
        ∀ J ≤ I,
          ∀ (m : ℕ),
            Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) z →
              (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ U →
                (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / HPow.hPow (α := ℝ) 2 m) → p J
hpI : ¬p I
s : (J : Box ι) → Set ι
hs : ∀ (J : Box ι) (hJ : J ≤ I), ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun (m : ℕ) ↦ (fun (J : Box ι) ↦ J.splitCenterBox (s J))^[m] I
⊢ ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))

Tactic:
have J_succ : ∀ m, J (m + 1) = splitCenterBox (J m) (s <| J m) :=
    fun m ↦ iterate_succ_apply' _ _ _