awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
We :
  Eq (α := ℝ≥0∞)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ i), m (ediam (t n)))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
We₁ :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
      Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (id t n).Nonempty), ⨅ (_ : ediam (id t n) ≤ r), m (ediam (id t n)))
        (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ id r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
We₂ :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
      Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
        (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
pos :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t) (htr : ∀ (n : ℕ), ediam (t n) ≤ r),
      Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
        (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞) (((mkMetric m : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
        ⨆ (_ : 0 < r),
          ⨅ (t : ℕ → Set X),
            ⨅ (_ : s ⊆ iUnion t),
              ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) :
      ℝ≥0∞)
have neg : ∀ r > 0,
  ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t) (htr : ¬∀ (n : ℕ), ediam (t n) ≤ r),
    Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
      (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
Tactic: classical
  -- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
  simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  refine
    surjective_id.iSup_congr id fun r =>
      iSup_congr_Prop Iff.rfl fun _ =>
        surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), ediam s ≤ ε → (μ : (a : Set X) → ℝ≥0∞) s ≤ m (ediam s)
⊢ μ ≤ mkMetric m
have rw : μ.toOuterMeasure ≤ OuterMeasure.mkMetric m
Tactic: rw [← toOuterMeasure_le, mkMetric_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (((mkMetric m : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l : ℝ≥0∞)
have haveI : ∀ (this : (n : β) → Encodable (ι n)),
  LE.le (α := ℝ≥0∞) (((mkMetric m : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l : ℝ≥0∞)
Tactic: haveI : ∀ n, Encodable (ι n) := fun n => Encodable.ofCountable _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
⊢ LE.le (α := ℝ≥0∞) (((mkMetric m : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l : ℝ≥0∞)
have simp : LE.le (α := ℝ≥0∞)
  (⨆ (r : ℝ≥0∞),
    ⨆ (_ : 0 < r),
      ⨅ (t : ℕ → Set X),
        ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
  (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l)
Tactic: simp only [mkMetric_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
    (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l)
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
  LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
    (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l)
Tactic: refine iSup₂_le fun ε hε => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
    (liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l)
have refine : ∀ (c : ℝ≥0∞) (hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c),
  ⨅ (t : ℕ → Set X),
      ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    c
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun c hc => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
⊢ ⨅ (t : ℕ → Set X),
      ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    c
have rcases : ∀ (n : β) (hn : ∑' (i : ι n), m (ediam (t n i)) < c) (hrn : r n < ε) (htn : ∀ (i : ι n), ediam (t n i) ≤ r n)
  (hstn : s ⊆ ⋃ (i : ι n), t n i),
  ⨅ (t : ℕ → Set X),
      ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    c
Tactic: rcases ((frequently_lt_of_liminf_lt (by isBoundedDefault) hc).and_eventually
        ((hr.eventually (gt_mem_nhds hε)).and (ht.and hst))).exists with
    ⟨n, hn, hrn, htn, hstn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ (i : ι n), t n i
u : ℕ → Set X := fun (j : ℕ) ↦ ⋃ (b : ι n), ⋃ (_ : Membership.mem (γ := Option (ι n)) (decode₂ (ι n) j) b), t n b
⊢ ⨅ (t : ℕ → Set X),
      ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    c
have refine : ⨅ (_ : ∀ (n : ℕ), ediam (u n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c
Tactic: refine iInf₂_le_of_le u (by rwa [iUnion_decode₂]) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ (i : ι n), t n i
u : ℕ → Set X := fun (j : ℕ) ↦ ⋃ (b : ι n), ⋃ (_ : Membership.mem (γ := Option (ι n)) (decode₂ (ι n) j) b), t n b
⊢ ⨅ (_ : ∀ (n : ℕ), ediam (u n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c
have refine_1 : ∀ (j : ℕ), ediam (u j) ≤ ε
Tactic: refine iInf_le_of_le (fun j => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ (i : ι n), t n i
u : ℕ → Set X := fun (j : ℕ) ↦ ⋃ (b : ι n), ⋃ (_ : Membership.mem (γ := Option (ι n)) (decode₂ (ι n) j) b), t n b
refine_1 : ∀ (j : ℕ), ediam (u j) ≤ ε
⊢ ⨅ (_ : ∀ (n : ℕ), ediam (u n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c
have refine_2 : ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c
Tactic: refine iInf_le_of_le (fun j => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ (i : ι n), t n i
u : ℕ → Set X := fun (j : ℕ) ↦ ⋃ (b : ι n), ⋃ (_ : Membership.mem (γ := Option (ι n)) (decode₂ (ι n) j) b), t n b
j : ℕ
⊢ ediam (u j) ≤ ε
have refine_1 : ⨆ (i : ι n), ⨆ (_ : Membership.mem (γ := Option (ι n)) (decode₂ (ι n) j) i), ediam (t n i) ≤ ε
Tactic: rw [ediam_iUnion_mem_option]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
⊢ Eq (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have by_contra! : ∀
  (H :
    Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (c : ℝ≥0),
    c ≠ 0 →
      ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
        HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ False
have rcases : ∀ (c : ℝ≥0) (hc0 : c > 0)
  (hc :
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) <
      ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s),
  False
Tactic: rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False
have suffices : ∀ (c : ℝ≥0),
  c ≠ 0 →
    ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: suffices ∀ c : ℝ≥0, c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s by
    rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
    exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
⊢ ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have refine : (fun (r : ℝ≥0∞) ↦ r ^ d₂) ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d₁
Tactic: refine le_iff'.1 (mkMetric_mono_smul ENNReal.coe_ne_top (mod_cast hc) ?_) s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
⊢ 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
have rw : ¬(c = 0 ∧ (d₂ - d₁)⁻¹ ≠ 0)
Tactic: rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero,
      NNReal.rpow_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
⊢ (fun (r : ℝ≥0∞) ↦ r ^ d₂) ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d₁
have this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
Tactic: have : 0 < ((c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) := by
    rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero,
      NNReal.rpow_eq_zero_iff]
    exact mt And.left hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
⊢ (fun (r : ℝ≥0∞) ↦ r ^ d₂) ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d₁
have h₁ : ∀ a ∈ Ico 0 ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹), a ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) a
Tactic: filter_upwards [Ico_mem_nhdsGE this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0∞
hr₀ : 0 ≤ r
hrc : r < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
⊢ r ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) r
have h₁ : ∀ (r : ℝ≥0) (hr₀ : 0 ≤ (↑r : ℝ≥0∞)) (hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹),
  (↑r : ℝ≥0∞) ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) (↑r : ℝ≥0∞)
Tactic: lift r to ℝ≥0 using ne_top_of_lt hrc
Cleared hypotheses: r, hr₀, hrc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
⊢ (↑r : ℝ≥0∞) ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) (↑r : ℝ≥0∞)
have h₁ : (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
Tactic: rw [Pi.smul_apply, smul_eq_mul,
    ← ENNReal.div_le_iff_le_mul (Or.inr ENNReal.coe_ne_top) (Or.inr <| mt ENNReal.coe_eq_zero.1 hc)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
⊢ (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
have h₁ : ∀ (hr₀ : 0 ≤ (↑0 : ℝ≥0∞)) (hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹),
  (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
Tactic: rcases eq_or_ne r 0 with (rfl | hr₀)
Cleared hypotheses: r, hr₀, hrc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ :
  ∀ (hr₀ : 0 ≤ (↑0 : ℝ≥0∞)) (hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹),
    (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
have h₂ : ∀ (hr₀ : r ≠ 0), (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
Tactic: rcases eq_or_ne r 0 with (rfl | hr₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ (↑0 : ℝ≥0∞)
hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
⊢ (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
have h₁ : ∀ (h₂ : 0 < d₂), (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
Tactic: rcases lt_or_ge 0 d₂ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ (↑0 : ℝ≥0∞)
hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ : ∀ (h₂ : 0 < d₂), (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
⊢ (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
have h₂ : ∀ (h₂ : d₂ ≤ 0), (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
Tactic: rcases lt_or_ge 0 d₂ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
⊢ (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
have this₁ : (↑r : ℝ≥0∞) ≠ 0
Tactic: have : (r : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using hr₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this_1 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
this : (↑r : ℝ≥0∞) ≠ 0
⊢ (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
have h₁ : (↑r : ℝ≥0∞) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
Tactic: rw [← ENNReal.rpow_sub _ _ this ENNReal.coe_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this_1 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
this : (↑r : ℝ≥0∞) ≠ 0
⊢ (↑r : ℝ≥0∞) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
have h₁ : ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
Tactic: refine (ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_