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 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
pos : Eq (α := ℝ≥0∞) 1 (s.indicator 1 a)
pos₁ : Eq (α := ℝ≥0∞) 1 (1 a)
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
have pos₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
have neg : LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [indicator_of_notMem h, ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have dirac : Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) {a}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: calc
    dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
    _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
⊢ map (fun (x : α) ↦ c) μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (dirac c)
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (dirac c) : (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (dirac c) : (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
Tactic: simp only [Measure.coe_smul, Pi.smul_apply,
    dirac_apply' _ hs, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have h : (μ : (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 [Measure.map_apply measurable_const hs, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have 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∞)
Tactic: by_cases hsc : c ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have 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∞)
Tactic: by_cases hsc : c ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
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∞)
have pos : (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have pos₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have pos₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
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∞)
have neg : (μ : (a : Set α) → ℝ≥0∞) ∅ =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have neg₁ : (μ : (a : Set α) → ℝ≥0∞) ∅ = HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have neg₂ : 0 = HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have neg₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have h : (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c) ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have h₁ : (μ : (a : Set α) → ℝ≥0∞) (if c ∈ s then univ else ∅) =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
⊢ μ.restrict {a} = HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a)
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
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∞)
have 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∞)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
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∞)
have this : s ∩ {a} = {a}
Tactic: have : s ∩ {a} = {a} := by simpa
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
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∞)
have this : s ∩ {a} = ∅
Tactic: have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ1 μ2 : Measure α
inst_2 : SigmaFinite μ1
inst_3 : SigmaFinite μ2
⊢ μ1 = μ2 ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}
have rw : (∀ (a : α), Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)) ↔
  ∀ (x : α), μ1.real {x} = μ2.real {x}
Tactic: rw [Measure.ext_iff_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ1 μ2 : Measure α
inst_2 : SigmaFinite μ1
inst_3 : SigmaFinite μ2
⊢ (∀ (a : α), Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)) ↔
    ∀ (x : α), μ1.real {x} = μ2.real {x}
have a : ∀ (x : α),
  Eq (α := ℝ≥0∞) ((μ1 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ2 : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ↔
    μ1.real {x} = μ2.real {x}
Tactic: congr! with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞) ↔
    μ1.real {x} = μ2.real {x}
have 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∞)
Tactic: rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Countable β
inst_3 : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ Eq (α := Measure β) (map f μ)
    (sum fun (b : β) ↦ HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {b}) : ℝ≥0∞) (dirac b))
have 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∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
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
⊢ 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∞)
have this : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
Tactic: have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : (↑measurableAtoms : Type u_1)
⊢ (↑s : Set α).Nonempty
have obtain : ∀ (y : α), Membership.mem (γ := Set α) univ y → ∀ (hy : measurableAtom y = (↑s : Set α)), (↑s : Set α).Nonempty
Tactic: obtain ⟨y, _, hy⟩ := s.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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 α)
⊢ (↑s : Set α).Nonempty
have rw : (measurableAtom y).Nonempty
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
⊢ ∃ (s : Set α),
    μ =
      sum fun (x : (↑s : Type u_1)) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
          (dirac (↑x : α))
have h_nonempty : ∀ (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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
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 : Set α),
    μ =
      sum fun (x : (↑s : Type u_1)) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
          (dirac (↑x : α))
have h_points_mem : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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 : α))
have 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∞)
Tactic: refine ⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩