-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem setFinite_index {s : Set (ι → ℝ)} (hs₁ : NullMeasurableSet s) (hs₂ : volume s ≠ ⊤) :
    Set.Finite {ν : ι → ℤ | ↑(box n ν) ⊆ s}

Proof state:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet ((fun ν => ↑(box n ν) ∩ s) ν) volume

Tactic:
refine NullMeasurableSet.inter ?_ hs₁

Result:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet (↑(box n ν)) volume

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ 0 < 1 / ↑n ^ card ι

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, (fun ν => ↑(box n ν) ∩ s) i) ≠ ⊤

Tactic:
exact lt_top_iff_ne_top.mp <| measure_lt_top_of_subset
  (by simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]) hs₂

Result:
no goals

Proof state:
case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Tactic:
rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ ⋃ i, (fun ν => ↑(box n ν) ∩ s) i ⊆ s

Tactic:
simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet (↑(box n ν)) volume

Tactic:
exact (box n ν).measurableSet_coe.nullMeasurableSet

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ {ν | ↑(box n ν) ⊆ s}.Finite

Tactic:
refine (Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι)
  (by norm_num) (As := fun ν : ι → ℤ ↦ (box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
    (fun _ hν ↦ ?_)

Result:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet ((fun ν => ↑(box n ν) ∩ s) ν) volume

case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν => ↑(box n ν) ∩ s) x✝¹ x✝

case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, (fun ν => ↑(box n ν) ∩ s) i) ≠ ⊤

case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Proof state:
case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν => ↑(box n ν) ∩ s) x✝¹ x✝

Tactic:
exact ((Disjoint.inter_right _ (disjoint.mp h)).inter_left _ ).aedisjoint

Result:
no goals