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

Proof state:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ ∀ (a : ℕ), (OuterMeasure.ofFunction ⇑m ⋯) (f a \ s) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
intro i

Result:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (f i \ s) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ t ∩ s ⊆ (⋃ i, f i) ∩ s

Tactic:
exact Set.inter_subset_inter_left _ hf_subset

Result:
no goals

Proof state:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (f i \ s) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
rw [h_diff_eq_sUnion]

Result:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Proof state:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
h6 : (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ A i, id i_1) ≤ ∑ i ∈ A i, (OuterMeasure.ofFunction ⇑m ⋯) (id i)
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
simp only [id_eq] at h6

Result:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
h6 : (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ A i, i_1) ≤ ∑ x ∈ A i, (OuterMeasure.ofFunction ⇑m ⋯) x
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
i : ℕ
⊢ f i \ s = ⋃₀ ↑(A i)

Tactic:
simp [A, IsSetSemiring.sUnion_disjointOfDiff]

Result:
no goals

Proof state:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (f i \ s) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
simp_rw [sUnion_eq_biUnion] at h_diff_eq_sUnion

Result:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (f i \ s) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i, f i \ s) ≤ ∑' (b : ℕ), ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
apply le_trans <| measure_iUnion_le (μ := OuterMeasure.ofFunction m addContent_empty)
  (fun i ↦ f i \ s)

Result:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ ∑' (i : ℕ), (OuterMeasure.ofFunction ⇑m ⋯) (f i \ s) ≤ ∑' (b : ℕ), ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯).measureOf (⋃ i, f i \ s) ≤ ∑' (b : ℕ), ∑ u ∈ A b, m u

Tactic:
simp only [OuterMeasure.measureOf_eq_coe, A]

Result:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i, f i \ s) ≤ ∑' (b : ℕ), ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Proof state:
case refine_2.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_top : ∀ s ∉ C, m s = ⊤
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i => hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
h6 : (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ A i, i_1) ≤ ∑ x ∈ A i, (OuterMeasure.ofFunction ⇑m ⋯) x
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
exact le_trans h6 <| Finset.sum_le_sum <| fun b _ ↦ OuterMeasure.ofFunction_le b

Result:
no goals