Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
classical
  let M : MeasurableSpace α := generateFrom C
  have Mle : M ≤ hα := generateFrom_le h'C
  set μ' := μ.trim Mle with hμ'
  obtain ⟨m', m'C, hm'⟩ :
      ∃ m' : @VectorMeasure α M E _ _, (∀ s ∈ C, m' s = m s) ∧ ∀ s, ‖m' s‖ₑ ≤ μ' s := by
    apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom hC (fun s hs ↦ ?_) rfl
    apply (hm s hs).trans_eq
    exact (MeasureTheory.trim_measurableSet_eq Mle (measurableSet_generateFrom hs)).symm
  have m'_le : m'.variation ≤ μ' := by
    exact variation_le_of_forall_enorm_le (fun s hs ↦ hm' _)
  -- next line is to make sure that the default instance is picked below when defininig `m''`.
  let : MeasurableSpace α := hα
  let m'' : VectorMeasure α E :=
  { measureOf' s := if MeasurableSet s then ∫ᵛ x, μ[s.indicator 1 | M] x ∂• m' else 0
    empty' := by simp
    not_measurable' s hs := by simp [hs]
    m_iUnion' f f_meas hf := by
      have : ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m'
          = ∫ᵛ (x : α), ∑' d, μ[(f d).indicator 1 | M] x ∂•m' := by
        apply VectorMeasure.integral_congr_ae
        apply ae_mono m'_le
        apply ae_eq_trim_of_measurable _ (by fun_prop) (by fun_prop)
        apply condExp_tsum (fun i ↦ ?_)
        · simp only [enorm_indicator_eq_indicator_enorm, Pi.one_apply, enorm_one, f_meas,
            lintegral_indicator, lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
            Set.univ_inter, one_mul, ne_eq, ← measure_iUnion hf f_meas, measure_ne_top,
            not_false_eq_true]
        · exact AEStronglyMeasurable.indicator (by fun_prop) (f_meas i)
      simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion,
        indicator_iUnion_of_pairwise_disjoint _ hf, this]
      have I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ < ∞ := by
        have A i : ∫⁻ a, ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ = μ (f i) :=
          lintegral_enorm_condExp_indicator Mle (f_meas i)
        simp_rw [A, ← measure_iUnion hf f_meas]
        exact measure_lt_top _ _
      rw [integral_tsum (by fun_prop)]; swap
      · apply ne_of_lt
        grw [m'_le, hμ']
        have A i : Measurable[M] (fun x ↦ ‖μ[(f i).indicator (1 : α → ℝ) | M] x‖ₑ) := by fun_prop
        simp_rw [lintegral_trim Mle (A _)]
        exact I
      refine Summable.hasSum (Summable.of_enorm ?_)
      apply ne_of_lt (lt_of_le_of_lt ?_ I)
      gcongr with i
      grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_lsmul_le, one_mul,
        lintegral_mono' m'_le le_rfl, hμ', lintegral_trim _ (by fun_prop)] }
  refine ⟨m'', fun s hs ↦ ?_, fun s ↦ ?_⟩
  · simp only [coe_mk, h'C s hs, ↓reduceIte, m'']
    have : ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = ∫ᵛ (x : α), s.indicator 1 x ∂•m' := by
      apply integral_congr_ae
      filter_upwards with x
      rw [condExp_of_stronglyMeasurable Mle]
      · exact StronglyMeasurable.indicator stronglyMeasurable_const
          (measurableSet_generateFrom hs)
      · exact (integrable_const 1).indicator (h'C s hs)
    rw [this, integral_indicator (measurableSet_generateFrom hs)]
    have : IsFiniteMeasure m'.variation :=
      isFiniteMeasure_of_le _ m'_le
    simp only [Pi.one_apply, setIntegral_const]
    simp [m'C s hs]
  · by_cases hs : MeasurableSet s; swap
    · simp [not_measurable _ hs]
    simp only [coe_mk, hs, ↓reduceIte, m'']
    grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_lsmul_le, one_mul,
      lintegral_mono' m'_le le_rfl, hμ', lintegral_trim _ (by fun_prop),
      lintegral_enorm_condExp_indicator Mle hs]

Goal state after: