awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J = x
⊢ J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x
have rcases : ∀ (hJ : J ∈ π.boxes),
  J ∈ π.boxes ∧ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π.tag J)
Tactic: rcases hJ with ⟨hJ, rfl⟩
Cleared hypotheses: x, hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι)
have J : #({J ∈ π.boxes | π.tag J = x}) ≤
  #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})
Tactic: calc
    #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩
    _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card ι)
have J : #({J ∈ π.boxes | π.tag J = x}) ≤
  #({J ∈ π.boxes | Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) x})
Tactic: classical
  calc
    #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩
    _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I J_1 : Box ι
π π₁_1 π₂_1 : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
    (if J ∈ π₁.boxes then π₁.tag J else π₂.tag J)
have pos : J ∈ π₁.boxes → Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₁.tag J)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I J_1 : Box ι
π π₁_1 π₂_1 : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
pos :
  J ∈ π₁.boxes → Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₁.tag J)
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ))
    (if J ∈ π₁.boxes then π₁.tag J else π₂.tag J)
have neg : J ∉ π₁.boxes → Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) (π₂.tag J)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsSubordinate r
have refine_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
  (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
Tactic: refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
      closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
⊢ (π₁.disjUnion π₂ h).IsSubordinate r
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
  (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
Tactic: refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
have refine_1 : (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₁.tag J) (↑(r (π₁.tag J)) : ℝ)
Tactic: rw [disjUnion_tag_of_mem_left _ hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
have refine_2 : (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆ closedBall (π₂.tag J) (↑(r (π₂.tag J)) : ℝ)
Tactic: rw [disjUnion_tag_of_mem_right _ hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsSubordinate r
have refine_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
  (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
Tactic: classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → (↑(Set.Ioi 0) : Type)
inst : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
      closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
⊢ (π₁.disjUnion π₂ h).IsSubordinate r
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
  (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    closedBall ((π₁.disjUnion π₂ h).tag J) (↑(r ((π₁.disjUnion π₂ h).tag J)) : ℝ)
Tactic: classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsHenstock
have refine_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)
Tactic: refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((π₁.disjUnion π₂ h).tag J)
⊢ (π₁.disjUnion π₂ h).IsHenstock
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)
Tactic: refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)
have refine_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₁.tag J)
Tactic: rw [disjUnion_tag_of_mem_left _ hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ_1 : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)
have refine_2 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) (π₂.tag J)
Tactic: rw [disjUnion_tag_of_mem_right _ hJ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsHenstock
have refine_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)
Tactic: classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Partition.Tagged (goal)
Goal:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₁.boxes),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ))
      ((π₁.disjUnion π₂ h).tag J)
⊢ (π₁.disjUnion π₂ h).IsHenstock
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ π₁.disjUnion π₂ h) (hJ : J ∈ π₂.boxes),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((π₁.disjUnion π₂ h).tag J)
Tactic: classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
have have : ∀ (this : Fintype ι), ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
have obtain : ∀ (R : ℝ) (hR₁ : 0 < R) (hR₂ : s ⊆ Metric.ball 0 R), ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
Tactic: obtain ⟨R, hR₁, hR₂⟩ := IsBounded.subset_ball_lt h 0 0
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
have hC : 0 < ⌈R⌉₊
Tactic: have hC := Nat.ceil_pos.mpr hR₁
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
have refine : Metric.ball 0 R ≤ (↑I : Set (ι → ℝ))
Tactic: refine ⟨I, ⟨fun _ ↦ - C, fun _ ↦ C, fun i ↦ (Int.cast_neg_natCast C).symm, fun _ ↦ rfl⟩,
    le_trans hR₂ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
⊢ Metric.ball 0 R ≤ (↑I : Set (ι → ℝ))
have suffices : Metric.ball 0 (↑C : ℝ) ≤ (↑I : Set (ι → ℝ))
Tactic: suffices Metric.ball (0 : ι → ℝ) C ≤ I from
    le_trans (Metric.ball_subset_ball (Nat.le_ceil R)) this
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) (Metric.ball 0 (↑C : ℝ)) x
⊢ x ∈ (↑I : Set (ι → ℝ))
have hx₁ : ∀ (i : ι), -(↑⌈R⌉₊ : ℝ) < x i ∧ x i < (↑⌈R⌉₊ : ℝ)
Tactic: simp_rw [C, mem_ball_zero_iff, pi_norm_lt_iff (Nat.cast_pos.mpr hC),
    Real.norm_eq_abs, abs_lt] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔
    ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
have simp_rw : (∀ (i : ι), x i ∈ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) ↔
  ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
Tactic: simp_rw [Box.mem_def, box, Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
simp_rw :
  (∀ (i : ι), x i ∈ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) ↔
    ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
⊢ x ∈ box n ν ↔
    ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
have simp_rw₁ : (∀ (i : ι), x i ∈ Set.Ioc (HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ)) (HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ))) ↔
  ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
Tactic: simp_rw [Box.mem_def, box, Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔ ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
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:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ x ∈ box n ν ↔ ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
have simp_rw : (∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)) ↔
  ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
Tactic: simp_rw [mem_box_iff, ← _root_.le_div_iff₀' h, ← div_lt_iff₀' h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
simp_rw :
  (∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)) ↔
    ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
⊢ x ∈ box n ν ↔ ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
have simp_rw₁ : (∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)) ↔
  ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
Tactic: simp_rw [mem_box_iff, ← _root_.le_div_iff₀' h, ← div_lt_iff₀' h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
⊢ Function.Injective (β := ι → ℝ) fun (ν : ι → ℤ) ↦ tag n ν
have refine : ∀ (x x_1 : ι → ℤ) (h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1))
  (i : ι), x i = x_1 i
Tactic: refine fun _ _ h ↦ funext_iff.mpr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x x_1 : ι → ℤ
h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1)
i : ι
⊢ x i = x_1 i
have this : Eq (α := ℝ) ((fun (x : ι → ℝ) ↦ x i) ((fun (ν : ι → ℤ) ↦ tag n ν) x))
  ((fun (x : ι → ℝ) ↦ x i) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1))
Tactic: have := congr_arg (fun x ↦ x i) h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
⊢ tag n ν ∈ box n ν
have refine : ∀ (x : ι),
  HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < tag n ν x ∧ tag n ν x ≤ HAdd.hAdd (α := ℝ) (↑(ν x) : ℝ) 1 / (↑n : ℝ)
Tactic: refine mem_box_iff.mpr fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
⊢ HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < tag n ν x ∧ tag n ν x ≤ HAdd.hAdd (α := ℝ) (↑(ν x) : ℝ) 1 / (↑n : ℝ)
have rw : HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ∧
  HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: rw [tag, add_div]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
⊢ HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ∧
    HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
      HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 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:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
simp_rw :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw₁ : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
  ∀ (x_1 : ι), index n x x_1 = ν x_1
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
simp_rw :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
simp_rw₁ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), index n x x_1 = ν x_1
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw₂ : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
  ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ - 1 = ν x_1
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
simp_rw :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
simp_rw₁ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), index n x x_1 = ν x_1
simp_rw₂ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ - 1 = ν x_1
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw₃ : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
  ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ = ν x_1 + 1
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
simp_rw :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
simp_rw₁ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), index n x x_1 = ν x_1
simp_rw₂ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ - 1 = ν x_1
simp_rw₃ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ = ν x_1 + 1
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw₄ : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
  ∀ (x_1 : ι), HSub.hSub (α := ℝ) (↑(ν x_1 + 1) : ℝ) 1 < (↑n : ℝ) * x x_1 ∧ (↑n : ℝ) * x x_1 ≤ (↑(ν x_1 + 1) : ℝ)
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]