awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)⁻¹
neg :
  ∀ (z : X) (hzt : z ∈ t) (hyz : edist y z < (↑(2 * j + r) : ℝ≥0∞)⁻¹),
    HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ ≤ edist x y
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ ≤ edist x y

Tactic:
rcases infEDist_lt_iff.mp this with ⟨z, hzt, hyz⟩

Premises used: Iff.mp, Metric.infEDist_lt_iff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)⁻¹
⊢ (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ ≤ edist x z

Tactic:
have hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z := le_infEDist.1 hx.2 _ hzt
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
neg : HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x y + edist y z
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ ≤ edist x y

Tactic:
apply ENNReal.le_of_add_le_add_right hyz.ne_top

Premises used: LT.lt.ne_top, ENNReal.le_of_add_le_add_right
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

Tactic:
le_trans ?_ (edist_triangle _ _ _)

Premises used: le_trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
neg : HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x z
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x y + edist y z

Tactic:
refine le_trans ?_ (edist_triangle _ _ _)

Premises used: le_trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

Tactic:
(add_le_add le_rfl hyz.le).trans (Eq.trans_le ?_ hxz)

Premises used: le_rfl, add_le_add, LT.lt.le, Eq.trans_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
neg :
  HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + (↑(2 * j + r) : ℝ≥0∞)⁻¹ =
    (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + edist y z ≤ edist x z

Tactic:
refine (add_le_add le_rfl hyz.le).trans (Eq.trans_le ?_ hxz)

Premises used: le_rfl, add_le_add, LT.lt.le, Eq.trans_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
neg neg₁ : Eq (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹
⊢ HSub.hSub (α := ℝ≥0∞) (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹ (↑(2 * j + r) : ℝ≥0∞)⁻¹ + (↑(2 * j + r) : ℝ≥0∞)⁻¹ =
    (↑(2 * i + 1 + r) : ℝ≥0∞)⁻¹

Tactic:
rw [tsub_add_cancel_of_le A.le]

Premises used: tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
hm : μ.IsMetric
rw : borel X ≤ μ.caratheodory
⊢ inst_1 ≤ μ.caratheodory

Tactic:
rw [BorelSpace.measurable_eq (α := X)]

Premises used: BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory

Tactic:
hm.borel_le_caratheodory

Premises used: MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory

Tactic:
exact hm.borel_le_caratheodory

Premises used: MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
r : ℝ≥0∞
μ : OuterMeasure X
⊢ μ ≤ pre m r ↔ ∀ (s : Set X), ediam s ≤ r → (μ : (a : Set X) → ℝ≥0∞) s ≤ m s

Tactic:
simp only [pre, le_boundedBy, extend, le_iInf_iff]

Premises used: MeasureTheory.extend, le_iInf_iff, MeasureTheory.OuterMeasure.mkMetric'.pre, MeasureTheory.OuterMeasure.le_boundedBy
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ (pre m r : (a : Set X) → ℝ≥0∞) s ≤ m s

Tactic:
(boundedBy_le _).trans <| iInf_le _ hs

Premises used: MeasureTheory.OuterMeasure.boundedBy_le, LE.le.trans, iInf_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
r r' : ℝ≥0∞
h : r ≤ r'
⊢ pre m r' ≤ pre m r

Tactic:
le_pre.2 fun _ hs => pre_le (hs.trans h)

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.mkMetric'.pre_le, LE.le.trans, MeasureTheory.OuterMeasure.mkMetric'.le_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
k l : ℕ
h : k ≤ l
x : Set X
hs : ediam x ≤ (↑l : ℝ≥0∞)⁻¹
⊢ LE.le (α := ℝ≥0∞) (↑l : ℝ≥0∞)⁻¹ (↑k : ℝ≥0∞)⁻¹

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ ((pre m r : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((mkMetric' m : (a : Set X) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
rw [← tendsto_comp_coe_Ioi_atBot]

Premises used: tendsto_comp_coe_Ioi_atBot
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
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))
⊢ 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:
simp only [mkMetric', OuterMeasure.iSup_apply, iSup_subtype']

Premises used: iSup_subtype', MeasureTheory.OuterMeasure.mkMetric', MeasureTheory.OuterMeasure.iSup_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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) atBot
    (𝓝 (⨆ (i : { i : ℝ≥0∞ // i > 0 }), (pre m (↑i : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s))

Tactic:
tendsto_atBot_iSup fun r r' hr => mono_pre _ hr _

Premises used: Set.Ioi, Set.Mem, setOf, tendsto_atBot_iSup, MeasureTheory.OuterMeasure.mkMetric'.mono_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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) atBot
    (𝓝 (⨆ (i : { i : ℝ≥0∞ // i > 0 }), (pre m (↑i : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s))

Tactic:
exact tendsto_atBot_iSup fun r r' hr => mono_pre _ hr _

Premises used: tendsto_atBot_iSup, MeasureTheory.OuterMeasure.mkMetric'.mono_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)

Tactic:
(tendsto_pre m s).comp (tendsto_inf.2 ⟨ENNReal.tendsto_inv_nat_nhds_zero, ?_⟩)

Premises used: Iff.mpr, Filter.tendsto_inf, MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, ENNReal.tendsto_inv_nat_nhds_zero, And.intro, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
refine : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)⁻¹) atTop (𝓟 (Ioi 0))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((pre m (↑n : ℝ≥0∞)⁻¹ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((mkMetric' m : (a : Set X) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
refine (tendsto_pre m s).comp (tendsto_inf.2 ⟨ENNReal.tendsto_inv_nat_nhds_zero, ?_⟩)

Premises used: Iff.mpr, Filter.tendsto_inf, MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, ENNReal.tendsto_inv_nat_nhds_zero, And.intro, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)⁻¹) atTop (𝓟 (Ioi 0))

Tactic:
tendsto_principal.2 (Eventually.of_forall fun n => ?_)

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.tendsto_principal
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
refine : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) (↑n : ℝ≥0∞)⁻¹
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)⁻¹) atTop (𝓟 (Ioi 0))

Tactic:
refine tendsto_principal.2 (Eventually.of_forall fun n => ?_)

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.tendsto_principal
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
n : ℕ
⊢ Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) (↑n : ℝ≥0∞)⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
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∞)
⊢ mkMetric' m = ⨆ (n : ℕ), pre m (↑n : ℝ≥0∞)⁻¹

Tactic:
ext1 s
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
h :
  Eq (α := ℝ≥0∞) ((mkMetric' m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : ℕ), (pre m (↑i : ℝ≥0∞)⁻¹ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((mkMetric' m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (n : ℕ), pre m (↑n : ℝ≥0∞)⁻¹ : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [iSup_apply]

Premises used: MeasureTheory.OuterMeasure.iSup_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
    (⨆ (i : ℕ), (pre m (↑i : ℝ≥0∞)⁻¹ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
tendsto_nhds_unique (mkMetric'.tendsto_pre_nat m s)
    (tendsto_atTop_iSup fun k l hkl => mkMetric'.mono_pre_nat m hkl s)

Premises used: MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat, MeasureTheory.OuterMeasure.mkMetric'.mono_pre_nat, tendsto_atTop_iSup, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
    (⨆ (i : ℕ), (pre m (↑i : ℝ≥0∞)⁻¹ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine tendsto_nhds_unique (mkMetric'.tendsto_pre_nat m s)
    (tendsto_atTop_iSup fun k l hkl => mkMetric'.mono_pre_nat m hkl s)

Premises used: MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat, MeasureTheory.OuterMeasure.mkMetric'.mono_pre_nat, tendsto_atTop_iSup, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

Tactic:
le_antisymm (le_pre.2 fun s hs => ?_) (le_trim _)

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.le_trim, le_antisymm, MeasureTheory.OuterMeasure.mkMetric'.le_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞
refine : ∀ (s : Set X) (hs : ediam s ≤ r), ((pre m r).trim : (a : Set X) → ℝ≥0∞) s ≤ m s
⊢ (pre m r).trim = pre m r

Tactic:
refine le_antisymm (le_pre.2 fun s hs => ?_) (le_trim _)

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.le_trim, le_antisymm, MeasureTheory.OuterMeasure.mkMetric'.le_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
rw : ⨅ (t : Set X), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r : (a : Set X) → ℝ≥0∞) t ≤ m s
⊢ ((pre m r).trim : (a : Set X) → ℝ≥0∞) s ≤ m s

Tactic:
rw [trim_eq_iInf]

Premises used: MeasureTheory.OuterMeasure.trim_eq_iInf
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

Tactic:
iInf_le_of_le (closure s) <| iInf_le_of_le subset_closure <|
    iInf_le_of_le measurableSet_closure ((pre_le ?_).trans_eq (hcl _))

Premises used: LE.le.trans_eq, subset_closure, measurableSet_closure, MeasureTheory.OuterMeasure.mkMetric'.pre_le, closure, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
refine : ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ r
⊢ ⨅ (t : Set X), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r : (a : Set X) → ℝ≥0∞) t ≤ m s

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 _))

Premises used: subset_closure, measurableSet_closure, closure, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 rwa rwa₁ rwa₂ rwa₃ : ediam s ≤ r
⊢ ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ r

Tactic:
rwa [ediam_closure]

Premises used: Metric.ediam_closure
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)

Tactic:
tendsto_nhds_unique_of_eventuallyEq
    (mkMetric'.tendsto_pre _ _) ((mkMetric'.tendsto_pre _ _).add (mkMetric'.tendsto_pre _ _)) ?_

Premises used: MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, tendsto_nhds_unique_of_eventuallyEq, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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∞)
⊢ (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∞)

Tactic:
refine tendsto_nhds_unique_of_eventuallyEq
    (mkMetric'.tendsto_pre _ _) ((mkMetric'.tendsto_pre _ _).add (mkMetric'.tendsto_pre _ _)) ?_

Premises used: MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, tendsto_nhds_unique_of_eventuallyEq, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ 0 < r

Tactic:
rw [← pos_iff_ne_zero] at r0

Premises used: pos_iff_ne_zero