awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x_in_A : x ∈ A
⊢ Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
simp only [Measure.dirac_apply' _ A_mble, x_in_A, indicator_of_mem, Pi.one_apply,
                 (h A A_mble).mp x_in_A]

Premises used: Pi.one_apply, MeasureTheory.Measure.dirac_apply', Set.indicator_of_mem, Iff.mp
-- 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
x_in_A : x ∉ A
⊢ y ∉ A

Tactic:
simp_all only [not_false_eq_true]

Premises used: not_false_eq_true
-- 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
x_in_A : x ∉ A
⊢ y ∉ A

Tactic:
have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true]
-- 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
x_in_A : x ∉ A
y_notin_A : y ∉ A
⊢ Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A,
                 not_false_eq_true, indicator_of_notMem]

Premises used: MeasureTheory.Measure.dirac_apply', Set.indicator_of_notMem, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
apply : ¬Ne (α := Measure α) (dirac x) (dirac y) ↔ ¬∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A
⊢ Ne (α := Measure α) (dirac x) (dirac y) ↔ ∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Tactic:
apply not_iff_not.mp

Premises used: not_iff_not, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
simp : (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
⊢ ¬Ne (α := Measure α) (dirac x) (dirac y) ↔ ¬∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Tactic:
simp only [ne_eq, not_not, not_exists, not_and, dirac_eq_dirac_iff_forall_mem_iff_mem]

Premises used: Classical.not_not, not_exists, ne_eq, MeasureTheory.dirac_eq_dirac_iff_forall_mem_iff_mem, not_and
-- 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
⊢ x ∈ A → y ∈ A

Tactic:
simp only [h A A_mble, imp_self]

Premises used: imp_self
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
refine :
  ∀ (h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1) (A : Set α) (A_mble : MeasurableSet A), x ∈ A ↔ y ∈ A
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1

Tactic:
refine ⟨fun h A A_mble ↦ by simp only [h A A_mble, imp_self], fun h A A_mble ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
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 : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simp only [x_in_A, h A A_mble x_in_A]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, false_iff] using h Aᶜ (MeasurableSet.compl_iff.mpr A_mble) x_in_A

Premises used: Iff.mpr, Compl.compl, MeasurableSet.compl_iff, false_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
obtain :
  ∀ (A : Set α) (A_mble : MeasurableSet A) (x_in_A : x ∈ A) (y_notin_A : y ∉ A), Ne (α := Measure α) (dirac x) (dirac y)
⊢ Ne (α := Measure α) (dirac x) (dirac y)

Tactic:
obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y

Premises used: MeasurableSpace.exists_measurableSet_of_ne
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
y_notin_A : y ∉ A
⊢ Ne (α := Measure α) (dirac x) (dirac y)

Tactic:
dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.dirac_ne_dirac_iff_exists_measurableSet, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
y_notin_A : y ∉ A
⊢ Ne (α := Measure α) (dirac x) (dirac y)

Tactic:
exact dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.dirac_ne_dirac_iff_exists_measurableSet, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
⊢ Ne (α := Measure α) (dirac x) (dirac y) ↔ x ≠ y

Tactic:
⟨fun h x_eq_y ↦ h <| congrArg dirac x_eq_y, fun h ↦ dirac_ne_dirac h⟩

Premises used: congrArg, MeasureTheory.dirac_ne_dirac, MeasureTheory.Measure.dirac, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
⊢ Eq (α := Measure α) (dirac x) (dirac y) ↔ x = y

Tactic:
not_iff_not.mp dirac_ne_dirac_iff

Premises used: not_iff_not, MeasureTheory.dirac_ne_dirac_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y :
  Eq.{u_1 + 1} (α := Measure α) ((fun (x : α) ↦ (dirac x : Measure α)) x) ((fun (x : α) ↦ (dirac x : Measure α)) y)
rwa rwa₁ rwa₂ rwa₃ : Eq (α := Measure α) (dirac x) (dirac y)
⊢ x = y

Tactic:
rwa [← dirac_eq_dirac_iff]

Premises used: MeasureTheory.dirac_eq_dirac_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
h :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) :
              Measure α) :
            (a : Set α) → ℝ≥0∞)
          t :
        ℝ≥0∞)
⊢ μ = ∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)

Tactic:
ext t ht
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ {x : α | (fun (a : α) ↦ a ∈ s) x}ᶜ) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
rw [← measure_diff_null (s := t) hμ]

Premises used: MeasureTheory.measure_diff_null
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ (↑s : Set α)ᶜ) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ {x : α | (fun (a : α) ↦ a ∈ s) x}ᶜ) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ x ∈ (↑s : Set α), {x}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ (↑s : Set α)ᶜ) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
rw [Set.diff_compl, ← (s : Set α).biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton, SetLike.coe, Set.diff_compl
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, t ∩ {i}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ x ∈ (↑s : Set α), {x}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
simp_rw [Finset.mem_coe, Set.inter_iUnion]

Premises used: Set.inter_iUnion, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ ∀ b ∈ s, MeasurableSet (t ∩ {b})

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t ∩ {p}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
rw : ∀ (i : α) (hi : i ∈ (↑s : Set α)) (j : α) (hj : j ∈ (↑s : Set α)) (hij : i ≠ j), Disjoint (α := Set α) {i} {j}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, t ∩ {i}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_)
      (by measurability)]

Premises used: Disjoint.inter_left', MeasureTheory.measure_biUnion_finset, Disjoint.inter_right'
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t ∩ {p}))
    (∑ x ∈ s,
      HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
        (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t ∩ {p}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
simp only [coe_finsetSum, Finset.sum_apply, smul_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  ∀ (a : α),
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
      HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
        (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t ∩ {p}))
    (∑ x ∈ s,
      HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
        (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))

Tactic:
congr with a
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
pos :
  ∀ (ha : a ∈ t),
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
      HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
        (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
neg :
  ∀ (ha : a ∉ t),
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
      HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
        (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
      (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
by_cases ha : a ∈ t
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∈ t
⊢ (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
      (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∉ t
⊢ (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
      (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
i : α
hi : i ∈ (↑s : Set α)
j : α
hj : j ∈ (↑s : Set α)
hij : i ≠ j
⊢ Disjoint (α := Set α) {i} {j}

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (↑s : Set α)) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
h₁ h₂ h₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ x ∈ (↑s : Set α), {x}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
h₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, t ∩ {i}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
h₅ :
  Eq (α := ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t ∩ {p}) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
rw rw₁ : ∀ (i : α) (hi : i ∈ (↑s : Set α)) (j : α) (hj : j ∈ (↑s : Set α)) (hij : i ≠ j), Disjoint (α := Set α) {i} {j}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ (↑s : Set α)ᶜ) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
classical
    rw [Set.diff_compl, ← (s : Set α).biUnion_of_singleton]
    simp_rw [Finset.mem_coe, Set.inter_iUnion]
    rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_)
      (by measurability)]
    · simp only [coe_finsetSum, Finset.sum_apply, smul_apply]
      congr with a
      by_cases ha : a ∈ t <;> simp [*]
    simpa

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply, Set.biUnion_of_singleton, Disjoint.inter_left', SetLike.coe, MeasureTheory.measure_biUnion_finset, MeasureTheory.Measure.smul_apply, Set.inter_iUnion, Disjoint.inter_right', Finset.mem_coe, Set.diff_compl
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
rw :
  ∀ i ∈ s, ∀ᵐ (x : α) ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i), x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s

Tactic:
rw [hμ, ae_finsetSum_measure_iff]

Premises used: MeasureTheory.ae_finsetSum_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
i : α
hi : i ∈ s
⊢ ∀ᵐ (x : α) ∂dirac i, x ∈ s

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
⊢ ∀ i ∈ s, ∀ᵐ (x : α) ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i), x ∈ s

Tactic:
exact fun i hi ↦ ae_smul_measure (by simpa) _

Premises used: MeasureTheory.Measure.ae_smul_measure
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ a₁ ∉ {a₂}

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
h : ∀ (x : α), x = a₁ ∨ x = a₂ ↔ x ∈ Finset.cons a₁ {a₂} ⋯
h₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a₁} : ℝ≥0∞) (dirac a₁) +
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a₂} : ℝ≥0∞) (dirac a₂) =
    ∑ a ∈ Finset.cons a₁ {a₂} ⋯,
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
⊢ (∀ᵐ (a : α) ∂μ, a = a₁ ∨ a = a₂) ↔
    μ =
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a₁} : ℝ≥0∞) (dirac a₁) +
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a₂} : ℝ≥0∞) (dirac a₂)

Tactic:
convert! ae_mem_finset_iff (s := .cons a₁ { a₂ } <| by simpa)

Premises used: MeasureTheory.Measure.ae_mem_finset_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
x : α
⊢ x = a₁ ∨ x = a₂ ↔ x ∈ Finset.cons a₁ {a₂} ⋯

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a₁} : ℝ≥0∞) (dirac a₁) +
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a₂} : ℝ≥0∞) (dirac a₂) =
    ∑ a ∈ Finset.cons a₁ {a₂} ⋯,
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ MeasurableSet.{u_4} (α := α) {x : α | x ∈ s}

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
rw :
  Eq (α := Measure α) (map f μ)
      (∑ a ∈ s,
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) (((map f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)) ↔
    Eq (α := Measure α) (map f μ)
      (∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (dirac a))
⊢ (∀ᵐ (b : β) ∂μ, f b ∈ s) ↔
    Eq (α := Measure α) (map f μ)
      (∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (dirac a))

Tactic:
rw [← ae_map_iff hf (by measurability), ae_mem_finset_iff]

Premises used: MeasureTheory.Measure.ae_mem_finset_iff, MeasureTheory.ae_map_iff
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ Eq (α := Measure α) (map f μ)
      (∑ a ∈ s,
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) (((map f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)) ↔
    Eq (α := Measure α) (map f μ)
      (∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (dirac a))

Tactic:
simp [map_apply₀ hf]

Premises used: MeasureTheory.Measure.map_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
⊢ a₁ ∉ {a₂}

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
h : ∀ (x : β), f x = a₁ ∨ f x = a₂ ↔ f x ∈ Finset.cons a₁ {a₂} ⋯
h₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a₁}) : ℝ≥0∞) (dirac a₁) +
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a₂}) : ℝ≥0∞) (dirac a₂) =
    ∑ a ∈ Finset.cons a₁ {a₂} ⋯,
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (dirac a)
⊢ (∀ᵐ (b : β) ∂μ, f b = a₁ ∨ f b = a₂) ↔
    map f μ =
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a₁}) : ℝ≥0∞) (dirac a₁) +
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a₂}) : ℝ≥0∞) (dirac a₂)

Tactic:
convert! ae_mem_finset_iff_map_eq_sum_dirac (s := .cons a₁ { a₂ } <| by simpa) hf

Premises used: MeasureTheory.Measure.ae_mem_finset_iff_map_eq_sum_dirac
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
x : β
⊢ f x = a₁ ∨ f x = a₂ ↔ f x ∈ Finset.cons a₁ {a₂} ⋯

Tactic:
simp