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 : 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 α))
x y : α
s : Set α
hyx : ¬y = points (Subtype.mk (p := fun (x : Set α) ↦ x ∈ measurableAtoms) (measurableAtom x) ⋯)
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left : Membership.mem (γ := Set α) univ z
hz : measurableAtom z = s
hsy : points (Subtype.mk (p := fun (a : Set α) ↦ a ∈ measurableAtoms) s ⋯) = y
h_points_mem : points (Subtype.mk (p := fun (x : Set α) ↦ x ∈ measurableAtoms) s ⋯) ∈ s
⊢ measurableAtom (points (Subtype.mk (p := fun (a : Set α) ↦ a ∈ measurableAtoms) s ⋯)) = measurableAtom z
have refine : points (Subtype.mk (p := fun (a : Set α) ↦ a ∈ measurableAtoms) s sorry) ∈ measurableAtom z
Tactic: refine measurableAtom_eq_of_mem ?_
-- 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 α))
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
⊢ s = measurableAtom x
have h2 : 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
-- 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 α)
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
⊢ s = measurableAtom x
have e_a₁ : measurableAtom x = measurableAtom x
Tactic: rw [← h2, h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [μ.sum_smul_dirac]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), s.indicator (fun (x : α) ↦ (μ : (a : Set α) → ℝ≥0∞) {x}) x : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s
have pos : a ∈ s → (s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s)
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
pos : a ∈ s → (s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s)
⊢ s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s
have neg : a ∉ s → (s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s)
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
⊢ ae (F := Measure α) (dirac a) = pure a
have h : ∀ (s : Set α), s ∈ ae (F := Measure α) (dirac a) ↔ Membership.mem (γ := Filter α) (pure a) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
⊢ Eq (α := Measure β) (map f (dirac a)) (dirac (f a))
have 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∞)
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 β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
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∞)
have h : Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable (by fun_prop) hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : α → β
a : α
⊢ Eq (α := Measure β) (map f (dirac a)) (dirac (f a))
have 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∞)
Tactic: classical
  ext s hs
  rw [map_apply_of_aemeasurable (by fun_prop) hs]
  simp [indicator_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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))
have 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∞)
Tactic: classical
  ext s hs
  rw [map_apply_of_aemeasurable (by fun_prop) hs]
  simp [indicator_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔ a ∈ s
have rw : s ∈ ae (F := Measure α) (dirac a) ↔ a ∈ s
Tactic: rw [← prob_compl_eq_zero_iff hs, ← mem_ae_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s
have rw : sᶜ ∈ ae (F := Measure α) (dirac a) ↔ a ∈ sᶜ
Tactic: rw [← compl_compl s, ← mem_ae_iff, notMem_compl_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (if a ∈ s then dirac a else 0)
have pos : ∀ (has : a ∈ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)
Tactic: split_ifs with has
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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)
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (if a ∈ s then dirac a else 0)
have neg : ∀ (has : a ∉ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
Tactic: split_ifs with has
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has : a ∈ s
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)
have pos : ∀ᵐ (x : α) ∂dirac a, x ∈ s
Tactic: apply restrict_eq_self_of_ae_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has pos : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
have pos₁ : MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}
Tactic: rw [ae_dirac_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst_1 : Decidable (a ∈ s)
has : a ∉ s
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
have neg : Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
have neg₁ : Eq (α := ℝ≥0∞) (s.indicator 1 a) 0
Tactic: rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
have neg₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (if a ∈ s then dirac a else 0)
have pos : ∀ (has : a ∈ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)
Tactic: split_ifs with has
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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)
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (if a ∈ s then dirac a else 0)
have neg : ∀ (has : a ∉ s), Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
Tactic: split_ifs with has
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
has : a ∈ s
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) (dirac a)
have pos : ∀ᵐ (x : α) ∂dirac a, x ∈ s
Tactic: apply restrict_eq_self_of_ae_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
have pos : ∀ᶠ (x : α) in pure a, x ∈ s
Tactic: rwa [ae_dirac_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
inst_1 : MeasurableSingletonClass α
inst_2 : Decidable (a ∈ s)
has : a ∉ s
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
have neg : Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
have neg₁ : Eq (α := ℝ≥0∞) (s.indicator 1 a) 0
Tactic: rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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
⊢ Eq (α := Measure α) (Measure.restrict (dirac a) s) 0
have neg₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
⊢ Eq (α := Measure α) (dirac x) (dirac y) ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
have mp : Eq (α := Measure α) (dirac x) (dirac y) → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
mp : Eq (α := Measure α) (dirac x) (dirac y) → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
⊢ Eq (α := Measure α) (dirac x) (dirac y) ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
have mpr : (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → Eq (α := Measure α) (dirac x) (dirac y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : Eq (α := Measure α) (dirac x) (dirac y)
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A
have obs : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
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))
⊢ x ∈ A ↔ y ∈ A
have obs₁ : Eq (α := ℝ≥0∞) (A.indicator 1 x) (A.indicator 1 y)
Tactic: simp only [Measure.dirac_apply' _ A_mble] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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 ∈ A ↔ y ∈ A
have pos : ∀ (x_in_A : x ∈ A), x ∈ A ↔ y ∈ A
Tactic: by_cases x_in_A : x ∈ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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
⊢ x ∈ A ↔ y ∈ A
have neg : ∀ (x_in_A : x ∉ A), x ∈ A ↔ y ∈ A
Tactic: by_cases x_in_A : x ∈ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
⊢ Eq (α := Measure α) (dirac x) (dirac y)
have 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∞)
Tactic: ext A A_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have pos : ∀ (x_in_A : x ∈ A),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((dirac x : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((dirac y : Measure α) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have neg : ∀ (x_in_A : x ∉ A),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
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∞)
have y_notin_A : y ∉ A
Tactic: have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
⊢ Ne (α := Measure α) (dirac x) (dirac y) ↔ ∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A
have apply : ¬Ne (α := Measure α) (dirac x) (dirac y) ↔ ¬∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A
Tactic: apply not_iff_not.mp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
⊢ ¬Ne (α := Measure α) (dirac x) (dirac y) ↔ ¬∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A
have simp : (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
Tactic: simp only [ne_eq, not_not, not_exists, not_and, dirac_eq_dirac_iff_forall_mem_iff_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
have refine : ∀ (h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1) (A : Set α) (A_mble : MeasurableSet A), x ∈ A ↔ y ∈ A
Tactic: refine ⟨fun h A A_mble ↦ by simp only [h A A_mble, imp_self], fun h A A_mble ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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 ∈ A ↔ y ∈ A
have pos : ∀ (x_in_A : x ∈ A), x ∈ A ↔ y ∈ A
Tactic: by_cases x_in_A : x ∈ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
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
⊢ x ∈ A ↔ y ∈ A
have neg : ∀ (x_in_A : x ∉ A), x ∈ A ↔ y ∈ A
Tactic: by_cases x_in_A : x ∈ A