-- 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) = ⊤
r n : ℕ
⊢ ∑ a ∈ Finset.range n, μ (S (2 * a + 1 + r) \ S (2 * a + r)) ≤ μ (⋃ n, S n)

Tactic:
rw [← hm.finset_iUnion_of_pairwise_separated]

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 ∈ Finset.range n, S (2 * i + 1 + r) \ S (2 * i + r)) ≤ μ (⋃ n, S n)

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 ∈ Finset.range n,
    ∀ j ∈ Finset.range n,
      i ≠ j → Metric.AreSeparated (S (2 * i + 1 + r) \ S (2 * i + r)) (S (2 * j + 1 + r) \ S (2 * j + r))

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)
⊢ μ (⋃ n, S n) ≤ ⨆ n, μ (S n)

Tactic:
refine (μ.iUnion_nat_of_monotone_of_tsum_ne_top this ?_).le

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) = ⊤
this : ∀ (n : ℕ), S n ⊆ S (n + 1)
⊢ ∑' (k : ℕ), μ (S (k + 1) \ S k) ≠ ⊤

Proof state:
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}
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
have Ssep (n) : Metric.AreSeparated (S n) t :=
  ⟨n⁻¹, ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _),
    fun x hx y hy ↦ hx.2.trans <| infEdist_le_edist_of_mem hy⟩

Result:
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
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Proof state:
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
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
have iUnion_S : ⋃ n, S n = s \ t := by
  refine Subset.antisymm (iUnion_subset S_sub) ?_
  rintro x ⟨hxs, hxt⟩
  rw [mem_iff_infEdist_zero_of_closed ht] at hxt
  rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩
  exact mem_iUnion.2 ⟨n, hxs, hn.le⟩

Result:
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
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

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 : ℕ), i < j → Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))

Tactic:
intro i j hj

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
⊢ Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))

Proof state:
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
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
have hSs : ∀ n, μ (s ∩ t) + μ (S n) ≤ μ s := fun n =>
  calc
    μ (s ∩ t) + μ (S n) = μ (s ∩ t ∪ S n) := Eq.symm <| hm _ _ <| (Ssep' n).symm
    _ ≤ μ (s ∩ t ∪ s \ t) := μ.mono <| union_subset_union_right _ <| S_sub n
    _ = μ s := by rw [inter_union_diff]

Result:
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
⊢ μ (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 : ¬infEdist x t = 0
⊢ x ∈ ⋃ n, S n

Tactic:
rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩

Result:
case 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
x : X
hxs : x ∈ s
hxt : ¬infEdist x t = 0
n : ℕ
hn : (↑n)⁻¹ < infEdist x t
⊢ x ∈ ⋃ n, S n