awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
⊢ Ne (α := Measure α) (dirac x) (dirac y)
have obtain : ∀ (A : Set α) (A_mble : MeasurableSet A) (x_in_A : x ∈ A) (y_notin_A : y ∉ A), Ne (α := Measure α) (dirac x) (dirac y)
Tactic: obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
⊢ μ = ∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
have 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∞)
Tactic: ext t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
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∞)
have 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∞)
Tactic: rw [← measure_diff_null (s := t) hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
Tactic: rw [Set.diff_compl, ← (s : Set α).biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
Tactic: simp_rw [Finset.mem_coe, Set.inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
Tactic: rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_)
      (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ 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∞)
have rw : ∀ (i : α) (hi : i ∈ (↑s : Set α)) (j : α) (hj : j ∈ (↑s : Set α)) (hij : i ≠ j), Disjoint (α := Set α) {i} {j}
Tactic: rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_)
      (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞)
have 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∞))
Tactic: simp only [coe_finsetSum, Finset.sum_apply, smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞))
have h : ∀ (a : α),
  (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
      (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
⊢ (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
      (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have 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∞)
Tactic: by_cases ha : a ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (t ∩ {a}) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
      (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have 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∞)
Tactic: by_cases ha : a ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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 \ (↑s : Set α)ᶜ) : ℝ≥0∞)
    (((∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) : Measure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ 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∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ 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∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ 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∞)
have rw : ∀ (i : α) (hi : i ∈ (↑s : Set α)) (j : α) (hj : j ∈ (↑s : Set α)) (hij : i ≠ j), Disjoint (α := Set α) {i} {j}
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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)
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s
have rw : ∀ i ∈ s, ∀ᵐ (x : α) ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i), x ∈ s
Tactic: rw [hμ, ae_finsetSum_measure_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ 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₂)
have h : ∀ (x : α), x = a₁ ∨ x = a₂ ↔ x ∈ Finset.cons a₁ {a₂} sorry
Tactic: convert! ae_mem_finset_iff (s := .cons a₁ { a₂ } <| by simpa)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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₂} ⋯
⊢ (∀ᵐ (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₂)
have 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₂} sorry, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
Tactic: convert! ae_mem_finset_iff (s := .cons a₁ { a₂ } <| by simpa)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ (∀ᵐ (b : β) ∂μ, f b ∈ s) ↔
    Eq (α := Measure α) (map f μ)
      (∑ a ∈ s, HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set β) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (dirac a))
have 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))
Tactic: rw [← ae_map_iff hf (by measurability), ae_mem_finset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ 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₂)
have h : ∀ (x : β), f x = a₁ ∨ f x = a₂ ↔ f x ∈ Finset.cons a₁ {a₂} sorry
Tactic: convert! ae_mem_finset_iff_map_eq_sum_dirac (s := .cons a₁ { a₂ } <| by simpa) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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₂} ⋯
⊢ (∀ᵐ (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₂)
have 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₂} sorry,
    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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
⊢ ∃ (f : X →ᵇ ℝ≥0),
    Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ∧
      ∀ y ∈ K, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
have obtain : ∀ (g : X → (↑unitInterval : Type)) (g_cont : Continuous[inst, _] g) (gx_zero : g x = 0) (g_one_on_K : EqOn g 1 K),
  ∃ (f : X →ᵇ ℝ≥0),
    Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ∧
      ∀ y ∈ K, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
Tactic: obtain ⟨g, g_cont, gx_zero, g_one_on_K⟩ :=
    CompletelyRegularSpace.completely_regular x K K_closed x_notin_K
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1
have refine : ∀ (x y : X), (↑1 : ℝ) * dist (↑(g x) : ℝ) (↑(g y) : ℝ) ≤ 1
Tactic: refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst] K
x : X
x_notin_K : x ∉ K
g : X → (↑unitInterval : Type)
g_cont : Continuous[inst, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∃ (f : X →ᵇ ℝ≥0),
    Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ∧
      ∀ y ∈ K, Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) y : ℝ≥0) (0 : ℝ≥0)
have g_bdd : ∀ (x y : X), dist (↑(g x) : ℝ).toNNReal (↑(g y) : ℝ).toNNReal ≤ 1
Tactic: have g_bdd : ∀ x y, dist (Real.toNNReal (g x)) (Real.toNNReal (g y)) ≤ 1 := by
    refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_
    simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_2
inst : MeasurableSpace X
inst_1 : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y :
  Eq.{u_2 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) y)
⊢ x = y
have rw : Eq (α := Measure X) (Measure.dirac x) (Measure.dirac y)
Tactic: rw [← dirac_eq_dirac_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.DiracProba (goal)
Goal:
X : Type u_2
inst : MeasurableSpace X
inst_1 : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y :
  Eq.{u_2 + 1} (α := ProbabilityMeasure X) ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x)
    ((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) y)
⊢ Eq (α := Measure X) (Measure.dirac x) (Measure.dirac y)
have rwa : ∀
  (x_eq_y :
    Eq.{u_2 + 1} (α := Measure X) (↑((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) x) : Measure X)
      (↑((fun (x : X) ↦ (diracProba x : ProbabilityMeasure X)) y) : Measure X)),
  Eq (α := Measure X) (Measure.dirac x) (Measure.dirac y)
Tactic: rwa [Subtype.ext_iff] at x_eq_y
Cleared hypotheses: x_eq_y