G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ borel G ≤ OuterMeasure.caratheodory (Content.outerMeasure μ)
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ S ≤ OuterMeasure.caratheodory (Content.outerMeasure μ)
rw [@BorelSpace.measurable_eq G _ _]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ ∀ (t : Set G), t ∈ {s | IsOpen s} → MeasurableSet t
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ borel G ≤ OuterMeasure.caratheodory (Content.outerMeasure μ)
refine' MeasurableSpace.generateFrom_le _
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
⊢ MeasurableSet U
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ ∀ (t : Set G), t ∈ {s | IsOpen s} → MeasurableSet t
intro U hU
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
⊢ ∀ (U_1 : Opens G),
    ↑(Content.outerMeasure μ) (↑U_1 ∩ U) + ↑(Content.outerMeasure μ) (↑U_1 \ U) ≤ ↑(Content.outerMeasure μ) ↑U_1
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
⊢ MeasurableSet U
rw [μ.outerMeasure_caratheodory]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ ↑(Content.outerMeasure μ) (↑U' ∩ U) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
⊢ ∀ (U_1 : Opens G),
    ↑(Content.outerMeasure μ) (↑U_1 ∩ U) + ↑(Content.outerMeasure μ) (↑U_1 \ U) ≤ ↑(Content.outerMeasure μ) ↑U_1
intro U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ innerContent μ { carrier := ↑U' ∩ U, is_open' := (_ : IsOpen (↑U' ∩ U)) } + ↑(Content.outerMeasure μ) (↑U' \ U) ≤
    ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ ↑(Content.outerMeasure μ) (↑U' ∩ U) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ (x : { i // ↑i ⊆ ↑{ carrier := ↑U' ∩ U, is_open' := (_ : IsOpen (↑U' ∩ U)) } }), ↑(toFun μ ↑x)) +
      ↑(Content.outerMeasure μ) (↑U' \ U) ≤
    ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ innerContent μ { carrier := ↑U' ∩ U, is_open' := (_ : IsOpen (↑U' ∩ U)) } + ↑(Content.outerMeasure μ) (↑U' \ U) ≤
    ↑(Content.outerMeasure μ) ↑U'
simp only [innerContent, iSup_subtype']
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ (x : { i // ↑i ⊆ ↑U' ∩ U }), ↑(toFun μ ↑x)) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ (x : { i // ↑i ⊆ ↑{ carrier := ↑U' ∩ U, is_open' := (_ : IsOpen (↑U' ∩ U)) } }), ↑(toFun μ ↑x)) +
      ↑(Content.outerMeasure μ) (↑U' \ U) ≤
    ↑(Content.outerMeasure μ) ↑U'
rw [Opens.coe_mk]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ (⨆ (x : { i // ↑i ⊆ ↑U' ∩ U }), ↑(toFun μ ↑x)) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ (x : { i // ↑i ⊆ ↑U' ∩ U }), ↑(toFun μ ↑x)) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
haveI : Nonempty { L : Compacts G // (L : Set G) ⊆ U' ∩ U } := ⟨⟨⊥, empty_subset _⟩⟩
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ (⨆ (b : { i // ↑i ⊆ ↑U' ∩ U }), ↑(toFun μ ↑b) + ↑(Content.outerMeasure μ) (↑U' \ U)) ≤ ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ (⨆ (x : { i // ↑i ⊆ ↑U' ∩ U }), ↑(toFun μ ↑x)) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
rw [ENNReal.iSup_add]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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 }), ↑(toFun μ ↑i) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ (⨆ (b : { i // ↑i ⊆ ↑U' ∩ U }), ↑(toFun μ ↑b) + ↑(Content.outerMeasure μ) (↑U' \ U)) ≤ ↑(Content.outerMeasure μ) ↑U'
refine' iSup_le _
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
⊢ ↑(toFun μ ↑{ val := L, property := hL }) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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 }), ↑(toFun μ ↑i) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
rintro ⟨L, hL⟩
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
⊢ ↑(toFun μ ↑{ val := L, property := hL }) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
simp only [subset_inter_iff] at hL
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
have : ↑U' \ U ⊆ U' \ L := diff_subset_diff_right hL.2
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) + ↑(Content.outerMeasure μ) (↑U' \ ↑L) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) + ↑(Content.outerMeasure μ) (↑U' \ U) ≤ ↑(Content.outerMeasure μ) ↑U'
refine' le_trans (add_le_add_left (μ.outerMeasure.mono' this) _) _
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) +
      innerContent μ { carrier := ↑U' \ ↑L, is_open' := (_ : IsOpen (↑U' \ ↑L)) } ≤
    ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) + ↑(Content.outerMeasure μ) (↑U' \ ↑L) ≤ ↑(Content.outerMeasure μ) ↑U'
rw [μ.outerMeasure_of_isOpen (↑U' \ L) (IsOpen.sdiff U'.2 L.2.isClosed)]
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ (↑(toFun μ L) + ⨆ (x : { i // ↑i ⊆ ↑{ carrier := ↑U' \ ↑L, is_open' := (_ : IsOpen (↑U' \ ↑L)) } }), ↑(toFun μ ↑x)) ≤
    ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ ↑{ val := L, property := hL✝ }) +
      innerContent μ { carrier := ↑U' \ ↑L, is_open' := (_ : IsOpen (↑U' \ ↑L)) } ≤
    ↑(Content.outerMeasure μ) ↑U'
simp only [innerContent, iSup_subtype']
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ (↑(toFun μ L) + ⨆ (x : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ ↑x)) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ (↑(toFun μ L) + ⨆ (x : { i // ↑i ⊆ ↑{ carrier := ↑U' \ ↑L, is_open' := (_ : IsOpen (↑U' \ ↑L)) } }), ↑(toFun μ ↑x)) ≤
    ↑(Content.outerMeasure μ) ↑U'
rw [Opens.coe_mk]
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
⊢ (↑(toFun μ L) + ⨆ (x : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ ↑x)) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this : ↑U' \ U ⊆ ↑U' \ ↑L
⊢ (↑(toFun μ L) + ⨆ (x : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ ↑x)) ≤ ↑(Content.outerMeasure μ) ↑U'
haveI : Nonempty { M : Compacts G // (M : Set G) ⊆ ↑U' \ L } := ⟨⟨⊥, empty_subset _⟩⟩
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
⊢ (⨆ (b : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ L) + ↑(toFun μ ↑b)) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
⊢ (↑(toFun μ L) + ⨆ (x : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ ↑x)) ≤ ↑(Content.outerMeasure μ) ↑U'
rw [ENNReal.add_iSup]
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
⊢ ∀ (i : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ L) + ↑(toFun μ ↑i) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
⊢ (⨆ (b : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ L) + ↑(toFun μ ↑b)) ≤ ↑(Content.outerMeasure μ) ↑U'
refine' iSup_le _
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM }) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
⊢ ∀ (i : { i // ↑i ⊆ ↑U' \ ↑L }), ↑(toFun μ L) + ↑(toFun μ ↑i) ≤ ↑(Content.outerMeasure μ) ↑U'
rintro ⟨M, hM⟩
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ }) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM }) ≤ ↑(Content.outerMeasure μ) ↑U'
simp only [subset_diff] at hM
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
this : ↑(L ⊔ M) ⊆ ↑U'
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ }) ≤ ↑(Content.outerMeasure μ) ↑U'
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ }) ≤ ↑(Content.outerMeasure μ) ↑U'
have : (↑(L ⊔ M) : Set G) ⊆ U' := by
  simp only [union_subset_iff, Compacts.coe_sup, hM, hL, and_self_iff]
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
this : ↑(L ⊔ M) ⊆ ↑U'
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ }) ≤
    innerContent μ { carrier := ↑U', is_open' := (_ : IsOpen U'.carrier) }
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
this : ↑(L ⊔ M) ⊆ ↑U'
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ }) ≤ ↑(Content.outerMeasure μ) ↑U'
rw [μ.outerMeasure_of_isOpen (↑U') U'.2]
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
this : ↑(L ⊔ M) ⊆ ↑U'
⊢ (fun s => ↑(toFun μ s)) (L ⊔ M) = ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ })
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
this : ↑(L ⊔ M) ⊆ ↑U'
⊢ ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ }) ≤
    innerContent μ { carrier := ↑U', is_open' := (_ : IsOpen U'.carrier) }
refine' le_trans (ge_of_eq _) (μ.le_innerContent _ _ this)
no goals
case mk.mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
this : ↑(L ⊔ M) ⊆ ↑U'
⊢ (fun s => ↑(toFun μ s)) (L ⊔ M) = ↑(toFun μ L) + ↑(toFun μ ↑{ val := M, property := hM✝ })
exact μ.sup_disjoint _ _ hM.2.symm
no goals
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space 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
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L
this : Nonempty { M // ↑M ⊆ ↑U' \ ↑L }
M : Compacts G
hM✝ : ↑M ⊆ ↑U' \ ↑L
hM : ↑M ⊆ ↑U' ∧ Disjoint ↑M ↑L
⊢ ↑(L ⊔ M) ⊆ ↑U'
simp only [union_subset_iff, Compacts.coe_sup, hM, hL, and_self_iff]