-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem borel_le_caratheodory (hm : IsMetric μ) : borel X ≤ μ.caratheodory

Proof state:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
this : ∀ (n : ℕ), S n ⊆ S (n + 1)
⊢ ∑' (k : ℕ), μ (S (k + 1) \ S k) ≠ ⊤

Tactic:
clear this

Result:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
⊢ ∑' (k : ℕ), μ (S (k + 1) \ S k) ≠ ⊤

Proof state:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
⊢ Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))

Tactic:
have A : ((↑(2 * j + r))⁻¹ : ℝ≥0∞) < (↑(2 * i + 1 + r))⁻¹ := by
  rw [ENNReal.inv_lt_inv, Nat.cast_lt]; omega

Result:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
⊢ Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))

Proof state:
case neg.intro.intro
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
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))⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r))⁻¹
hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ ≤ edist x y

Tactic:
apply ENNReal.le_of_add_le_add_right hyz.ne_top

Result:
case neg.intro.intro
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
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))⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r))⁻¹
hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ + edist y z ≤ edist x y + edist y z

Proof state:
case pos
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : μ (s \ t) = ⊤
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
rw [htop, add_top, ← htop]

Result:
case pos
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : μ (s \ t) = ⊤
⊢ μ (s \ t) ≤ μ s

Proof state:
case intro
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
x : X
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ⋃ n, S n

Tactic:
rw [mem_iff_infEdist_zero_of_closed ht] at hxt

Result:
case intro
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
x : X
hxs : x ∈ s
hxt : ¬infEdist x t = 0
⊢ x ∈ ⋃ n, S n

Proof state:
case neg.intro.intro
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
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))⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r))⁻¹
hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ + edist y z ≤ edist x y + edist y z

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

Result:
case neg.intro.intro
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
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))⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r))⁻¹
hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ + edist y z ≤ edist x z