awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
rw :
  Membership.mem (γ := TaggedPrepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun (I : Box ι) ↦
          if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
            tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
          else ⋯.choose (p := Membership.mem B),
        tag_mem_Icc := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
rw₁ :
  Membership.mem (γ := Prepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯,
        pairwiseDisjoint := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw₂ : Membership.mem (γ := Finset (Box ι)) (Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) I ↔
  ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: classical
  rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
rw :
  Membership.mem (γ := TaggedPrepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun (I : Box ι) ↦
          if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
            tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
          else ⋯.choose (p := Membership.mem B),
        tag_mem_Icc := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
rw₁ :
  Membership.mem (γ := Prepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯,
        pairwiseDisjoint := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
rw₂ :
  Membership.mem (γ := Finset (Box ι)) (Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw₃ : (∃ a ∈ admissibleIndex n B, box n a = I) ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: classical
  rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then
      tag n (hI.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1))
    else ⋯.choose (p := Membership.mem B)) =
    tag n ν
have h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
Tactic: have h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν' := ⟨ν, hν, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then
      tag n (hI.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1))
    else ⋯.choose (p := Membership.mem B)) =
    tag n ν
have rw : box n (h.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1)) = box n ν
Tactic: rw [dif_pos h, (tag_injective n).eq_iff, ← (box_injective n).eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
hI : I ∈ (prepartition n B).boxes
⊢ box n (index n ((prepartition n B).tag I)) = I
have obtain : ∀ (ν : ι → ℤ) (hν : ν ∈ admissibleIndex n B) (hI : box n ν ∈ (prepartition n B).boxes),
  box n (index n ((prepartition n B).tag (box n ν))) = box n ν
Tactic: obtain ⟨ν, hν, rfl⟩ := mem_prepartition_boxes_iff.mp hI
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ (prepartition n B).boxes
⊢ box n (index n ((prepartition n B).tag (box n ν))) = box n ν
have rw : box n (index n (tag n ν)) = box n ν
Tactic: rw [prepartition_tag n hν, index_tag]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ (prepartition n B).boxes
rw : box n (index n (tag n ν)) = box n ν
⊢ box n (index n ((prepartition n B).tag (box n ν))) = box n ν
have rw₁ : box n ν = box n ν
Tactic: rw [prepartition_tag n hν, index_tag]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B J : Box ι
hI : J ∈ prepartition n B
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((prepartition n B).tag J)
have obtain : ∀ (ν : ι → ℤ) (hν : ν ∈ admissibleIndex n B) (hI : box n ν ∈ prepartition n B),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
    ((prepartition n B).tag (box n ν))
Tactic: obtain ⟨ν, hν, rfl⟩ := mem_prepartition_iff.mp hI
Cleared hypotheses: J, hI
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
    ((prepartition n B).tag (box n ν))
have rw : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)
Tactic: rw [prepartition_tag n hν]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
J : Box ι
hI : J ∈ prepartition n B
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    Metric.closedBall ((prepartition n B).tag J)
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag J)) :
        ℝ)
have obtain : ∀ (ν : ι → ℤ) (hν : ν ∈ admissibleIndex n B) (hI : box n ν ∈ prepartition n B),
  (Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν))
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag (box n ν))) :
        ℝ)
Tactic: obtain ⟨ν, hν, rfl⟩ := mem_prepartition_iff.mp hI
Cleared hypotheses: J, hI
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν))
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag (box n ν))) :
        ℝ)
have refine_1 : ∀ (x : ι → ℝ) (h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
    ((prepartition n B).tag (box n ν))
Tactic: refine fun _ h ↦ le_trans (Metric.dist_le_diam_of_mem (Box.isBounded_Icc _) h ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
refine_1 :
  ∀ (x : ι → ℝ)
    (h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
      ((prepartition n B).tag (box n ν))
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν))
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag (box n ν))) :
        ℝ)
have refine_2 : ∀ (x : ι → ℝ) (h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x),
  Metric.diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν)) ≤
    (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
          ((prepartition n B).tag (box n ν))) :
      ℝ)
Tactic: refine fun _ h ↦ le_trans (Metric.dist_le_diam_of_mem (Box.isBounded_Icc _) h ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
    ((prepartition n B).tag (box n ν))
have refine_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)
Tactic: rw [prepartition_tag n hν]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have h : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 = (↑((↑n : ℤ) * a + 1) : ℝ)
have norm_cast : (↑n : ℤ) * a + 1 = (↑n : ℤ) * a + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₄ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a < ⌈(↑n : ℝ) * x⌉
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
rw₄ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a < ⌈(↑n : ℝ) * x⌉
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₅ : (↑a : ℝ) < x ↔ (↑((↑n : ℤ) * a) : ℝ) < (↑n : ℝ) * x
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
rw₄ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a < ⌈(↑n : ℝ) * x⌉
rw₅ : (↑a : ℝ) < x ↔ (↑((↑n : ℤ) * a) : ℝ) < (↑n : ℝ) * x
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₆ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
rw₄ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a < ⌈(↑n : ℝ) * x⌉
rw₅ : (↑a : ℝ) < x ↔ (↑((↑n : ℤ) * a) : ℝ) < (↑n : ℝ) * x
rw₆ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₇ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
rw₄ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a < ⌈(↑n : ℝ) * x⌉
rw₅ : (↑a : ℝ) < x ↔ (↑((↑n : ℤ) * a) : ℝ) < (↑n : ℝ) * x
rw₆ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
rw₇ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)
have rw₈ : (↑a : ℝ) < x ↔ (↑a : ℝ) < x
Tactic: rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have h : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) = (↑((↑n : ℤ) * a) : ℝ)
have norm_cast : (↑n : ℤ) * a = (↑n : ℤ) * a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₂ : x ≤ (↑a : ℝ) ↔ LE.le (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑((↑n : ℤ) * a) : ℝ)
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
rw₂ : x ≤ (↑a : ℝ) ↔ LE.le (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑((↑n : ℤ) * a) : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₃ : x ≤ (↑a : ℝ) ↔ ⌈(↑n : ℝ) * x⌉ ≤ (↑n : ℤ) * a
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
rw₂ : x ≤ (↑a : ℝ) ↔ LE.le (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑((↑n : ℤ) * a) : ℝ)
rw₃ : x ≤ (↑a : ℝ) ↔ ⌈(↑n : ℝ) * x⌉ ≤ (↑n : ℤ) * a
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₄ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ (↑((↑n : ℤ) * a) : ℝ)
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
rw₂ : x ≤ (↑a : ℝ) ↔ LE.le (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑((↑n : ℤ) * a) : ℝ)
rw₃ : x ≤ (↑a : ℝ) ↔ ⌈(↑n : ℝ) * x⌉ ≤ (↑n : ℤ) * a
rw₄ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ (↑((↑n : ℤ) * a) : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₅ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ)
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
rw₂ : x ≤ (↑a : ℝ) ↔ LE.le (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑((↑n : ℤ) * a) : ℝ)
rw₃ : x ≤ (↑a : ℝ) ↔ ⌈(↑n : ℝ) * x⌉ ≤ (↑n : ℤ) * a
rw₄ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ (↑((↑n : ℤ) * a) : ℝ)
rw₅ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₆ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
Tactic: rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]