-- Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean
theorem ofFunction_eq (hC : IsSetSemiring C) (m : AddContent C)
    (m_sigma_subadd : m.IsSigmaSubadditive) (m_top : ∀ s ∉ C, m s = ∞) (hs : s ∈ C) :
    OuterMeasure.ofFunction m addContent_empty s = m s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m (s ∩ ⋃ i, f i) = m (⋃ i, s ∩ f i)

Tactic:
rw [inter_iUnion]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ ∑' (i : ℕ), m (s ∩ f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
refine tsum_le_tsum (fun i ↦ ?_) ENNReal.summable ENNReal.summable

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
i : ℕ
⊢ m (s ∩ f i) ≤ m (f i)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
⊢ m s ≤ (OuterMeasure.ofFunction ⇑m ⋯) s

Tactic:
rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
⊢ m s ≤ ⨅ t, ⨅ (_ : ∀ (i : ℕ), t i ∈ C), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
i : ℕ
⊢ m (s ∩ f i) ≤ m (f i)

Tactic:
exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
⊢ m s ≤ ⨅ t, ⨅ (_ : ∀ (i : ℕ), t i ∈ C), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)

Tactic:
refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hs_subset ↦ ?_

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s ≤ ∑' (i : ℕ), m (f i)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m (⋃ i, s ∩ f i) ≤ ∑' (i : ℕ), m (s ∩ f i)

Tactic:
refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ ⋃ i, s ∩ f i ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ ⋃ i, s ∩ f i ∈ C

Tactic:
rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s ≤ ∑' (i : ℕ), m (f i)

Tactic:
calc m s = m (s ∩ ⋃ i, f i) := by rw [inter_eq_self_of_subset_left hs_subset]
  _ = m (⋃ i, s ∩ f i) := by rw [inter_iUnion]
  _ ≤ ∑' i, m (s ∩ f i) := by
    refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_
    rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]
  _ ≤ ∑' i, m (f i) := by
    refine tsum_le_tsum (fun i ↦ ?_) ENNReal.summable ENNReal.summable
    exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
⊢ (OuterMeasure.ofFunction ⇑m ⋯) s = m s

Tactic:
refine le_antisymm (OuterMeasure.ofFunction_le s) ?_

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
⊢ m s ≤ (OuterMeasure.ofFunction ⇑m ⋯) s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s = m (s ∩ ⋃ i, f i)

Tactic:
rw [inter_eq_self_of_subset_left hs_subset]

Result:
no goals