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

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
⊢ ⋃ n, S n = s \ t

Tactic:
refine Subset.antisymm (iUnion_subset S_sub) ?_

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 ⊆ ⋃ 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
n : ℕ
⊢ μ (s ∩ t ∪ s \ t) = μ s

Tactic:
rw [inter_union_diff]

Result:
no goals

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

Tactic:
exact μ.mono (iUnion_subset fun i => iUnion_subset fun _ x hx => mem_iUnion.2 ⟨_, hx.1⟩)

Result:
no goals

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

Tactic:
refine fun r => ne_top_of_le_ne_top htop ?_

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 : ℕ
⊢ ∑' (k : ℕ), μ (S (2 * k + 1 + r) \ S (2 * k + r)) ≤ μ (s \ t)

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

Tactic:
exact μ.mono diff_subset

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) = ⊤
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ ≠ 0

Tactic:
simpa [tsub_eq_zero_iff_le] using A

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
⊢ s \ t ⊆ ⋃ n, S n

Tactic:
rintro x ⟨hxs, 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 : x ∉ t
⊢ x ∈ ⋃ 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 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)
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ ≤ edist x y

Tactic:
have : infEdist y t < (↑(2 * j + r))⁻¹ := not_le.1 fun hle => hy.2 ⟨hy.1, hle⟩

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))⁻¹
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))⁻¹
⊢ (↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹ ≤ edist x y

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) = ⊤
⊢ ∑' (k : ℕ), μ (S (2 * k + 1) \ S (2 * k)) ≠ ⊤ ∧ ∑' (k : ℕ), μ (S (2 * k + 1 + 1) \ S (2 * k + 1)) ≠ ⊤

Tactic:
suffices ∀ a, (∑' k : ℕ, μ (S (2 * k + 1 + a) \ S (2 * k + a))) ≠ ∞ from
  ⟨by simpa using this 0, by simpa using this 1⟩

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