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)
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)
refine' iSup₂_le fun K hK => _
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)
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)
obtain ⟨t, ht⟩ :=
  K.isCompact.elim_finite_subcover _ (fun i => (U i).isOpen) (by rwa [← Opens.coe_iSup])
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)
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)
rcases K.isCompact.finite_compact_cover t (SetLike.coe ∘ U) (fun i _ => (U i).isOpen) ht with
  ⟨K', h1K', h2K', h3K'⟩
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)
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)
let L : ℕ → Compacts G := fun n => ⟨K' n, h1K' n⟩
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

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)
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)
convert le_trans (h3 t L) _
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)
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)
refine' le_trans (Finset.sum_le_sum _) (ENNReal.sum_le_tsum t)
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)
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)
intro i _
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)
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)
refine' le_trans _ (le_iSup _ (L i))
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)
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)
refine' le_trans _ (le_iSup _ (h2K' i))
no goals
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)
rfl
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)
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)
intro t K
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)

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)
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)
refine' Finset.induction_on t _ _
no goals
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)
simp only [μ.empty, nonpos_iff_eq_zero, Finset.sum_empty, Finset.sup_empty]
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)
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)
intro n s hn ih
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)
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)
rw [Finset.sup_insert, Finset.sum_insert hn]
no goals
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)
exact le_trans (μ.sup_le _ _) (add_le_add_left ih _)
no goals
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)
rwa [← Opens.coe_iSup]
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)
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
ext1
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)
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)
rw [Compacts.coe_finset_sup, Finset.sup_eq_iSup]
no goals
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)
exact h3K'