[GOAL]
G : Type w
inst✝ : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → (fun x => 0) K₁ ≤ (fun x => 0) K₂
[PROOFSTEP]
simp
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → (fun x => 0) (K₁ ⊔ K₂) = (fun x => 0) K₁ + (fun x => 0) K₂
[PROOFSTEP]
simp
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), (fun x => 0) (K₁ ⊔ K₂) ≤ (fun x => 0) K₁ + (fun x => 0) K₂
[PROOFSTEP]
simp
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
⊢ (fun s => ↑(toFun μ s)) K₁ ≤ (fun s => ↑(toFun μ s)) K₂
[PROOFSTEP]
simp [apply_eq_coe_toFun, μ.mono' _ _ h]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : Disjoint ↑K₁ ↑K₂
⊢ (fun s => ↑(toFun μ s)) (K₁ ⊔ K₂) = (fun s => ↑(toFun μ s)) K₁ + (fun s => ↑(toFun μ s)) K₂
[PROOFSTEP]
simp [apply_eq_coe_toFun, μ.sup_disjoint' _ _ h]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ (fun s => ↑(toFun μ s)) (K₁ ⊔ K₂) ≤ (fun s => ↑(toFun μ s)) K₁ + (fun s => ↑(toFun μ s)) K₂
[PROOFSTEP]
simp only [apply_eq_coe_toFun]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ ↑(toFun μ (K₁ ⊔ K₂)) ≤ ↑(toFun μ K₁) + ↑(toFun μ K₂)
[PROOFSTEP]
norm_cast
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ toFun μ (K₁ ⊔ K₂) ≤ toFun μ K₁ + toFun μ K₂
[PROOFSTEP]
exact μ.sup_le' _ _
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ (fun s => ↑(toFun μ s)) ⊥ = 0
[PROOFSTEP]
have := μ.sup_disjoint' ⊥ ⊥
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
this : Disjoint ↑⊥ ↑⊥ → toFun μ (⊥ ⊔ ⊥) = toFun μ ⊥ + toFun μ ⊥
⊢ (fun s => ↑(toFun μ s)) ⊥ = 0
[PROOFSTEP]
simpa [apply_eq_coe_toFun] using this
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ = 0
[PROOFSTEP]
refine' le_antisymm _ (zero_le _)
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ ≤ 0
[PROOFSTEP]
rw [← μ.empty]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ ≤ (fun s => ↑(toFun μ s)) ⊥
[PROOFSTEP]
refine' iSup₂_le fun K hK => _
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ (fun s => ↑(toFun μ s)) K ≤ (fun s => ↑(toFun μ s)) ⊥
[PROOFSTEP]
have : K = ⊥ := by
  ext1
  rw [subset_empty_iff.mp hK, Compacts.coe_bot]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ K = ⊥
[PROOFSTEP]
ext1
[GOAL]
case h
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥
[PROOFSTEP]
rw [subset_empty_iff.mp hK, Compacts.coe_bot]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ (fun s => ↑(toFun μ s)) K ≤ (fun s => ↑(toFun μ s)) ⊥
[PROOFSTEP]
rw [this]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
have h'ε := ENNReal.coe_ne_zero.2 hε
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
cases' le_or_lt (μ.innerContent U) ε with h h
[GOAL]
case inl
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : innerContent μ U ≤ ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
exact ⟨⊥, empty_subset _, le_add_left h⟩
[GOAL]
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
have h₂ := ENNReal.sub_lt_self hU h.ne_bot h'ε
[GOAL]
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
conv at h₂ => rhs; rw [innerContent]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
| innerContent μ U - ↑ε < innerContent μ U
[PROOFSTEP]
rhs; rw [innerContent]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
| innerContent μ U - ↑ε < innerContent μ U
[PROOFSTEP]
rhs; rw [innerContent]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
| innerContent μ U - ↑ε < innerContent μ U
[PROOFSTEP]
rhs
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
| innerContent μ U
[PROOFSTEP]
rw [innerContent]
[GOAL]
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < ⨆ (K : Compacts G) (_ : ↑K ⊆ ↑U), (fun s => ↑(toFun μ s)) K
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
simp only [lt_iSup_iff] at h₂
[GOAL]
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : ∃ i i_1, innerContent μ U - ↑ε < ↑(toFun μ i)
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
rcases h₂ with ⟨U, h1U, h2U⟩
[GOAL]
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ ∃ K, ↑K ⊆ ↑U✝ ∧ innerContent μ U✝ ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
refine' ⟨U, h1U, _⟩
[GOAL]
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ innerContent μ U✝ ≤ (fun s => ↑(toFun μ s)) U + ↑ε
[PROOFSTEP]
rw [← tsub_le_iff_right]
[GOAL]
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ innerContent μ U✝ - ↑ε ≤ (fun s => ↑(toFun μ s)) U
[PROOFSTEP]
exact le_of_lt h2U
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
⊢ innerContent μ (⨆ (i : ℕ), U i) ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
have h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ t.sum fun i => μ (K i) :=
  by
  intro t K
  refine' Finset.induction_on t _ _
  · simp only [μ.empty, nonpos_iff_eq_zero, Finset.sum_empty, Finset.sup_empty]
  · intro n s hn ih
    rw [Finset.sup_insert, Finset.sum_insert hn]
    exact le_trans (μ.sup_le _ _) (add_le_add_left ih _)
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
⊢ ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
[PROOFSTEP]
intro t K
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
[PROOFSTEP]
refine' Finset.induction_on t _ _
[GOAL]
case refine'_1
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ (fun s => ↑(toFun μ s)) (Finset.sup ∅ K) ≤ Finset.sum ∅ fun i => (fun s => ↑(toFun μ s)) (K i)
[PROOFSTEP]
simp only [μ.empty, nonpos_iff_eq_zero, Finset.sum_empty, Finset.sup_empty]
[GOAL]
case refine'_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      ((fun s => ↑(toFun μ s)) (Finset.sup s K) ≤ Finset.sum s fun i => (fun s => ↑(toFun μ s)) (K i)) →
        (fun s => ↑(toFun μ s)) (Finset.sup (insert a s) K) ≤
          Finset.sum (insert a s) fun i => (fun s => ↑(toFun μ s)) (K i)
[PROOFSTEP]
intro n s hn ih
[GOAL]
case refine'_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
n : ℕ
s : Finset ℕ
hn : ¬n ∈ s
ih : (fun s => ↑(toFun μ s)) (Finset.sup s K) ≤ Finset.sum s fun i => (fun s => ↑(toFun μ s)) (K i)
⊢ (fun s => ↑(toFun μ s)) (Finset.sup (insert n s) K) ≤ Finset.sum (insert n s) fun i => (fun s => ↑(toFun μ s)) (K i)
[PROOFSTEP]
rw [Finset.sup_insert, Finset.sum_insert hn]
[GOAL]
case refine'_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
n : ℕ
s : Finset ℕ
hn : ¬n ∈ s
ih : (fun s => ↑(toFun μ s)) (Finset.sup s K) ≤ Finset.sum s fun i => (fun s => ↑(toFun μ s)) (K i)
⊢ (fun s => ↑(toFun μ s)) (K n ⊔ Finset.sup s K) ≤
    (fun s => ↑(toFun μ s)) (K n) + Finset.sum s fun x => (fun s => ↑(toFun μ s)) (K x)
[PROOFSTEP]
exact le_trans (μ.sup_le _ _) (add_le_add_left ih _)
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
⊢ innerContent μ (⨆ (i : ℕ), U i) ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
refine' iSup₂_le fun K hK => _
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
⊢ (fun s => ↑(toFun μ s)) K ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
obtain ⟨t, ht⟩ := K.isCompact.elim_finite_subcover _ (fun i => (U i).isOpen) (by rwa [← Opens.coe_iSup])
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
⊢ ↑K ⊆ ⋃ (i : ℕ), ↑(U i)
[PROOFSTEP]
rwa [← Opens.coe_iSup]
[GOAL]
case intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
⊢ (fun s => ↑(toFun μ s)) K ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
rcases K.isCompact.finite_compact_cover t (SetLike.coe ∘ U) (fun i _ => (U i).isOpen) ht with ⟨K', h1K', h2K', h3K'⟩
[GOAL]
case intro.intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
⊢ (fun s => ↑(toFun μ s)) K ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
let L : ℕ → Compacts G := fun n => ⟨K' n, h1K' n⟩
[GOAL]
case intro.intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
⊢ (fun s => ↑(toFun μ s)) K ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
convert le_trans (h3 t L) _
[GOAL]
case h.e'_3.h.e'_1
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
⊢ K = Finset.sup t L
[PROOFSTEP]
ext1
[GOAL]
case h.e'_3.h.e'_1.h
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
⊢ ↑K = ↑(Finset.sup t L)
[PROOFSTEP]
rw [Compacts.coe_finset_sup, Finset.sup_eq_iSup]
[GOAL]
case h.e'_3.h.e'_1.h
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
⊢ ↑K = ⨆ (a : ℕ) (_ : a ∈ t), ↑(L a)
[PROOFSTEP]
exact h3K'
[GOAL]
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
⊢ (Finset.sum t fun i => (fun s => ↑(toFun μ s)) (L i)) ≤ ∑' (i : ℕ), innerContent μ (U i)
[PROOFSTEP]
refine' le_trans (Finset.sum_le_sum _) (ENNReal.sum_le_tsum t)
[GOAL]
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
⊢ ∀ (i : ℕ), i ∈ t → (fun s => ↑(toFun μ s)) (L i) ≤ innerContent μ (U i)
[PROOFSTEP]
intro i _
[GOAL]
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
i : ℕ
a✝ : i ∈ t
⊢ (fun s => ↑(toFun μ s)) (L i) ≤ innerContent μ (U i)
[PROOFSTEP]
refine' le_trans _ (le_iSup _ (L i))
[GOAL]
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
i : ℕ
a✝ : i ∈ t
⊢ (fun s => ↑(toFun μ s)) (L i) ≤ ⨆ (_ : ↑(L i) ⊆ ↑(U i)), (fun s => ↑(toFun μ s)) (L i)
[PROOFSTEP]
refine' le_trans _ (le_iSup _ (h2K' i))
[GOAL]
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Opens G
h3 :
  ∀ (t : Finset ℕ) (K : ℕ → Compacts G),
    (fun s => ↑(toFun μ s)) (Finset.sup t K) ≤ Finset.sum t fun i => (fun s => ↑(toFun μ s)) (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ (i : ℕ), U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ (i : ℕ) (_ : i ∈ t), ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ (i : ℕ) (_ : i ∈ t), K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := (_ : IsCompact (K' n)) }
i : ℕ
a✝ : i ∈ t
⊢ (fun s => ↑(toFun μ s)) (L i) ≤ (fun s => ↑(toFun μ s)) (L i)
[PROOFSTEP]
rfl
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
⊢ innerContent μ { carrier := ⋃ (i : ℕ), U i, is_open' := (_ : IsOpen (⋃ (i : ℕ), U i)) } ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
[PROOFSTEP]
have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  innerContent μ (⨆ (i : ℕ), { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ innerContent μ { carrier := ⋃ (i : ℕ), U i, is_open' := (_ : IsOpen (⋃ (i : ℕ), U i)) } ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
[PROOFSTEP]
rwa [Opens.iSup_def] at this
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
⊢ innerContent μ (↑(Opens.comap (Homeomorph.toContinuousMap f)) U) = innerContent μ U
[PROOFSTEP]
refine' (Compacts.equiv f).surjective.iSup_congr _ fun K => iSup_congr_Prop image_subset_iff _
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
⊢ ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U) →
    (fun s => ↑(toFun μ s)) (↑(Compacts.equiv f) K) = (fun s => ↑(toFun μ s)) K
[PROOFSTEP]
intro hK
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U)
⊢ (fun s => ↑(toFun μ s)) (↑(Compacts.equiv f) K) = (fun s => ↑(toFun μ s)) K
[PROOFSTEP]
simp only [Equiv.coe_fn_mk, Subtype.mk_eq_mk, Compacts.equiv]
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U)
⊢ ↑(toFun μ (Compacts.map ↑f (_ : Continuous ↑f) K)) = ↑(toFun μ K)
[PROOFSTEP]
apply h
[GOAL]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
g : G
U : Opens G
⊢ innerContent μ (↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U) = innerContent μ U
[PROOFSTEP]
convert μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
⊢ 0 < innerContent μ U
[PROOFSTEP]
have : (interior (U : Set G)).Nonempty
[GOAL]
case this
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
⊢ Set.Nonempty (interior ↑U)
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this : Set.Nonempty (interior ↑U)
⊢ 0 < innerContent μ U
[PROOFSTEP]
rwa [U.isOpen.interior_eq]
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this : Set.Nonempty (interior ↑U)
⊢ 0 < innerContent μ U
[PROOFSTEP]
rcases compact_covered_by_mul_left_translates K.2 this with ⟨s, hs⟩
[GOAL]
case intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
⊢ 0 < innerContent μ U
[PROOFSTEP]
suffices μ K ≤ s.card * μ.innerContent U by exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this✝ : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
this : (fun s => ↑(toFun μ s)) K ≤ ↑(Finset.card s) * innerContent μ U
⊢ 0 < innerContent μ U
[PROOFSTEP]
exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2
[GOAL]
case intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Finset.card s) * innerContent μ U
[PROOFSTEP]
have : (K : Set G) ⊆ ↑(⨆ g ∈ s, Opens.comap (Homeomorph.mulLeft g).toContinuousMap U) := by
  simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
⊢ ↑K ⊆ ↑(⨆ (g : G) (_ : g ∈ s), ↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U)
[PROOFSTEP]
simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]
[GOAL]
case intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this✝ : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ (g : G) (_ : g ∈ s), ↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U)
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Finset.card s) * innerContent μ U
[PROOFSTEP]
refine' (μ.le_innerContent _ _ this).trans _
[GOAL]
case intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this✝ : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ (g : G) (_ : g ∈ s), ↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U)
⊢ innerContent μ (⨆ (g : G) (_ : g ∈ s), ↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U) ≤
    ↑(Finset.card s) * innerContent μ U
[PROOFSTEP]
refine' (rel_iSup_sum μ.innerContent μ.innerContent_bot (· ≤ ·) μ.innerContent_iSup_nat _ _).trans _
[GOAL]
case intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Opens G
hU : Set.Nonempty ↑U
this✝ : Set.Nonempty (interior ↑U)
s : Finset G
hs : K.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ (g : G) (_ : g ∈ s), ↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U)
⊢ (Finset.sum s fun d => innerContent μ (↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft d))) U)) ≤
    ↑(Finset.card s) * innerContent μ U
[PROOFSTEP]
simp only [μ.is_mul_left_invariant_innerContent h3, Finset.sum_const, nsmul_eq_mul, le_refl]
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Content.outerMeasure μ) ↑K
[PROOFSTEP]
rw [Content.outerMeasure, inducedOuterMeasure_eq_iInf]
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤
    ⨅ (t : Set G) (ht : IsOpen t) (_ : ↑K ⊆ t), innerContent μ { carrier := t, is_open' := ht }
[PROOFSTEP]
exact le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩
[GOAL]
case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ (i : ℕ), f i)
[PROOFSTEP]
exact fun U hU => isOpen_iUnion hU
[GOAL]
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    innerContent μ { carrier := ⋃ (i : ℕ), f i, is_open' := (_ : IsOpen (⋃ (i : ℕ), (fun i => f i) i)) } ≤
      ∑' (i : ℕ), innerContent μ { carrier := f i, is_open' := (_ : IsOpen (f i)) }
[PROOFSTEP]
exact μ.innerContent_iUnion_nat
[GOAL]
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → innerContent μ { carrier := s₁, is_open' := hs₁ } ≤ innerContent μ { carrier := s₂, is_open' := hs₂ }
[PROOFSTEP]
exact μ.innerContent_mono
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : ↑(Content.outerMeasure μ) ↑U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ ↑(Content.outerMeasure μ) ↑U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
[PROOFSTEP]
rw [μ.outerMeasure_opens] at hU ⊢
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
[PROOFSTEP]
rcases μ.innerContent_exists_compact hU hε with ⟨K, h1K, h2K⟩
[GOAL]
case intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
[PROOFSTEP]
exact ⟨K, h1K, le_trans h2K <| add_le_add_right (μ.le_outerMeasure_compacts K) _⟩
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
hA : ↑(Content.outerMeasure μ) A ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ U, A ⊆ ↑U ∧ ↑(Content.outerMeasure μ) ↑U ≤ ↑(Content.outerMeasure μ) A + ↑ε
[PROOFSTEP]
rcases inducedOuterMeasure_exists_set _ μ.innerContent_iUnion_nat μ.innerContent_mono hA (ENNReal.coe_ne_zero.2 hε) with
  ⟨U, hU, h2U, h3U⟩
[GOAL]
case intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
hA : ↑(Content.outerMeasure μ) A ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
U : Set G
hU : IsOpen U
h2U : A ⊆ U
h3U :
  ↑(inducedOuterMeasure (fun s₁ hs₁ => innerContent μ { carrier := s₁, is_open' := hs₁ }) (_ : IsOpen ∅)
          (_ : innerContent μ ⊥ = 0))
      U ≤
    ↑(inducedOuterMeasure (fun s₁ hs₁ => innerContent μ { carrier := s₁, is_open' := hs₁ }) (_ : IsOpen ∅)
            (_ : innerContent μ ⊥ = 0))
        A +
      ↑ε
⊢ ∃ U, A ⊆ ↑U ∧ ↑(Content.outerMeasure μ) ↑U ≤ ↑(Content.outerMeasure μ) A + ↑ε
[PROOFSTEP]
exact ⟨⟨U, hU⟩, h2U, h3U⟩
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A : Set G
⊢ ↑(Content.outerMeasure μ) (↑f ⁻¹' A) = ↑(Content.outerMeasure μ) A
[PROOFSTEP]
refine' inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _ (fun _ => f.isOpen_preimage) _
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A : Set G
⊢ ∀ (s : Set G) (hs : IsOpen s),
    innerContent μ { carrier := ↑f.toEquiv ⁻¹' s, is_open' := (_ : IsOpen (↑f.toEquiv ⁻¹' s)) } =
      innerContent μ { carrier := s, is_open' := hs }
[PROOFSTEP]
intro s hs
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A s : Set G
hs : IsOpen s
⊢ innerContent μ { carrier := ↑f.toEquiv ⁻¹' s, is_open' := (_ : IsOpen (↑f.toEquiv ⁻¹' s)) } =
    innerContent μ { carrier := s, is_open' := hs }
[PROOFSTEP]
convert μ.innerContent_comap f h ⟨s, hs⟩
[GOAL]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
⊢ ↑(Content.outerMeasure μ) K < ⊤
[PROOFSTEP]
rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩
[GOAL]
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ ↑(Content.outerMeasure μ) K < ⊤
[PROOFSTEP]
calc
  μ.outerMeasure K ≤ μ.outerMeasure (interior F) := OuterMeasure.mono' _ h2F
  _ ≤ μ ⟨F, h1F⟩ := by apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset
  _ < ⊤ := μ.lt_top _
[GOAL]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ ↑(Content.outerMeasure μ) (interior F) ≤ (fun s => ↑(toFun μ s)) { carrier := F, isCompact' := h1F }
[PROOFSTEP]
apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
g : G
A : Set G
⊢ ↑(Content.outerMeasure μ) ((fun x => g * x) ⁻¹' A) = ↑(Content.outerMeasure μ) A
[PROOFSTEP]
convert μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Opens G),
      ↑(Content.outerMeasure μ) (↑U ∩ A) + ↑(Content.outerMeasure μ) (↑U \ A) ≤ ↑(Content.outerMeasure μ) ↑U
[PROOFSTEP]
rw [Opens.forall]
[GOAL]
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      ↑(Content.outerMeasure μ) (↑{ carrier := U, is_open' := hU } ∩ A) +
          ↑(Content.outerMeasure μ) (↑{ carrier := U, is_open' := hU } \ A) ≤
        ↑(Content.outerMeasure μ) ↑{ carrier := U, is_open' := hU }
[PROOFSTEP]
apply inducedOuterMeasure_caratheodory
[GOAL]
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    innerContent μ { carrier := ⋃ (i : ℕ), f i, is_open' := (_ : ?P (⋃ (i : ℕ), f i)) } ≤
      ∑' (i : ℕ), innerContent μ { carrier := f i, is_open' := (_ : IsOpen (f i)) }
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → innerContent μ { carrier := s₁, is_open' := hs₁ } ≤ innerContent μ { carrier := s₂, is_open' := hs₂ }
case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ (i : ℕ), f i)
[PROOFSTEP]
apply innerContent_iUnion_nat
[GOAL]
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → innerContent μ { carrier := s₁, is_open' := hs₁ } ≤ innerContent μ { carrier := s₂, is_open' := hs₂ }
[PROOFSTEP]
apply innerContent_mono'
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Set G
h1U : IsOpen U
h2U : Set.Nonempty U
⊢ 0 < ↑(Content.outerMeasure μ) U
[PROOFSTEP]
convert μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U
[GOAL]
case h.e'_4
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Set G
h1U : IsOpen U
h2U : Set.Nonempty U
⊢ ↑(Content.outerMeasure μ) U = innerContent μ { carrier := U, is_open' := h1U }
[PROOFSTEP]
exact μ.outerMeasure_opens ⟨U, h1U⟩
[GOAL]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ S ≤ OuterMeasure.caratheodory (Content.outerMeasure μ)
[PROOFSTEP]
rw [@BorelSpace.measurable_eq G _ _]
[GOAL]
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ borel G ≤ OuterMeasure.caratheodory (Content.outerMeasure μ)
[PROOFSTEP]
refine' MeasurableSpace.generateFrom_le _
[GOAL]
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
[PROOFSTEP]
intro U hU
[GOAL]
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
[PROOFSTEP]
rw [μ.outerMeasure_caratheodory]
[GOAL]
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
[PROOFSTEP]
intro U'
[GOAL]
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'
[PROOFSTEP]
rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]
[GOAL]
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'
[PROOFSTEP]
simp only [innerContent, iSup_subtype']
[GOAL]
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'
[PROOFSTEP]
rw [Opens.coe_mk]
[GOAL]
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'
[PROOFSTEP]
haveI : Nonempty { L : Compacts G // (L : Set G) ⊆ U' ∩ U } := ⟨⟨⊥, empty_subset _⟩⟩
[GOAL]
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'
[PROOFSTEP]
rw [ENNReal.iSup_add]
[GOAL]
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'
[PROOFSTEP]
refine' iSup_le _
[GOAL]
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'
[PROOFSTEP]
rintro ⟨L, hL⟩
[GOAL]
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'
[PROOFSTEP]
simp only [subset_inter_iff] at hL
[GOAL]
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'
[PROOFSTEP]
have : ↑U' \ U ⊆ U' \ L := diff_subset_diff_right hL.2
[GOAL]
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'
[PROOFSTEP]
refine' le_trans (add_le_add_left (μ.outerMeasure.mono' this) _) _
[GOAL]
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'
[PROOFSTEP]
rw [μ.outerMeasure_of_isOpen (↑U' \ L) (IsOpen.sdiff U'.2 L.2.isClosed)]
[GOAL]
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'
[PROOFSTEP]
simp only [innerContent, iSup_subtype']
[GOAL]
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'
[PROOFSTEP]
rw [Opens.coe_mk]
[GOAL]
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'
[PROOFSTEP]
haveI : Nonempty { M : Compacts G // (M : Set G) ⊆ ↑U' \ L } := ⟨⟨⊥, empty_subset _⟩⟩
[GOAL]
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'
[PROOFSTEP]
rw [ENNReal.add_iSup]
[GOAL]
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'
[PROOFSTEP]
refine' iSup_le _
[GOAL]
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'
[PROOFSTEP]
rintro ⟨M, hM⟩
[GOAL]
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'
[PROOFSTEP]
simp only [subset_diff] at hM
[GOAL]
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'
[PROOFSTEP]
have : (↑(L ⊔ M) : Set G) ⊆ U' := by simp only [union_subset_iff, Compacts.coe_sup, hM, hL, and_self_iff]
[GOAL]
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'
[PROOFSTEP]
simp only [union_subset_iff, Compacts.coe_sup, hM, hL, and_self_iff]
[GOAL]
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'
[PROOFSTEP]
rw [μ.outerMeasure_of_isOpen (↑U') U'.2]
[GOAL]
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) }
[PROOFSTEP]
refine' le_trans (ge_of_eq _) (μ.le_innerContent _ _ this)
[GOAL]
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✝ })
[PROOFSTEP]
exact μ.sup_disjoint _ _ hM.2.symm
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
⊢ Measure.Regular (Content.measure μ)
[PROOFSTEP]
have : μ.measure.OuterRegular := by
  refine' ⟨fun A hA r (hr : _ < _) => _⟩
  rw [μ.measure_apply hA, outerMeasure_eq_iInf] at hr
  simp only [iInf_lt_iff] at hr
  rcases hr with ⟨U, hUo, hAU, hr⟩
  rw [← μ.outerMeasure_of_isOpen U hUo, ← μ.measure_apply hUo.measurableSet] at hr
  exact ⟨U, hAU, hUo, hr⟩
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
⊢ Measure.OuterRegular (Content.measure μ)
[PROOFSTEP]
refine' ⟨fun A hA r (hr : _ < _) => _⟩
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ↑↑(Content.measure μ) A < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(Content.measure μ) U < r
[PROOFSTEP]
rw [μ.measure_apply hA, outerMeasure_eq_iInf] at hr
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ⨅ (U : Set G) (hU : IsOpen U) (_ : A ⊆ U), innerContent μ { carrier := U, is_open' := hU } < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(Content.measure μ) U < r
[PROOFSTEP]
simp only [iInf_lt_iff] at hr
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ∃ i h i_1, innerContent μ { carrier := i, is_open' := (_ : IsOpen i) } < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(Content.measure μ) U < r
[PROOFSTEP]
rcases hr with ⟨U, hUo, hAU, hr⟩
[GOAL]
case intro.intro.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : innerContent μ { carrier := U, is_open' := (_ : IsOpen U) } < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(Content.measure μ) U < r
[PROOFSTEP]
rw [← μ.outerMeasure_of_isOpen U hUo, ← μ.measure_apply hUo.measurableSet] at hr
[GOAL]
case intro.intro.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : ↑↑(Content.measure μ) U < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(Content.measure μ) U < r
[PROOFSTEP]
exact ⟨U, hAU, hUo, hr⟩
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this : Measure.OuterRegular (Content.measure μ)
⊢ Measure.Regular (Content.measure μ)
[PROOFSTEP]
have : IsFiniteMeasureOnCompacts μ.measure := by
  refine' ⟨fun K hK => _⟩
  rw [measure_apply _ hK.measurableSet]
  exact μ.outerMeasure_lt_top_of_isCompact hK
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this : Measure.OuterRegular (Content.measure μ)
⊢ IsFiniteMeasureOnCompacts (Content.measure μ)
[PROOFSTEP]
refine' ⟨fun K hK => _⟩
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this : Measure.OuterRegular (Content.measure μ)
K : Set G
hK : IsCompact K
⊢ ↑↑(Content.measure μ) K < ⊤
[PROOFSTEP]
rw [measure_apply _ hK.measurableSet]
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this : Measure.OuterRegular (Content.measure μ)
K : Set G
hK : IsCompact K
⊢ ↑(Content.outerMeasure μ) K < ⊤
[PROOFSTEP]
exact μ.outerMeasure_lt_top_of_isCompact hK
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this✝ : Measure.OuterRegular (Content.measure μ)
this : IsFiniteMeasureOnCompacts (Content.measure μ)
⊢ Measure.Regular (Content.measure μ)
[PROOFSTEP]
refine' ⟨fun U hU r hr => _⟩
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this✝ : Measure.OuterRegular (Content.measure μ)
this : IsFiniteMeasureOnCompacts (Content.measure μ)
U : Set G
hU : IsOpen U
r : ℝ≥0∞
hr : r < ↑↑(Content.measure μ) U
⊢ ∃ K, K ⊆ U ∧ IsCompact K ∧ r < ↑↑(Content.measure μ) K
[PROOFSTEP]
rw [measure_apply _ hU.measurableSet, μ.outerMeasure_of_isOpen U hU] at hr
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this✝ : Measure.OuterRegular (Content.measure μ)
this : IsFiniteMeasureOnCompacts (Content.measure μ)
U : Set G
hU : IsOpen U
r : ℝ≥0∞
hr : r < innerContent μ { carrier := U, is_open' := hU }
⊢ ∃ K, K ⊆ U ∧ IsCompact K ∧ r < ↑↑(Content.measure μ) K
[PROOFSTEP]
simp only [innerContent, lt_iSup_iff] at hr
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this✝ : Measure.OuterRegular (Content.measure μ)
this : IsFiniteMeasureOnCompacts (Content.measure μ)
U : Set G
hU : IsOpen U
r : ℝ≥0∞
hr : ∃ i i_1, r < ↑(toFun μ i)
⊢ ∃ K, K ⊆ U ∧ IsCompact K ∧ r < ↑↑(Content.measure μ) K
[PROOFSTEP]
rcases hr with ⟨K, hKU, hr⟩
[GOAL]
case intro.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this✝ : Measure.OuterRegular (Content.measure μ)
this : IsFiniteMeasureOnCompacts (Content.measure μ)
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : ↑K ⊆ ↑{ carrier := U, is_open' := hU }
hr : r < ↑(toFun μ K)
⊢ ∃ K, K ⊆ U ∧ IsCompact K ∧ r < ↑↑(Content.measure μ) K
[PROOFSTEP]
refine' ⟨K, hKU, K.2, hr.trans_le _⟩
[GOAL]
case intro.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : LocallyCompactSpace G
this✝ : Measure.OuterRegular (Content.measure μ)
this : IsFiniteMeasureOnCompacts (Content.measure μ)
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : ↑K ⊆ ↑{ carrier := U, is_open' := hU }
hr : r < ↑(toFun μ K)
⊢ ↑(toFun μ K) ≤ ↑↑(Content.measure μ) ↑K
[PROOFSTEP]
exact (μ.le_outerMeasure_compacts K).trans (le_toMeasure_apply _ _ _)
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
by_contra hc
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ False
[PROOFSTEP]
simp only [not_exists, not_and, not_le] at hc
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
⊢ False
[PROOFSTEP]
have lower_bound_iInf :
  μ K + ε ≤ ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K' :=
  le_iInf fun K' => le_iInf fun K'_hyp => le_of_lt (hc K' K'_hyp)
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
lower_bound_iInf :
  (fun s => ↑(toFun μ s)) K + ↑ε ≤ ⨅ (K' : Compacts G) (_ : ↑K ⊆ interior ↑K'), (fun s => ↑(toFun μ s)) K'
⊢ False
[PROOFSTEP]
rw [← H] at lower_bound_iInf
[GOAL]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
lower_bound_iInf : (fun s => ↑(toFun μ s)) K + ↑ε ≤ (fun s => ↑(toFun μ s)) K
⊢ False
[PROOFSTEP]
exact
  (lt_self_iff_false (μ K)).mp
    (lt_of_le_of_lt' lower_bound_iInf (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ↑↑(Content.measure μ) ↑K = (fun s => ↑(toFun μ s)) K
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K
[PROOFSTEP]
apply ENNReal.le_of_forall_pos_le_add
[GOAL]
case refine'_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ∀ (ε : ℝ≥0), 0 < ε → (fun s => ↑(toFun μ s)) K < ⊤ → ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
intro ε εpos _
[GOAL]
case refine'_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
obtain ⟨K', K'_hyp⟩ := contentRegular_exists_compact μ H K (ne_bot_of_gt εpos)
[GOAL]
case refine'_1.h.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
[PROOFSTEP]
calc
  μ.measure ↑K ≤ μ.measure (interior ↑K') :=
    by
    rw [μ.measure_apply isOpen_interior.measurableSet, μ.measure_apply K.isCompact.measurableSet]
    exact μ.outerMeasure.mono K'_hyp.left
  _ ≤ μ K' := by
    rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
    exact μ.outerMeasure_interior_compacts K'
  _ ≤ μ K + ε := K'_hyp.right
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) ↑K ≤ ↑↑(Content.measure μ) (interior ↑K')
[PROOFSTEP]
rw [μ.measure_apply isOpen_interior.measurableSet, μ.measure_apply K.isCompact.measurableSet]
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑(Content.outerMeasure μ) ↑K ≤ ↑(Content.outerMeasure μ) (interior ↑K')
[PROOFSTEP]
exact μ.outerMeasure.mono K'_hyp.left
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) (interior ↑K') ≤ (fun s => ↑(toFun μ s)) K'
[PROOFSTEP]
rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
[GOAL]
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑(Content.outerMeasure μ) (interior ↑K') ≤ (fun s => ↑(toFun μ s)) K'
[PROOFSTEP]
exact μ.outerMeasure_interior_compacts K'
[GOAL]
case refine'_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑↑(Content.measure μ) ↑K
[PROOFSTEP]
rw [μ.measure_apply (IsCompact.measurableSet K.isCompact)]
[GOAL]
case refine'_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Content.outerMeasure μ) ↑K
[PROOFSTEP]
exact μ.le_outerMeasure_compacts K


[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
⊢ (fun i => { re := ↑s i, im := ↑t i }) ∅ = 0
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := ↑s ∅, im := ↑t ∅ } = 0
[PROOFSTEP]
rw [s.empty, t.empty]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := 0, im := 0 } = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ (fun i => { re := ↑s i, im := ↑t i }) i = 0
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ { re := ↑s i, im := ↑t i } = 0
[PROOFSTEP]
rw [s.not_measurable hi, t.not_measurable hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ { re := 0, im := 0 } = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
c d : ComplexMeasure α
⊢ Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ c + Equiv.toFun src✝ d
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
⊢ ∀ (r : R) (x : ComplexMeasure α),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
          x
[PROOFSTEP]
intro r c
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
      (r • c) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
        c
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
⊢ (mapRange (r • c) (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
      mapRange (r • c) (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im) =
    (r • mapRange c (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
      r • mapRange c (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im)
[PROOFSTEP]
ext
[GOAL]
case h₁.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (r • c) (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            mapRange (r • c) (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).fst
      i✝ =
    ↑(r • mapRange c (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            r • mapRange c (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).fst
      i✝
[PROOFSTEP]
simp [Complex.smul_re]
[GOAL]
case h₂.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (r • c) (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            mapRange (r • c) (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).snd
      i✝ =
    ↑(r • mapRange c (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            r • mapRange c (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).snd
      i✝
[PROOFSTEP]
simp [Complex.smul_im]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ ↔ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ → ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ → c ≪ᵥ μ
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
[PROOFSTEP]
constructor
[GOAL]
case mp.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑re c ≪ᵥ μ
[PROOFSTEP]
intro i hi
[GOAL]
case mp.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(↑re c) i = 0
[PROOFSTEP]
simp [h hi]
[GOAL]
case mp.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑im c ≪ᵥ μ
[PROOFSTEP]
intro i hi
[GOAL]
case mp.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(↑im c) i = 0
[PROOFSTEP]
simp [h hi]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
⊢ c ≪ᵥ μ
[PROOFSTEP]
intro i hi
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑c i = 0
[PROOFSTEP]
rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).im = 0
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).re = 0
[PROOFSTEP]
exacts [by simp, h.2 hi, h.1 hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0
[PROOFSTEP]
simp


[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t, (∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), ↑↑μ (t i) = 0) ∧ Pairwise (Disjoint on fun i => s i \ t i)
[PROOFSTEP]
refine'
  ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({ i }ᶜ : Set ι), s j), fun i => measurableSet_toMeasurable _ _, fun i => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ ↑↑μ ((fun i => toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j)) i) = 0
[PROOFSTEP]
simp only [measure_toMeasurable, inter_iUnion]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ ↑↑μ (⋃ (i_1 : ι) (_ : i_1 ∈ {i}ᶜ), s i ∩ s i_1) = 0
[PROOFSTEP]
exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ Pairwise (Disjoint on fun i => s i \ (fun i => toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j)) i)
[PROOFSTEP]
simp only [Pairwise, disjoint_left, onFun, mem_diff, not_and, and_imp, Classical.not_not]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∀ ⦃i j : ι⦄,
    i ≠ j →
      ∀ ⦃a : α⦄,
        a ∈ s i →
          ¬a ∈ toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j) →
            a ∈ s j → a ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
intro i j hne x hi hU hj
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hU : ¬x ∈ toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j)
hj : x ∈ s j
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
replace hU : x ∉ s i ∩ iUnion λ j => iUnion λ _ => s j := λ h => hU (subset_toMeasurable _ _ h)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : ¬x ∈ s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
simp only [mem_inter_iff, mem_iUnion, not_and, not_exists] at hU
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : x ∈ s i → ∀ (x_1 : ι), x_1 ∈ {i}ᶜ → ¬x ∈ s x_1
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
exact (hU hi j hne.symm hj).elim
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
⊢ AEDisjoint μ t s
[PROOFSTEP]
rwa [AEDisjoint, inter_comm]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : Disjoint s t
⊢ AEDisjoint μ s t
[PROOFSTEP]
rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ (i : ι), s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t
[PROOFSTEP]
simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t✝ u v : Set α
inst✝ : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ (i : ι), t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)
[PROOFSTEP]
simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
⊢ AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u
[PROOFSTEP]
simp [union_eq_iUnion, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
⊢ AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u
[PROOFSTEP]
simp [union_eq_iUnion, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.9910 h \ t
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.9910 h ∧ ¬x ∈ t
[PROOFSTEP]
exact ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩