awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
hKd : (↑K : ℝ≥0∞) ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)
⊢ ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d
have inr : ediam (f ⁻¹' t n) ^ d ≤ (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d
Tactic: simp only [nonempty_of_nonempty_preimage hft, ciSup_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
hKd : (↑K : ℝ≥0∞) ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)
⊢ ediam (f ⁻¹' t n) ^ d ≤ (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d
have inr : ediam (f ⁻¹' t n) ^ d ≤ ((↑K : ℝ≥0∞) * ediam (t n)) ^ d
Tactic: rw [← ENNReal.mul_rpow_of_nonneg _ _ hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞)
  ((((OuterMeasure.comap f : (a : OuterMeasure Y) → OuterMeasure X) (OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d) :
          OuterMeasure X) :
        (a : Set X) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  (((OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [hausdorffMeasure, ← OuterMeasure.coe_mkMetric, ← OuterMeasure.comap_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ Eq (α := ℝ≥0∞)
    ((((OuterMeasure.comap f : (a : OuterMeasure Y) → OuterMeasure X) (OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d) :
            OuterMeasure X) :
          (a : Set X) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have rw : 0 ≤ d → Monotone (β := ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d
Tactic: rw [OuterMeasure.isometry_comap_mkMetric _ hf (hd.imp_left _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
  (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [← hf.hausdorffMeasure_image hd, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
rw :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
  (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [← hf.hausdorffMeasure_image hd, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
⊢ Eq (α := Measure Y) (Measure.map f μH[d]) (Measure.restrict μH[d] (range f))
have h : ∀ (s : Set Y) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.map f μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map f μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply hf.continuous.measurable hs, Measure.restrict_apply hs,
    hf.hausdorffMeasure_preimage hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [map_apply hf.continuous.measurable hs, Measure.restrict_apply hs,
    hf.hausdorffMeasure_preimage hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
  (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [map_apply hf.continuous.measurable hs, Measure.restrict_apply hs,
    hf.hausdorffMeasure_preimage hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
s : Set Y
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ((⇑e : (a : X) → Y) ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ((⇑e.symm : (a : Y) → X) '' s) : ℝ≥0∞)
  (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← e.image_symm, e.symm.hausdorffMeasure_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
s : Set Y
rw :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ((⇑e.symm : (a : Y) → X) '' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ((⇑e : (a : X) → Y) ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
  (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← e.image_symm, e.symm.hausdorffMeasure_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
⊢ Eq.{u_3 + 1} (α := Measure Y) (Measure.map.{u_2, u_3} (α := X) (⇑e : (a : X) → Y) μH[d]) μH[d]
have rw : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] (range.{u_3, u_2 + 1} (ι := X) (⇑e : (a : X) → Y))) μH[d]
Tactic: rw [e.isometry.map_hausdorffMeasure (Or.inr e.surjective), e.surjective.range_eq, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
rw : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] (range.{u_3, u_2 + 1} (ι := X) (⇑e : (a : X) → Y))) μH[d]
⊢ Eq.{u_3 + 1} (α := Measure Y) (Measure.map.{u_2, u_3} (α := X) (⇑e : (a : X) → Y) μH[d]) μH[d]
have rw₁ : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] univ) μH[d]
Tactic: rw [e.isometry.map_hausdorffMeasure (Or.inr e.surjective), e.surjective.range_eq, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
rw : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] (range.{u_3, u_2 + 1} (ι := X) (⇑e : (a : X) → Y))) μH[d]
rw₁ : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] univ) μH[d]
⊢ Eq.{u_3 + 1} (α := Measure Y) (Measure.map.{u_2, u_3} (α := X) (⇑e : (a : X) → Y) μH[d]) μH[d]
have rw₂ : Eq.{u_3 + 1} (α := Measure Y) μH[d] μH[d]
Tactic: rw [e.isometry.map_hausdorffMeasure (Or.inr e.surjective), e.surjective.range_eq, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
⊢ Eq.{u_4 + 1} (α := Measure (ι → ℝ)) (μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))
have refine : ∀ (s : (i : ι) → Set ℝ),
  (∀ (i : ι), Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) (s i)) →
    Eq (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞)
      (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (pi_eq_generateFrom (fun _ => Real.borel_eq_generateFrom_Ioo_rat.symm)
    (fun _ => Real.isPiSystem_Ioo_rat) (fun _ => Real.finiteSpanningSetsInIooRat _) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
⊢ ∀ (s : (i : ι) → Set ℝ),
    (∀ (i : ι),
        Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) (s i)) →
      Eq (α := ℝ≥0∞)
        (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
            (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
          ℝ≥0∞)
        (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp : ∀ (s : (i : ι) → Set ℝ),
  (∀ (i : ι), ∃ (i_1 : ℚ) (i_2 : ℚ) (_ : i_1 < i_2), s i = Ioo (↑i_1 : ℝ) (↑i_2 : ℝ)) →
    Eq (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x) : ℝ≥0∞)
Tactic: simp only [mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), ∃ (i_1 : ℚ) (i_2 : ℚ) (_ : i_1 < i_2), s i = Ioo (↑i_1 : ℝ) (↑i_2 : ℝ)
⊢ Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x) : ℝ≥0∞)
have choose : ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), ∃ (_ : a i < b i), s i = Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)),
  Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x) : ℝ≥0∞)
Tactic: choose a b H using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
s : (i : ι) → Set ℝ
a b : (i : ι) → ℚ
H : ∀ (i : ι), ∃ (_ : a i < b i), s i = Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)
⊢ Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x) : ℝ≥0∞)
have obtain : ∀
  (H :
    ∀ (i : ι),
      ∃ (_ : a i < b i),
        Eq (α := Set ℝ) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) i) (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ))),
  Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
Tactic: obtain rfl : s = fun i => Ioo (α := ℝ) (a i) (b i) := funext fun i => (H i).2
Cleared hypotheses: s, H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H :
  ∀ (i : ι),
    ∃ (_ : a i < b i),
      Eq (α := Set ℝ) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) i) (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ))
⊢ Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have H₁ : ∀ (i : ι), a i < b i
Tactic: replace H := fun i => (H i).1
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
⊢ Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞)
  (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
  (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
    ℝ≥0∞)
Tactic: apply le_antisymm _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
apply :
  LE.le (α := ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have apply₁ : LE.le (α := ℝ≥0∞)
  (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
    ℝ≥0∞)
  (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
Tactic: apply le_antisymm _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
⊢ LE.le.{u_4} (α := Measure (ι → ℝ)) volume μH[(↑(Fintype.card ι) : ℝ)]
have refine : ∀ (s : Set (ι → ℝ)),
  ediam s ≤ ∞ →
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s ≤ HPow.hPow (β := ℝ) (ediam s) (↑(Fintype.card ι) : ℝ)
Tactic: refine le_hausdorffMeasure _ _ ∞ ENNReal.coe_lt_top fun s _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
s : Set (ι → ℝ)
h : ediam s ≤ ∞
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s ≤ HPow.hPow (β := ℝ) (ediam s) (↑(Fintype.card ι) : ℝ)
have rw : ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s ≤ ediam s ^ Fintype.card ι
Tactic: rw [ENNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
⊢ LE.le (α := ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
have Hle : LE.le.{u_4} (α := Measure (ι → ℝ)) volume μH[(↑(Fintype.card ι) : ℝ)]
Tactic: have Hle : volume ≤ (μH[Fintype.card ι] : Measure (ι → ℝ)) := by
      refine le_hausdorffMeasure _ _ ∞ ENNReal.coe_lt_top fun s _ => ?_
      rw [ENNReal.rpow_natCast]
      exact Real.volume_pi_le_diam_pow s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
Hle : LE.le.{u_4} (α := Measure (ι → ℝ)) volume μH[(↑(Fintype.card ι) : ℝ)]
⊢ LE.le (α := ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
    ℝ≥0∞)
  (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
    ℝ≥0∞)
Tactic: rw [← volume_pi_pi fun i => Ioo (a i : ℝ) (b i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
⊢ LE.le (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
Tactic: have I : ∀ i, 0 ≤ (b i : ℝ) - a i := fun i => by
    simpa only [sub_nonneg, Rat.cast_le] using (H i).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
⊢ LE.le (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
Tactic: have A : Tendsto (fun n : ℕ => 1 / (n : ℝ≥0∞)) atTop (𝓝 0) := by
    simp only [one_div, ENNReal.tendsto_inv_nat_nhds_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
have refine : ∀ (n : ℕ) (hn : n ≥ 1) (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
Tactic: refine eventually_atTop.2 ⟨1, fun n hn => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
n : ℕ
hn : n ≥ 1
f : γ n
⊢ ediam (t n f) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
have refine : ∀ (b_1 : ι),
  ediam
      (Icc ((↑(a b_1) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f b_1) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a b_1) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f b_1) : ℕ) : ℝ) 1 / (↑n : ℝ))) ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
Tactic: refine ediam_pi_le_of_le fun b => ?_