∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (m : MeasureTheory.AddContent ENNReal C)
  (hC : MeasureTheory.IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive),
  s ∈ C → (m.measureCaratheodory hC m_sigma_subadd) s = m s