-- Mathlib/MeasureTheory/Measure/Content.lean
theorem borel_le_caratheodory : S ≤ μ.outerMeasure.caratheodory

Proof state:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
⊢ ∀ (i : { i // ↑i ⊆ ↑U' \ ↑L' }), μ L' + μ ↑i ≤ μ.outerMeasure ↑U'

Tactic:
rintro ⟨M, hM⟩

Result:
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
⊢ μ L' + μ ↑⟨M, hM⟩ ≤ μ.outerMeasure ↑U'

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ ∀ (i : { i // ↑i ⊆ ↑U' ∩ U }), μ ↑i + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
rintro ⟨L, hL⟩

Result:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
hL : ↑L ⊆ ↑U' ∩ U
⊢ μ ↑⟨L, hL⟩ + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Proof state:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
hL : ↑L ⊆ ↑U' ∩ U
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
⊢ μ ↑⟨L, hL⟩ + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
suffices μ L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure U' by
  have A : μ L ≤ μ L' := μ.mono _ _ subset_closure
  exact (add_le_add_right A _).trans this

Result:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
hL : ↑L ⊆ ↑U' ∩ U
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
⊢ μ L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
⊢ ↑(L' ⊔ M') ⊆ ↑U'

Tactic:
simp only [Compacts.coe_sup, union_subset_iff, hL'U', true_and]

Result:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
⊢ ↑M' ⊆ ↑U'

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
⊢ ↑M' ⊆ ↑U'

Tactic:
exact hM'.trans diff_subset

Result:
no goals

Proof state:
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
this : ↑(L' ⊔ M') ⊆ ↑U'
⊢ μ L' + μ M' ≤ μ.outerMeasure ↑U'

Tactic:
rw [μ.outerMeasure_of_isOpen (↑U') U'.2]

Result:
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
this : ↑(L' ⊔ M') ⊆ ↑U'
⊢ μ L' + μ M' ≤ μ.innerContent { carrier := ↑U', is_open' := ⋯ }

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ μ.innerContent { carrier := ↑U' ∩ U, is_open' := ⋯ } + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
simp only [innerContent, iSup_subtype']

Result:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ x, μ ↑x) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Proof state:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
hL : ↑L ⊆ ↑U' ∩ U
⊢ μ ↑⟨L, hL⟩ + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
let L' : Compacts G := ⟨closure L, L.isCompact.closure⟩

Result:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
hL : ↑L ⊆ ↑U' ∩ U
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
⊢ μ ↑⟨L, hL⟩ + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'