-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
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 (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
have have₁ have₂ :
  ∀
    (h_m_eq :
      ∀ (i : ℕ),
        (m : (a : Set α) → ℝ≥0∞) (f i) =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
            (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
      ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)
have₃ :
  ∀
    (h_m_eq :
      ∀ (i : ℕ),
        (m : (a : Set α) → ℝ≥0∞) (f i) =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
            (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
      ∑' (i : ℕ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
          (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have₄ :
  ∀
    (h_m_eq :
      ∀ (i : ℕ),
        (m : (a : Set α) → ℝ≥0∞) (f i) =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
            (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
      HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s))
        (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u)
refine_1 :
  ∀
    (h_m_eq :
      ∀ (i : ℕ),
        (m : (a : Set α) → ℝ≥0∞) (f i) =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
            (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s) : ℝ≥0∞)
refine_2 refine_2₁ :
  ∀
    (h_m_eq :
      ∀ (i : ℕ),
        (m : (a : Set α) → ℝ≥0∞) (f i) =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
            (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
      (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)

Tactic:
classical
  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
  simp_rw [h_m_eq]
  rw [ENNReal.tsum_add]
  refine add_le_add ?_ ?_
  · refine iInf_le_of_le (fun i ↦ f i ∩ s) <| iInf_le_of_le ?_ le_rfl
    rw [← iUnion_inter]
    exact Set.inter_subset_inter_left _ hf_subset
  · apply le_trans <| (OuterMeasure.ofFunction m addContent_empty).mono
      <| (iUnion_diff s f) ▸ diff_subset_diff_left hf_subset
    simp only [OuterMeasure.measureOf_eq_coe, A]
    apply le_trans <| measure_iUnion_le (μ := OuterMeasure.ofFunction m addContent_empty)
      (fun i ↦ f i \ s)
    apply ENNReal.tsum_le_tsum
    intro i
    simp_rw [sUnion_eq_biUnion] at h_diff_eq_sUnion
    rw [h_diff_eq_sUnion]
    obtain h6 := MeasureTheory.measure_biUnion_finset_le
      (μ := OuterMeasure.ofFunction m addContent_empty) (A i) id
    simp only [id_eq] at h6
    exact le_trans h6 <| Finset.sum_le_sum <| fun b _ ↦ OuterMeasure.ofFunction_le b

Premises used: ENNReal.tsum_le_tsum, le_rfl, ENNReal.tsum_add, MeasureTheory.OuterMeasure.mono, add_le_add, Set.sUnion_eq_biUnion, Set.iUnion_inter, Set.inter_subset_inter_left, Inter.inter, SDiff.sdiff, MeasureTheory.measure_iUnion_le, MeasureTheory.OuterMeasure.measureOf_eq_coe, MeasureTheory.OuterMeasure.ofFunction_le, Finset.sum_le_sum, iInf_le_of_le, DFunLike.coe, MeasureTheory.addContent_empty, MeasureTheory.OuterMeasure.ofFunction, id_eq, le_trans