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
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
htop : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
r n i j : ℕ
hj : i < j
A : LT.lt (α := ℝ≥0∞) (↑(2 * j + r) : ℝ≥0∞)⁻¹ (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
x : X
hx : x ∈ S (2 * i + 1 + r)
y : X
hy : y ∈ s \ S (2 * j + r)
this : infEDist y t < (↑(2 * j + r) : ℝ≥0∞)⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r) : ℝ≥0∞)⁻¹
hxz : (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ ≤ edist x z
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x y + edist y z
have neg : HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x z
Tactic: refine le_trans ?_ (edist_triangle _ _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
htop : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
r n i j : ℕ
hj : i < j
A : LT.lt (α := ℝ≥0∞) (↑(2 * j + r) : ℝ≥0∞)⁻¹ (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
x : X
hx : x ∈ S (2 * i + 1 + r)
y : X
hy : y ∈ s \ S (2 * j + r)
this : infEDist y t < (↑(2 * j + r) : ℝ≥0∞)⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r) : ℝ≥0∞)⁻¹
hxz : (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ ≤ edist x z
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x z
have neg : HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + (↑(2 * j + r) : ℝ≥0∞)⁻¹ =
  (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
Tactic: refine (add_le_add le_rfl hyz.le).trans (Eq.trans_le ?_ hxz)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
htop : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
r n i j : ℕ
hj : i < j
A : LT.lt (α := ℝ≥0∞) (↑(2 * j + r) : ℝ≥0∞)⁻¹ (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
x : X
hx : x ∈ S (2 * i + 1 + r)
y : X
hy : y ∈ s \ S (2 * j + r)
this : infEDist y t < (↑(2 * j + r) : ℝ≥0∞)⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r) : ℝ≥0∞)⁻¹
hxz : (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ ≤ edist x z
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + (↑(2 * j + r) : ℝ≥0∞)⁻¹ =
    (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
have neg : Eq (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
Tactic: rw [tsub_add_cancel_of_le A.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
hm : μ.IsMetric
⊢ inst_1 ≤ μ.caratheodory
have rw : borel X ≤ μ.caratheodory
Tactic: rw [BorelSpace.measurable_eq (α := X)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ ((pre m r : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((mkMetric' m : (a : Set X) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (x : (↑(Ioi 0) : Type)) ↦ ((pre m (↑x : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) atBot
  (𝓝 ((mkMetric' m : (a : Set X) → ℝ≥0∞) s) : Filter ℝ≥0∞)
Tactic: rw [← tendsto_comp_coe_Ioi_atBot]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (β := ℝ≥0∞) (fun (x : (↑(Ioi 0) : Type)) ↦ ((pre m (↑x : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) atBot
    (𝓝 ((mkMetric' m : (a : Set X) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have simp : Tendsto (β := ℝ≥0∞) (fun (x : (↑(Ioi 0) : Type)) ↦ (pre m (↑x : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s) atBot
  (𝓝 (⨆ (i : { i : ℝ≥0∞ // i > 0 }), (pre m (↑i : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s))
Tactic: simp only [mkMetric', OuterMeasure.iSup_apply, iSup_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((pre m (↑n : ℝ≥0∞)⁻¹ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((mkMetric' m : (a : Set X) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have refine : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)⁻¹) atTop (𝓟 (Ioi 0))
Tactic: refine (tendsto_pre m s).comp (tendsto_inf.2 ⟨ENNReal.tendsto_inv_nat_nhds_zero, ?_⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)⁻¹) atTop (𝓟 (Ioi 0))
have refine : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) (↑n : ℝ≥0∞)⁻¹
Tactic: refine tendsto_principal.2 (Eventually.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
⊢ mkMetric' m = ⨆ (n : ℕ), pre m (↑n : ℝ≥0∞)⁻¹
have h : ∀ (s : Set X),
  Eq (α := ℝ≥0∞) ((mkMetric' m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (n : ℕ), pre m (↑n : ℝ≥0∞)⁻¹ : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Eq (α := ℝ≥0∞) ((mkMetric' m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (n : ℕ), pre m (↑n : ℝ≥0∞)⁻¹ : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((mkMetric' m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
  (⨆ (i : ℕ), (pre m (↑i : ℝ≥0∞)⁻¹ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [iSup_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 : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
⊢ (pre m r).trim = pre m r
have refine : ∀ (s : Set X) (hs : ediam s ≤ r), ((pre m r).trim : (a : Set X) → ℝ≥0∞) s ≤ m s
Tactic: refine le_antisymm (le_pre.2 fun s hs => ?_) (le_trim _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ((pre m r).trim : (a : Set X) → ℝ≥0∞) s ≤ m s
have rw : ⨅ (t : Set X), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r : (a : Set X) → ℝ≥0∞) t ≤ m s
Tactic: rw [trim_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ⨅ (t : Set X), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r : (a : Set X) → ℝ≥0∞) t ≤ m s
have refine : ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ r
Tactic: refine iInf_le_of_le (closure s) <| iInf_le_of_le subset_closure <|
    iInf_le_of_le measurableSet_closure ((pre_le ?_).trans_eq (hcl _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
⊢ (mkMetric' m : (a : Set X) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric' m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric' m : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
have refine : EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (r : ℝ≥0∞) ↦ (mkMetric'.pre m r : (a : Set X) → ℝ≥0∞) (s ∪ t)) fun (x : ℝ≥0∞) ↦
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine tendsto_nhds_unique_of_eventuallyEq
    (mkMetric'.tendsto_pre _ _) ((mkMetric'.tendsto_pre _ _).add (mkMetric'.tendsto_pre _ _)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (r : ℝ≥0∞) ↦ (mkMetric'.pre m r : (a : Set X) → ℝ≥0∞) (s ∪ t)) fun (x : ℝ≥0∞) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
have r0₁ : 0 < r
Tactic: rw [← pos_iff_ne_zero] at r0
Cleared hypotheses: r0, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (r : ℝ≥0∞) ↦ (mkMetric'.pre m r : (a : Set X) → ℝ≥0∞) (s ∪ t)) fun (x : ℝ≥0∞) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
have h : ∀ a ∈ Ioo 0 r,
  (mkMetric'.pre m a : (a : Set X) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m a : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m a : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: filter_upwards [Ioo_mem_nhdsGT r0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
⊢ (mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
have h : ∀ (u : Set X),
  (s ∩ u).Nonempty →
    (t ∩ u).Nonempty → extend (P := fun (s : Set X) ↦ ediam s ≤ ε) (fun (s : Set X) (x : ediam s ≤ ε) ↦ m s) u = ∞
Tactic: refine boundedBy_union_of_top_of_nonempty_inter ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
u : Set X
x : X
hxs : x ∈ s
hxu : x ∈ u
y : X
hyt : y ∈ t
hyu : y ∈ u
⊢ extend (P := fun (s : Set X) ↦ ediam s ≤ ε) (fun (s : Set X) (x : ediam s ≤ ε) ↦ m s) u = ∞
have this : ε < ediam u
Tactic: have : ε < ediam u := εr.trans_le ((hr x hxs y hyt).trans <| edist_le_ediam_of_mem hxu hyu)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
have rcases : ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
  (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}),
  mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
Tactic: rcases (mem_nhdsGE_iff_exists_Ico_subset' zero_lt_one).1 hle with ⟨r, hr0, hr⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
have refine : ∀ (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r),
  Membership.mem (γ := Set ℝ≥0∞)
    {x : ℝ≥0∞ |
      (fun (x : ℝ≥0∞) ↦
          LE.le (α := ℝ≥0∞)
            ((fun (r : ℝ≥0∞) ↦
                (((mkMetric'.pre (fun (s : Set X) ↦ m₁ (ediam s)) r : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
              x)
            ((fun (b : ℝ≥0∞) ↦
                HMul.hMul (β := ℝ≥0∞) c
                  (((mkMetric'.pre (fun (s : Set X) ↦ m₂ (ediam s)) b : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
              x))
        x}
    r'
Tactic: refine fun s =>
    le_of_tendsto_of_tendsto (mkMetric'.tendsto_pre _ s)
      (ENNReal.Tendsto.const_mul (mkMetric'.tendsto_pre _ s) (Or.inr hc))
      (mem_of_superset (Ioo_mem_nhdsGT hr0) fun r' hr' => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ Membership.mem (γ := Set ℝ≥0∞)
    {x : ℝ≥0∞ |
      (fun (x : ℝ≥0∞) ↦
          LE.le (α := ℝ≥0∞)
            ((fun (r : ℝ≥0∞) ↦
                (((mkMetric'.pre (fun (s : Set X) ↦ m₁ (ediam s)) r : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
              x)
            ((fun (b : ℝ≥0∞) ↦
                HMul.hMul (β := ℝ≥0∞) c
                  (((mkMetric'.pre (fun (s : Set X) ↦ m₂ (ediam s)) b : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
              x))
        x}
    r'
have simp : ((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) :
        OuterMeasure X) :
      (a : Set X) → ℝ≥0∞)
    s ≤
  HMul.hMul (β := ℝ≥0∞) c
    (((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s)) :
            OuterMeasure X) :
          (a : Set X) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: simp only [mem_setOf_eq, mkMetric'.pre]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ ((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) :
          OuterMeasure X) :
        (a : Set X) → ℝ≥0∞)
      s ≤
    HMul.hMul (β := ℝ≥0∞) c
      (((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s)) :
              OuterMeasure X) :
            (a : Set X) → ℝ≥0∞)
          s :
        ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  (((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) :
          OuterMeasure X) :
        (a : Set X) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((boundedBy
          (HSMul.hSMul (β := Set X → ℝ≥0∞) c
            (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s))) :
        (a : Set X) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: rw [← smul_eq_mul, ← smul_apply, smul_boundedBy hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ LE.le (α := ℝ≥0∞)
    (((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) :
            OuterMeasure X) :
          (a : Set X) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((boundedBy
            (HSMul.hSMul (β := Set X → ℝ≥0∞) c
              (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s))) :
          (a : Set X) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have refine : ∀ (t : Set X),
  extend (P := fun (s : Set X) ↦ ediam s ≤ r') (fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) t ≤
    HSMul.hSMul (β := Set X → ℝ≥0∞) c
      (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s)) t
Tactic: refine le_boundedBy.2 (fun t => (boundedBy_le _).trans ?_) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
t : Set X
⊢ extend (P := fun (s : Set X) ↦ ediam s ≤ r') (fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) t ≤
    HSMul.hSMul (β := Set X → ℝ≥0∞) c
      (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s)) t
have simp : (if ediam t ≤ r' then m₁ (ediam t) else ∞) ≤ c * if ediam t ≤ r' then m₂ (ediam t) else ∞
Tactic: simp only [smul_eq_mul, Pi.smul_apply, extend, iInf_eq_if]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
t : Set X
⊢ (if ediam t ≤ r' then m₁ (ediam t) else ∞) ≤ c * if ediam t ≤ r' then m₂ (ediam t) else ∞
have pos : ∀ (ht : ediam t ≤ r'), m₁ (ediam t) ≤ c * m₂ (ediam t)
Tactic: split_ifs with ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r
hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
t : Set X
pos : ∀ (ht : ediam t ≤ r'), m₁ (ediam t) ≤ c * m₂ (ediam t)
⊢ (if ediam t ≤ r' then m₁ (ediam t) else ∞) ≤ c * if ediam t ≤ r' then m₂ (ediam t) else ∞
have neg : ∀ (ht : ¬ediam t ≤ r'), ∞ ≤ c * ∞
Tactic: split_ifs with ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
have rcases : ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
  (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}),
  mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
Tactic: classical
  rcases (mem_nhdsGE_iff_exists_Ico_subset' zero_lt_one).1 hle with ⟨r, hr0, hr⟩
  refine fun s =>
    le_of_tendsto_of_tendsto (mkMetric'.tendsto_pre _ s)
      (ENNReal.Tendsto.const_mul (mkMetric'.tendsto_pre _ s) (Or.inr hc))
      (mem_of_superset (Ioo_mem_nhdsGT hr0) fun r' hr' => ?_)
  simp only [mem_setOf_eq, mkMetric'.pre]
  rw [← smul_eq_mul, ← smul_apply, smul_boundedBy hc]
  refine le_boundedBy.2 (fun t => (boundedBy_le _).trans ?_) _
  simp only [smul_eq_mul, Pi.smul_apply, extend, iInf_eq_if]
  split_ifs with ht
  · exact hr ⟨zero_le, ht.trans_lt hr'.2⟩
  · simp [h0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
rcases :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}),
    mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
have rcases₁ : ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
  (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r),
  Membership.mem (γ := Set ℝ≥0∞)
    {x : ℝ≥0∞ |
      (fun (x : ℝ≥0∞) ↦
          LE.le (α := ℝ≥0∞)
            ((fun (r : ℝ≥0∞) ↦
                (((mkMetric'.pre (fun (s : Set X) ↦ m₁ (ediam s)) r : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
              x)
            ((fun (b : ℝ≥0∞) ↦
                HMul.hMul (β := ℝ≥0∞) c
                  (((mkMetric'.pre (fun (s : Set X) ↦ m₂ (ediam s)) b : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
              x))
        x}
    r'
Tactic: classical
  rcases (mem_nhdsGE_iff_exists_Ico_subset' zero_lt_one).1 hle with ⟨r, hr0, hr⟩
  refine fun s =>
    le_of_tendsto_of_tendsto (mkMetric'.tendsto_pre _ s)
      (ENNReal.Tendsto.const_mul (mkMetric'.tendsto_pre _ s) (Or.inr hc))
      (mem_of_superset (Ioo_mem_nhdsGT hr0) fun r' hr' => ?_)
  simp only [mem_setOf_eq, mkMetric'.pre]
  rw [← smul_eq_mul, ← smul_apply, smul_boundedBy hc]
  refine le_boundedBy.2 (fun t => (boundedBy_le _).trans ?_) _
  simp only [smul_eq_mul, Pi.smul_apply, extend, iInf_eq_if]
  split_ifs with ht
  · exact hr ⟨zero_le, ht.trans_lt hr'.2⟩
  · simp [h0]