awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
pos :
  ∀ (hsc : c ∈ s),
    (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
neg :
  ∀ (hsc : c ∉ s),
    (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)

Tactic:
by_cases hsc : c ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
pos :
  (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
pos₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
pos₂ pos₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)

Tactic:
rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]

Premises used: Iff.mpr, if_pos, mul_one, Set.indicator_eq_one_iff_mem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∉ s
neg :
  (μ : (a : Set α) → ℝ≥0∞) ∅ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
neg₁ : (μ : (a : Set α) → ℝ≥0∞) ∅ = HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
neg₂ : 0 = HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
neg₃ neg₄ : Eq (α := ℝ≥0∞) 0 0
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)

Tactic:
rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]

Premises used: Iff.mpr, MeasureTheory.measure_empty, MulZeroClass.mul_zero, Set.indicator_eq_zero_iff_notMem, if_neg
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
h :
  (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c) ⁻¹' s) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
h₁ h₂ h₃ :
  (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
pos :
  ∀ (hsc : c ∈ s),
    (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
neg neg₁ :
  ∀ (hsc : c ∉ s),
    (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
⊢ ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)

Tactic:
classical
  rw [Measure.map_apply measurable_const hs, Set.preimage_const]
  by_cases hsc : c ∈ s
  · rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
  · rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]

Premises used: MeasureTheory.Measure.map_apply, Set.preimage_const, MeasureTheory.measure_empty, MulZeroClass.mul_zero, measurable_const, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.restrict {a} : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : (a : Set α) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ μ.restrict {a} = HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
pos :
  ∀ (ha : a ∈ s),
    Eq (α := ℝ≥0∞) ((μ.restrict {a} : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : (a : Set α) → ℝ≥0∞)
          s :
        ℝ≥0∞)
neg :
  ∀ (ha : a ∉ s),
    Eq (α := ℝ≥0∞) ((μ.restrict {a} : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : (a : Set α) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict {a} : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
have : s ∩ {a} = {a} := by simpa
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ Eq (α := ℝ≥0∞) ((μ.restrict {a} : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
this : s ∩ {a} = ∅
⊢ Eq (α := ℝ≥0∞) ((μ.restrict {a} : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ ν : Measure α
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
⊢ Eq (α := Set α) (⋃₀ range singleton) univ

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ ν : Measure α
h : ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
⊢ ∀ (s : Set α), Membership.mem (γ := Set (Set α)) (range singleton) s → μ.restrict s = ν.restrict s

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ ν : Measure α
⊢ μ = ν ↔ ∀ (a : α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)

Tactic:
⟨fun h _ ↦ h ▸ rfl, ext_of_singleton⟩

Premises used: MeasureTheory.Measure.ext_of_singleton, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ1 μ2 : Measure α
inst_2 : SigmaFinite μ1
inst_3 : SigmaFinite μ2
rw :
  (∀ (a : α), Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)) ↔
    ∀ (x : α), μ1.real {x} = μ2.real {x}
⊢ μ1 = μ2 ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}

Tactic:
rw [Measure.ext_iff_singleton]

Premises used: MeasureTheory.Measure.ext_iff_singleton
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ1 μ2 : Measure α
inst_2 : SigmaFinite μ1
inst_3 : SigmaFinite μ2
a :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ↔
      μ1.real {x} = μ2.real {x}
⊢ (∀ (a : α), Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)) ↔
    ∀ (x : α), μ1.real {x} = μ2.real {x}

Tactic:
congr! with x
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ1 μ2 : Measure α
inst_2 : SigmaFinite μ1
inst_3 : SigmaFinite μ2
x : α
a :
  Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Eq (α := ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          Eq (α := ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ↔
    μ1.real {x} = μ2.real {x}

Tactic:
rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff]

Premises used: ENNReal.toReal_eq_toReal_iff, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ1 μ2 : Measure α
inst_2 : SigmaFinite μ1
inst_3 : SigmaFinite μ2
x : α
⊢ Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Eq (α := ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          Eq (α := ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [measure_singleton_lt_top, ne_of_lt]

Premises used: MeasureTheory.measure_singleton_lt_top, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Countable β
inst_3 : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
h :
  ∀ (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((sum fun (b : β) ↦
                  HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {b}) : ℝ≥0∞) (dirac b) :
                Measure β) :
              (a : Set β) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ Eq (α := Measure β) (map f μ)
    (sum fun (b : β) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {b}) : ℝ≥0∞) (dirac b))

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Countable β
inst_3 : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
h : MeasurableSet s
⊢ ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})

Tactic:
have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _)
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Countable β
inst_3 : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
h : MeasurableSet s
this : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (b : β) ↦
              HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {b}) : ℝ≥0∞) (dirac b) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
    tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})]

Premises used: tsum_subtype, Set.preimage, MeasureTheory.tsum_measure_preimage_singleton, Set.to_countable, Singleton.singleton, Set.indicator_mul_right, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
μ : Measure α
⊢ (sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)) = μ

Tactic:
simpa using (map_eq_sum μ id measurable_id).symm

Premises used: measurable_id, MeasureTheory.Measure.map_eq_sum, id, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ((sum fun (b : α) ↦ HSMul.hSMul (β := Measure α) (f b) (dirac b) : Measure α) : (a : Set α) → ℝ≥0∞) {a} = f a

Tactic:
simp +contextual [tsum_eq_single a]

Premises used: tsum_eq_single
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : (↑measurableAtoms : Type u_1)
obtain : ∀ (y : α), Membership.mem (γ := Set α) univ y → ∀ (hy : measurableAtom y = (↑s : Set α)), (↑s : Set α).Nonempty
⊢ (↑s : Set α).Nonempty

Tactic:
obtain ⟨y, _, hy⟩ := s.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : (↑measurableAtoms : Type u_1)
y : α
left : Membership.mem (γ := Set α) univ y
hy : measurableAtom y = (↑s : Set α)
rw : (measurableAtom y).Nonempty
⊢ (↑s : Set α).Nonempty

Tactic:
rw [← hy]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : (↑measurableAtoms : Type u_1)
y : α
left : Membership.mem (γ := Set α) univ y
hy : measurableAtom y = (↑s : Set α)
⊢ (measurableAtom y).Nonempty

Tactic:
⟨y, mem_measurableAtom_self y⟩

Premises used: mem_measurableAtom_self, Set.Nonempty, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : (↑measurableAtoms : Type u_1)
y : α
left : Membership.mem (γ := Set α) univ y
hy : measurableAtom y = (↑s : Set α)
⊢ (measurableAtom y).Nonempty

Tactic:
exact ⟨y, mem_measurableAtom_self y⟩
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
⊢ ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty

Tactic:
have h_nonempty (s : measurableAtoms) : Set.Nonempty s.1 := by
    obtain ⟨y, _, hy⟩ := s.2
    rw [← hy]
    exact ⟨y, mem_measurableAtom_self y⟩
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
⊢ ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)

Tactic:
have h_points_mem (s : measurableAtoms) : points s ∈ s.1 := (h_nonempty s).some_mem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
⊢ ∃ (s : Set α),
    μ =
      sum fun (x : (↑s : Type u_1)) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
          (dirac (↑x : α))

Tactic:
⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩

Premises used: MeasureTheory.ext_of_measurableAtoms, Exists.intro, Set.range
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
refine :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      (((sum fun (x : (↑(range points) : Type u_1)) ↦
                HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
                  (dirac (↑x : α)) :
              Measure α) :
            (a : Set α) → ℝ≥0∞)
          (measurableAtom x) :
        ℝ≥0∞)
⊢ ∃ (s : Set α),
    μ =
      sum fun (x : (↑s : Type u_1)) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
          (dirac (↑x : α))

Tactic:
refine ⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
x : α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    (∑' (i : (↑(range points) : Type u_1)),
        (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑i : α)) : ℝ≥0∞)
              (dirac (↑i : α)) :
            (a : Set α) → ℝ≥0∞)
          (measurableAtom x) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    (((sum fun (x : (↑(range points) : Type u_1)) ↦
              HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
                (dirac (↑x : α)) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        (measurableAtom x) :
      ℝ≥0∞)

Tactic:
rw [sum_apply _ (MeasurableSet.measurableAtom_of_countable x)]

Premises used: MeasureTheory.Measure.sum_apply, MeasurableSet.measurableAtom_of_countable
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
x : α
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    (∑' (i : (↑(range points) : Type u_1)),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑i : α)) : ℝ≥0∞)
          (((dirac (↑i : α) : Measure α) : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    (∑' (i : (↑(range points) : Type u_1)),
        (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑i : α)) : ℝ≥0∞)
              (dirac (↑i : α)) :
            (a : Set α) → ℝ≥0∞)
          (measurableAtom x) :
      ℝ≥0∞)

Tactic:
simp only [Measure.smul_apply, smul_eq_mul]

Premises used: MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
x : α
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    (∑' (i : (↑(range points) : Type u_1)),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑i : α)) : ℝ≥0∞)
          ((measurableAtom x).indicator 1 (↑i : α) : ℝ≥0∞) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    (∑' (i : (↑(range points) : Type u_1)),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑i : α)) : ℝ≥0∞)
          (((dirac (↑i : α) : Measure α) : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
simp_rw [dirac_apply' _ (MeasurableSet.measurableAtom_of_countable x)]

Premises used: MeasureTheory.Measure.dirac_apply', MeasurableSet.measurableAtom_of_countable
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
x : α
⊢ measurableAtom x ∈ measurableAtoms

Tactic:
simp [measurableAtoms]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : (↑measurableAtoms : Type u_1)), (↑s : Set α).Nonempty
points : (↑measurableAtoms : Type u_1) → α := fun (s : (↑measurableAtoms : Type u_1)) ↦ ⋯.some (s := (↑s : Set α))
h_points_mem : ∀ (s : (↑measurableAtoms : Type u_1)), points s ∈ (↑s : Set α)
x : α
⊢ points (Subtype.mk (p := fun (x : Set α) ↦ x ∈ measurableAtoms) (measurableAtom x) ⋯) ∈ range points

Tactic:
simp