awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : WithBot (Box ι)
⊢ (↑(I ⊓ J) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
have bot : (↑(⊥ ⊓ J) : Set (ι → ℝ)) = (↑⊥ : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
Tactic: induction I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : WithBot (Box ι)
bot : (↑(⊥ ⊓ J) : Set (ι → ℝ)) = (↑⊥ : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
⊢ (↑(I ⊓ J) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
have coe : ∀ (a : Box ι),
  (↑((↑a : WithBot (Box ι)) ⊓ J) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
Tactic: induction I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
J : WithBot (Box ι)
a : Box ι
⊢ (↑((↑a : WithBot (Box ι)) ⊓ J) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
have coe : (↑((↑a : WithBot (Box ι)) ⊓ ⊥) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑⊥ : Set (ι → ℝ))
Tactic: induction J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
J : WithBot (Box ι)
a : Box ι
coe : (↑((↑a : WithBot (Box ι)) ⊓ ⊥) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑⊥ : Set (ι → ℝ))
⊢ (↑((↑a : WithBot (Box ι)) ⊓ J) : Set (ι → ℝ)) = (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))
have coe₁ : ∀ (a_1 : Box ι),
  (↑((↑a : WithBot (Box ι)) ⊓ (↑a_1 : WithBot (Box ι))) : Set (ι → ℝ)) =
    (↑(↑a : WithBot (Box ι)) : Set (ι → ℝ)) ∩ (↑(↑a_1 : WithBot (Box ι)) : Set (ι → ℝ))
Tactic: induction J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ I
have rw : (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))
Tactic: rw [← withBotCoe_subset_iff, coe_inf]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I_1 J_1 : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ J
have rw : (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑J : Set (ι → ℝ))
Tactic: rw [← withBotCoe_subset_iff, coe_inf]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I_1 J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : I ≤ J₁
h₂ : I ≤ J₂
⊢ I ≤ J₁ ⊓ J₂
have simp : ∀ (h₁ : (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ))) (h₂ : (↑I : Set (ι → ℝ)) ⊆ (↑J₂ : Set (ι → ℝ))),
  (↑I : Set (ι → ℝ)) ⊆ (↑J₁ : Set (ι → ℝ)) ∩ (↑J₂ : Set (ι → ℝ))
Tactic: simp only [← withBotCoe_subset_iff, coe_inf] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : WithBot (Box ι)
⊢ Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ)) ↔ Disjoint I J
have simp : (↑I : Set (ι → ℝ)) ⊓ (↑J : Set (ι → ℝ)) ≤ ⊥ ↔ (↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ)) ⊆ (↑⊥ : Set (ι → ℝ))
Tactic: simp only [disjoint_iff_inf_le, ← withBotCoe_subset_iff, coe_inf]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
⊢ ¬Disjoint (↑I : WithBot (Box ι)) (↑J : WithBot (Box ι)) ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
have rw : ¬Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ)) ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
Tactic: rw [disjoint_coe, Set.not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I J : Box ι
rw : ¬Disjoint (↑I : Set (ι → ℝ)) (↑J : Set (ι → ℝ)) ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
⊢ ¬Disjoint (↑I : WithBot (Box ι)) (↑J : WithBot (Box ι)) ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
have rw₁ : ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty ↔ ((↑I : Set (ι → ℝ)) ∩ (↑J : Set (ι → ℝ))).Nonempty
Tactic: rw [disjoint_coe, Set.not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : (j : Fin n) → ℝ
hy : y ∈ (↑(I.face i) : Set (Fin n → ℝ))
⊢ i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) x y ∈ (↑I : Set (Fin (n + 1) → ℝ))
have simp_rw : x ∈ Ioc (I.lower i) (I.upper i) ∧ ∀ (i_1 : Fin n), y i_1 ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))
Tactic: simp_rw [mem_coe, mem_def, i.forall_iff_succAbove, Fin.insertNth_apply_same,
    Fin.insertNth_apply_succAbove]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
I : Box ι
⊢ ∃ (J : ℕ →o Box ι),
    (∀ (n : ℕ),
        Subset (α := Set (ι → ℝ))
          ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) ((J : (a : ℕ) → Box ι) n : Box ι) : Set (ι → ℝ))
          ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))) ∧
      Tendsto (α := ℕ) (lower ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.lower) ∧
        Tendsto (α := ℕ) (upper ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.upper)
have choose : ∀ (a b : (i : ι) → ℕ → ℝ) (ha_anti : ∀ (i : ι), StrictAnti (a i)) (hb_mono : ∀ (i : ι), StrictMono (b i))
  (ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i))
  (hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)) (hab : ∀ (i : ι) (k l : ℕ), a i k < b i l)
  (ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i)))
  (hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))),
  ∃ (J : ℕ →o Box ι),
    (∀ (n : ℕ),
        Subset (α := Set (ι → ℝ))
          ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) ((J : (a : ℕ) → Box ι) n : Box ι) : Set (ι → ℝ))
          ((Box.Ioo : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))) ∧
      Tendsto (α := ℕ) (lower ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.lower) ∧
        Tendsto (α := ℕ) (upper ∘ (⇑J : (a : ℕ) → Box ι)) atTop (𝓝 I.upper)
Tactic: choose a b ha_anti hb_mono ha_mem hb_mem hab ha_tendsto hb_tendsto using
    fun i ↦ exists_seq_strictAnti_strictMono_tendsto (I.lower_lt_upper i)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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.distortion = J.distortion
have simp : 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: simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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
⊢ 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))
have 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)) :
      ℝ)
Tactic: congr 1 with i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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
have by_contra : ∀ (hr : ¬0 < r), False
Tactic: by_contra hr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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
⊢ False
have this : (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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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
⊢ False
have this₁ : I.upper i - I.lower i ≤ 0
Tactic: rw [← h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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 : ι
⊢ (↑((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)) :
      ℝ)
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
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
⊢ (↑((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)) :
      ℝ)
have hn0 : Ne (α := ℝ≥0) ((Real.nnabs : (a : ℝ) → ℝ≥0) r : ℝ≥0) (0 : ℝ≥0)
Tactic: have hn0 := (map_ne_zero Real.nnabs).2 this.ne'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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)
⊢ (↑((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)) :
      ℝ)
have 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)) :
    ℝ)
Tactic: simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right₀ hn0]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
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)
have 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)
Tactic: grw [distortion, ← Finset.le_sup (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: grw [distortion, ← Finset.le_sup (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
I : Box ι
i : ι
⊢ dist I.lower I.upper ≤ (↑I.distortion : ℝ) * (I.upper i - I.lower i)
have A : 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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.Basic (goal)
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
⊢ (↑I.distortion : ℝ) * (I.upper i - I.lower i) ≤ (↑c : ℝ) * (I.upper i - I.lower i)
have ha : 0 ≤ I.upper i - I.lower i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I_1 J I : Box ι
s : Set ι
i : ι
⊢ (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
have pos : i ∈ s → (I.lower i + I.upper i) / 2 < I.upper i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
⊢ (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
have neg : i ∉ s → I.lower i < (I.lower i + I.upper i) / 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
⊢ y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
have 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)
Tactic: simp only [splitCenterBox, mem_def, ← forall_and]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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)
have 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)
Tactic: refine forall_congr' fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ 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)
have 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)
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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 ↔ i ∈ s)
have 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
Tactic: simp only [hs, iff_true, iff_false, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
have 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
Tactic: simp only [hs, iff_true, iff_false, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint (↑(I.splitCenterBox s) : Set (ι → ℝ)) (↑(I.splitCenterBox t) : Set (ι → ℝ))
have rw : (↑(I.splitCenterBox s) : Set (ι → ℝ)) ⊓ (↑(I.splitCenterBox t) : Set (ι → ℝ)) ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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 (ι → ℝ))
⊢ Membership.mem (γ := Set (ι → ℝ)) ⊥ y
have apply : s = t
Tactic: apply h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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 (ι → ℝ))
⊢ s = t
have h₁ : ∀ (i : ι), i ∈ s ↔ i ∈ t
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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 : ι
⊢ i ∈ s ↔ i ∈ t
have 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
Tactic: rw [mem_coe, mem_splitCenterBox] at hs ht
Cleared hypotheses: hs, ht, i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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 : ι
⊢ i ∈ s ↔ i ∈ t
have h₁ : (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t
Tactic: rw [← hs.2, ← ht.2]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
⊢ i ∈ s ↔ i ∈ t
have h₂ : (I.lower i + I.upper i) / 2 < y i ↔ (I.lower i + I.upper i) / 2 < y i
Tactic: rw [← hs.2, ← ht.2]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
⊢ ⋃ (s : Set ι), (↑(I.splitCenterBox s) : Set (ι → ℝ)) = (↑I : Set (ι → ℝ))
have h : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) (⋃ (s : Set ι), (↑(I.splitCenterBox s) : Set (ι → ℝ))) x ↔ x ∈ (↑I : Set (ι → ℝ))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
have pos : i ∈ s → (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
Tactic: by_cases i ∈ s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
have neg : i ∉ s → (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
Tactic: by_cases i ∈ s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
have pos : I.upper i * 2 - (I.lower i + I.upper i) = I.upper i - I.lower i
Tactic: simp [field, splitCenterBox, *]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
Goal:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h : i ∉ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
have neg : I.lower i + I.upper i - I.lower i * 2 = I.upper i - I.lower i
Tactic: simp [field, splitCenterBox, *]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (goal)
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
⊢ p I
have by_contra : ∀ (hpI : ¬p I), False
Tactic: by_contra hpI