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

Tactic:
intro n

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

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

Tactic:
suffices ∀ i j, i < j → Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r)) from
  fun i _ j _ hij => hij.lt_or_lt.elim
    (fun h => (this i j h).mono inter_subset_left fun x hx => by exact ⟨hx.1.1, hx.2⟩)
    fun h => (this j i h).symm.mono (fun x hx => by exact ⟨hx.1.1, hx.2⟩) inter_subset_left

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 : ℕ), i < j → Metric.AreSeparated (S (2 * i + 1 + r)) (s \ 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) = ⊤
r : ℕ
⊢ ∑' (k : ℕ), μ (S (2 * k + 1 + r) \ S (2 * k + r)) ≤ μ (s \ t)

Tactic:
rw [← iUnion_S, ENNReal.tsum_eq_iSup_nat, iSup_le_iff]

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

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
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
this : μ (⋃ n, S n) ≤ ⨆ n, μ (S n)
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
calc
μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
_ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
_ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
_ ≤ μ s := iSup_le hSs

Result:
no goals

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
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
this : μ (⋃ n, S n) ≤ ⨆ n, μ (S n)
⊢ μ (s ∩ t) + μ (⋃ n, S n) ≤ μ (s ∩ t) + ⨆ n, μ (S n)

Tactic:
gcongr

Result:
no goals

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))⁻¹ + (↑(2 * j + r))⁻¹ = (↑(2 * i + 1 + r))⁻¹

Tactic:
rw [tsub_add_cancel_of_le A.le]

Result:
no goals

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 z

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

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))⁻¹ + (↑(2 * j + r))⁻¹ = (↑(2 * i + 1 + r))⁻¹