-- 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
α : 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 ⋯) (t \ s) ≤ ∑' (b : ℕ), ∑ u ∈ A b, m u

Tactic:
apply le_trans <| (OuterMeasure.ofFunction m addContent_empty).mono
  <| (iUnion_diff s f) ▸ diff_subset_diff_left hf_subset

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 ⋯).measureOf (⋃ i, f i \ s) ≤ ∑' (b : ℕ), ∑ u ∈ A b, 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 α),
    (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ (OuterMeasure.ofFunction ⇑m ⋯) t

Tactic:
intro t

Result:
α : 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 α
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ (OuterMeasure.ofFunction ⇑m ⋯) t

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 α
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ (OuterMeasure.ofFunction ⇑m ⋯) t

Tactic:
conv_rhs => rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]

Result:
α : 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 α
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤
    ⨅ t_1, ⨅ (_ : ∀ (i : ℕ), t_1 i ∈ C), ⨅ (_ : t ⊆ ⋃ i, t_1 i), ∑' (i : ℕ), m (t_1 i)

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
⊢ (OuterMeasure.ofFunction ⇑m ⋯).IsCaratheodory s

Tactic:
rw [OuterMeasure.isCaratheodory_iff_le']

Result:
α : 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 α),
    (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ (OuterMeasure.ofFunction ⇑m ⋯) t

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, (fun i => f i ∩ s) i

Tactic:
rw [← iUnion_inter]

Result:
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

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 ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
obtain h6 := MeasureTheory.measure_biUnion_finset_le
  (μ := OuterMeasure.ofFunction m addContent_empty) (A i) id

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, 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

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
⊢ ∑' (i : ℕ), (OuterMeasure.ofFunction ⇑m ⋯) (f i \ s) ≤ ∑' (b : ℕ), ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
apply ENNReal.tsum_le_tsum

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
⊢ ∀ (a : ℕ), (OuterMeasure.ofFunction ⇑m ⋯) (f a \ s) ≤ ∑ 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 ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ ∑' (i : ℕ), m (f i)

Tactic:
have h_m_eq i : m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u :=
  eq_add_disjointOfDiff_of_subset hC (hC.inter_mem (f i) (hf i) s hs) (hf i) inter_subset_left

Result:
α : 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 ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ ∑' (i : ℕ), m (f i)