-- Mathlib/MeasureTheory/Measure/Content.lean
theorem innerContent_iSup_nat [R1Space G] (U : ℕ → Opens G) :
    μ.innerContent (⨆ i : ℕ, U i) ≤ ∑' i : ℕ, μ.innerContent (U i)

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
⊢ ↑K ⊆ ⋃ i, ↑(U i)

Tactic:
rwa [← Opens.coe_iSup]

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
⊢ μ K ≤ ∑' (i : ℕ), μ.innerContent (U i)

Tactic:
let L : ℕ → Compacts G := fun n => ⟨K' n, h1K' n⟩

Result:
case intro.intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
⊢ μ K ≤ ∑' (i : ℕ), μ.innerContent (U i)

Proof state:
case h.e'_3.h.e'_6
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
⊢ K = t.sup L

Tactic:
ext1

Result:
case h.e'_3.h.e'_6.h
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
⊢ ↑K = ↑(t.sup L)

Proof state:
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
i : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ ⨆ (_ : ↑(L i) ⊆ ↑(U i)), μ (L i)

Tactic:
refine le_trans ?_ (le_iSup _ (h2K' i))

Result:
case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
i : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ μ (L i)

Proof state:
case refine_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ}, a ∉ s → μ (s.sup K) ≤ ∑ i ∈ s, μ (K i) → μ ((insert a s).sup K) ≤ ∑ i ∈ insert a s, μ (K i)

Tactic:
intro n s hn ih

Result:
case refine_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
n : ℕ
s : Finset ℕ
hn : n ∉ s
ih : μ (s.sup K) ≤ ∑ i ∈ s, μ (K i)
⊢ μ ((insert n s).sup K) ≤ ∑ i ∈ insert n s, μ (K i)

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)

Tactic:
refine Finset.induction_on t ?_ ?_

Result:
case refine_1
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ μ (∅.sup K) ≤ ∑ i ∈ ∅, μ (K i)

case refine_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ}, a ∉ s → μ (s.sup K) ≤ ∑ i ∈ s, μ (K i) → μ ((insert a s).sup K) ≤ ∑ i ∈ insert a s, μ (K i)

Proof state:
case refine_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
n : ℕ
s : Finset ℕ
hn : n ∉ s
ih : μ (s.sup K) ≤ ∑ i ∈ s, μ (K i)
⊢ μ ((insert n s).sup K) ≤ ∑ i ∈ insert n s, μ (K i)

Tactic:
rw [Finset.sup_insert, Finset.sum_insert hn]

Result:
case refine_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
n : ℕ
s : Finset ℕ
hn : n ∉ s
ih : μ (s.sup K) ≤ ∑ i ∈ s, μ (K i)
⊢ μ (K n ⊔ s.sup K) ≤ μ (K n) + ∑ x ∈ s, μ (K x)

Proof state:
case intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
⊢ μ K ≤ ∑' (i : ℕ), μ.innerContent (U i)

Tactic:
rcases K.isCompact.finite_compact_cover t (SetLike.coe ∘ U) (fun i _ => (U i).isOpen) ht with
  ⟨K', h1K', h2K', h3K'⟩

Result:
case intro.intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
⊢ μ K ≤ ∑' (i : ℕ), μ.innerContent (U i)

Proof state:
case intro.intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
⊢ μ K ≤ ∑' (i : ℕ), μ.innerContent (U i)

Tactic:
convert le_trans (h3 t L) _

Result:
case h.e'_3.h.e'_6
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
⊢ K = t.sup L

case intro.intro.intro.intro.convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }
⊢ ∑ i ∈ t, μ (L i) ≤ ∑' (i : ℕ), μ.innerContent (U i)