ProbabilityTheory.Measure.ext_iff_singleton_finiteSupport

theorem Measure.ext_iff_singleton_finiteSupport    {μ1 μ2 : Measure S} [FiniteSupport μ1] [FiniteSupport μ2] :    μ1 = μ2 ↔ ∀ x, μ1 {x} = μ2 {x} := by  classical  constructor  · rintro rfl    simp  · let A1 := μ1.support    have hA1 := measure_compl_support μ1    let A2 := μ2.support    have hA2 := measure_compl_support μ2    intro h    ext s    have h1 : μ1 s = μ1 (s ∩ (A1 ∪ A2)) := by      apply (measure_eq_measure_of_null_sdiff _ _).symm      · simp      refine measure_mono_null ?_ hA1      intro x      simp (config := { contextual := true }) [A1]    have h2 : μ2 s = μ2 (s ∩ (A1 ∪ A2)) := by      apply (measure_eq_measure_of_null_sdiff _ _).symm      · simp      exact measure_mono_null (fun x ↦ by simp (config := { contextual := true }) [A2]) hA2    rw [h1, h2]    have hs : Set.Finite (s ∩ (A1 ∪ A2)) := Set.toFinite (s ∩ (↑A1 ∪ ↑A2))    rw [← hs.coe_toFinset, ← sum_measure_singleton (μ := μ1), ← sum_measure_singleton (μ := μ2)]    simp_rw [h]