awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 y : α
s : Set α
hs : s ∈ measurableAtoms
hsy : points (Subtype.mk (p := fun (a : Set α) ↦ a ∈ measurableAtoms) s hs) = y
hyx : ¬y = points (Subtype.mk (p := fun (x : Set α) ↦ x ∈ measurableAtoms) (measurableAtom x) ⋯)
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
⊢ measurableAtom y = s

Tactic:
have h2 : measurableAtom y = s := by
      specialize h_points_mem ⟨s, hs⟩
      obtain ⟨z, _, hz⟩ := hs
      simp only at h_points_mem
      rw [← hz, ← hsy]
      refine measurableAtom_eq_of_mem ?_
      convert! h_points_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 α)
x y : α
s : Set α
hs : s ∈ measurableAtoms
hsy : points (Subtype.mk (p := fun (a : Set α) ↦ a ∈ measurableAtoms) s hs) = y
hyx : ¬y = points (Subtype.mk (p := fun (x : Set α) ↦ x ∈ measurableAtoms) (measurableAtom x) ⋯)
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
h2 : measurableAtom y = s
e_a : measurableAtom y = measurableAtom x
e_a₁ e_a₂ : measurableAtom x = measurableAtom x
⊢ s = measurableAtom x

Tactic:
rw [← h2, h1]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    (((sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
        Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]

Premises used: Set.indicator_apply, Pi.one_apply, mul_ite, MeasureTheory.Measure.sum_apply, MulZeroClass.mul_zero, MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.dirac_apply, smul_eq_mul, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [μ.sum_smul_dirac]

Premises used: MeasureTheory.Measure.sum_smul_dirac
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
x :
  Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    (((sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
x₁ :
  Eq (α := ℝ≥0∞)
    (((sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    (∑' x : α, s.indicator (fun x => μ {x}) x) =
      Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
      simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
        Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]
    _ = μ s := by rw [μ.sum_smul_dirac]

Premises used: Set.indicator, MeasureTheory.Measure.dirac, tsum, HSMul.hSMul, MeasureTheory.Measure.sum, Singleton.singleton, DFunLike.coe, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
x :
  Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    (((sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
x₁ :
  Eq (α := ℝ≥0∞)
    (((sum fun (a : α) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
classical
  calc
    (∑' x : α, s.indicator (fun x => μ {x}) x) =
      Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
      simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
        Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]
    _ = μ s := by rw [μ.sum_smul_dirac]

Premises used: Set.indicator, MeasureTheory.Measure.dirac, tsum, HSMul.hSMul, MeasureTheory.Measure.sum, Singleton.singleton, DFunLike.coe, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
pos : a ∈ s → (s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s)
neg : a ∉ s → (s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s)
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s

Tactic:
by_cases a ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h : a ∈ s
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s

Tactic:
simp [mem_ae_iff, dirac_apply', hs.compl, *]

Premises used: MeasureTheory.Measure.dirac_apply', MeasurableSet.compl, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h : a ∉ s
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s

Tactic:
simp [mem_ae_iff, dirac_apply', hs.compl, *]

Premises used: MeasureTheory.Measure.dirac_apply', MeasurableSet.compl, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
p : α → Prop
hp : MeasurableSet.{u_1} (α := α) {x : α | p x}
⊢ (∀ᵐ (x : α) ∂dirac a, p x) ↔ p a

Tactic:
mem_ae_dirac_iff hp

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.mem_ae_dirac_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
h : ∀ (s : Set α), s ∈ ae (F := Measure α) (dirac a) ↔ Membership.mem (γ := Filter α) (pure a) s
⊢ ae (F := Measure α) (dirac a) = pure a

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ Membership.mem (γ := Filter α) (pure a) s

Tactic:
simp [mem_ae_iff, imp_false]

Premises used: imp_false, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass β
a : α
f : α → β
hf : Measurable f
⊢ f =ᶠ[ae (F := Measure α) (dirac a)] const α (f a)

Tactic:
(ae_dirac_iff <| show MeasurableSet (f ⁻¹' {f a}) from hf <| measurableSet_singleton _).2 rfl

Premises used: Iff.mpr, MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, Filter.EventuallyEq, MeasureTheory.ae_dirac_iff, Set.singleton, rfl
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
δ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
f : α → δ
⊢ f =ᶠ[ae (F := Measure α) (dirac a)] const α (f a)

Tactic:
simp [Filter.EventuallyEq]

Premises used: Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
a : α
f : α → β
⊢ AEMeasurable (_m := inst) f (dirac a)

Tactic:
⟨fun _ ↦ f a, measurable_const, ae_eq_dirac f⟩

Premises used: AEMeasurable, MeasureTheory.ae_eq_dirac, And.intro, Exists.intro, measurable_const
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map f (dirac a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (map f (dirac a)) (dirac (f a))

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
⊢ AEMeasurable (_m := inst) f (dirac a)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f (dirac a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply_of_aemeasurable (by fun_prop) hs]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [indicator_apply]

Premises used: Set.indicator_apply
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map f (dirac a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (map f (dirac a)) (dirac (f a))

Tactic:
classical
  ext s hs
  rw [map_apply_of_aemeasurable (by fun_prop) hs]
  simp [indicator_apply]

Premises used: Set.indicator_apply
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
a x : α
⊢ IsProbabilityMeasure (m0 := inst) (dirac x)

Tactic:
⟨dirac_apply_of_mem <| mem_univ x⟩

Premises used: MeasureTheory.Measure.dirac_apply_of_mem, Set.mem_univ, MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
δ : Type u_3
ι : Type u_4
mδ : MeasurableSpace δ
c : ι → ℝ≥0∞
d : ι → δ
h : HasSum c 1
⊢ Eq (α := ℝ≥0∞)
    (((sum fun (i : ι) ↦ HSMul.hSMul (β := Measure δ) (c i) (dirac (d i)) : Measure δ) : (a : Set δ) → ℝ≥0∞) univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp [h.tsum_eq]

Premises used: HasSum.tsum_eq
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
δ : Type u_3
ι : Type u_4
mδ : MeasurableSpace δ
c : ι → ℝ≥0
d : ι → δ
h : HasSum c 1
⊢ IsProbabilityMeasure.{u_3} (α := δ) (m0 := mδ) (sum fun (i : ι) ↦ HSMul.hSMul (β := Measure δ) (c i) (dirac (d i)))

Tactic:
(ENNReal.hasSum_coe.2 h).isProbabilityMeasure_sum_dirac_ennreal

Premises used: Iff.mpr, HasSum.isProbabilityMeasure_sum_dirac_ennreal, ENNReal.hasSum_coe
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
δ : Type u_3
ι : Type u_4
mδ : MeasurableSpace δ
c : ι → ℝ
d : ι → δ
h1 : ∀ (i : ι), 0 ≤ c i
h2 : HasSum c 1
⊢ HasSum (α := ℝ≥0) (fun (i : ι) ↦ (c i).toNNReal) 1

Tactic:
simpa using h2.toNNReal h1

Premises used: HasSum.toNNReal
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
a : α
hα : Nonempty α
⊢ Nonempty.{max 1 (u_1 + 1)} { μ : Measure α // IsProbabilityMeasure μ }

Tactic:
⟨Measure.dirac hα.some, inferInstance⟩

Premises used: inferInstance, Nonempty.some, MeasureTheory.Measure.dirac, Nonempty.intro, Subtype.mk
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
a_1 a : α
⊢ IsFiniteMeasure (m0 := inst) (dirac a)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
a_1 a : α
⊢ SigmaFinite (m0 := inst) (dirac a)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
rw : s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔ a ∈ s

Tactic:
rw [← prob_compl_eq_zero_iff hs, ← mem_ae_iff]

Premises used: MeasureTheory.prob_compl_eq_zero_iff, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s

Tactic:
apply mem_ae_dirac_iff hs

Premises used: MeasureTheory.mem_ae_dirac_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
rw : sᶜ ∈ ae (F := Measure α) (dirac a) ↔ a ∈ sᶜ
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s

Tactic:
rw [← compl_compl s, ← mem_ae_iff, notMem_compl_iff]

Premises used: compl_compl, Set.notMem_compl_iff, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ sᶜ ∈ ae (F := Measure α) (dirac a) ↔ a ∈ sᶜ

Tactic:
apply mem_ae_dirac_iff (MeasurableSet.compl_iff.mpr hs)

Premises used: Iff.mpr, MeasurableSet.compl_iff, MeasureTheory.mem_ae_dirac_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
pos : ∀ (has : a ∈ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)
neg : ∀ (has : a ∉ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (if a ∈ s then dirac a else 0)

Tactic:
split_ifs with has
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has : a ∈ s
pos : ∀ᵐ (x : α) ∂dirac a, x ∈ s
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)

Tactic:
apply restrict_eq_self_of_ae_mem

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has pos : a ∈ s
pos₁ : MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s

Tactic:
rw [ae_dirac_iff]

Premises used: MeasureTheory.ae_dirac_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has : a ∈ s
⊢ a ∈ s

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has : a ∈ s
⊢ MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has : a ∉ s
neg : Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg₁ : Eq (α := ℝ≥0∞) (s.indicator 1 a) 0
neg₂ neg₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0

Tactic:
rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has]

Premises used: MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.Measure.dirac_apply', Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
pos : ∀ (has : a ∈ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)
neg : ∀ (has : a ∉ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (if a ∈ s then dirac a else 0)

Tactic:
split_ifs with has
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
has : a ∈ s
pos : ∀ᵐ (x : α) ∂dirac a, x ∈ s
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)

Tactic:
apply restrict_eq_self_of_ae_mem

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
has : a ∈ s
pos pos₁ pos₂ pos₃ : ∀ᶠ (x : α) in pure a, x ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s

Tactic:
rwa [ae_dirac_eq]

Premises used: MeasureTheory.ae_dirac_eq
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
has : a ∉ s
neg : Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg₁ : Eq (α := ℝ≥0∞) (s.indicator 1 a) 0
neg₂ neg₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0

Tactic:
rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]

Premises used: MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.Measure.dirac_apply, Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x : α
μ : Measure α
inst_2 : NoAtoms μ
⊢ Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) {x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x : α
μ : Measure α
inst_2 : NoAtoms μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x}ᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
mp : Eq (α := Measure α) (dirac x) (dirac y) → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
mpr : (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → Eq (α := Measure α) (dirac x) (dirac y)
⊢ Eq (α := Measure α) (dirac x) (dirac y) ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : Eq (α := Measure α) (dirac x) (dirac y)
A : Set α
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((fun (μ : Measure α) ↦ ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)) (dirac x))
    ((fun (μ : Measure α) ↦ ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)) (dirac y))

Tactic:
have obs := congr_arg (fun μ ↦ μ A) h
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : Eq (α := Measure α) (dirac x) (dirac y)
A : Set α
A_mble : MeasurableSet A
obs :
  Eq (α := ℝ≥0∞) ((fun (μ : Measure α) ↦ ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)) (dirac x))
    ((fun (μ : Measure α) ↦ ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)) (dirac y))
⊢ Eq (α := ℝ≥0∞) (A.indicator 1 x) (A.indicator 1 y)

Tactic:
simp only [Measure.dirac_apply' _ A_mble] at obs

Premises used: MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : Eq (α := Measure α) (dirac x) (dirac y)
A : Set α
A_mble : MeasurableSet A
obs : Eq (α := ℝ≥0∞) (A.indicator 1 x) (A.indicator 1 y)
pos : ∀ (x_in_A : x ∈ A), x ∈ A ↔ y ∈ A
neg : ∀ (x_in_A : x ∉ A), x ∈ A ↔ y ∈ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
by_cases x_in_A : x ∈ A
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : Eq (α := Measure α) (dirac x) (dirac y)
A : Set α
A_mble : MeasurableSet A
obs : Eq (α := ℝ≥0∞) (A.indicator 1 x) (A.indicator 1 y)
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)),
                  indicator_eq_one_iff_mem] using obs

Premises used: Pi.one_apply, true_iff, Set.indicator_of_mem, Eq.comm, Set.indicator_eq_one_iff_mem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : Eq (α := Measure α) (dirac x) (dirac y)
A : Set α
A_mble : MeasurableSet A
obs : Eq (α := ℝ≥0∞) (A.indicator 1 x) (A.indicator 1 y)
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, indicator_of_notMem, Eq.comm (a := (0 : ℝ≥0∞)), indicator_apply_eq_zero,
                  false_iff, not_false_eq_true, Pi.one_apply, one_ne_zero, imp_false] using obs

Premises used: imp_false, Pi.one_apply, false_iff, Eq.comm, Set.indicator_of_notMem, one_ne_zero, not_false_eq_true, Set.indicator_apply_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
mpr :
  ∀ (A : Set α) (A_mble : MeasurableSet A),
    Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := Measure α) (dirac x) (dirac y)

Tactic:
ext A A_mble
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
pos :
  ∀ (x_in_A : x ∈ A),
    Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
neg :
  ∀ (x_in_A : x ∉ A),
    Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
by_cases x_in_A : x ∈ A