awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
rw₆ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))
rw₇ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
rw₈ : ν₁ + ν₂ = ν₁.singularPart μ + μ.withDensity (ν₁.rnDeriv μ) + ν₂
rw₉ rw₁₀ : ν₁ + ν₂ = ν₁ + ν₂
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_assoc, MeasureTheory.withDensity_add_left, add_comm, MeasureTheory.Measure.singularPart, HAdd.hAdd, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.singularPart_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

Tactic:
(measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ

Tactic:
((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.add, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ

Tactic:
exact ((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.add, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
h : ν₂ ⟂ₘ μ
h₁ :
  ∀ (x : α) (hx_add : (ν₁ + ν₂).rnDeriv μ x = (ν₁.rnDeriv μ + ν₂.rnDeriv μ) x) (hx_zero : ν₂.rnDeriv μ x = 0 x),
    (ν₁ + ν₂).rnDeriv μ x = ν₁.rnDeriv μ x
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ

Tactic:
filter_upwards [rnDeriv_add' ν₁ ν₂ μ, (rnDeriv_eq_zero ν₂ μ).mpr h] with x hx_add hx_zero

Premises used: Iff.mpr, MeasureTheory.Measure.rnDeriv_add', MeasureTheory.Measure.rnDeriv_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
h : ν₂ ⟂ₘ μ
x : α
hx_add : (ν₁ + ν₂).rnDeriv μ x = (ν₁.rnDeriv μ + ν₂.rnDeriv μ) x
hx_zero : ν₂.rnDeriv μ x = 0 x
⊢ (ν₁ + ν₂).rnDeriv μ x = ν₁.rnDeriv μ x

Tactic:
simp [hx_add, hx_zero]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
⊢ MeasurableSet s

Tactic:
have hs : MeasurableSet s := h.measurableSet_nullSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
rw : 0 + (ν.restrict s - ξ.restrict s) = 0 + ν.restrict s - ξ.restrict s
⊢ μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s

Tactic:
rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]

Premises used: MeasureTheory.Measure.MutuallySingular.restrict_nullSet, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
⊢ 0 + (ν.restrict s - ξ.restrict s) = 0 + ν.restrict s - ξ.restrict s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
⊢ μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s

Tactic:
have h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s := by
    rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
    simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
rw : μ.restrict sᶜ + (ν.restrict sᶜ - 0) = μ.restrict sᶜ + ν.restrict sᶜ - 0
⊢ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ

Tactic:
rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict, MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ.restrict sᶜ + (ν.restrict sᶜ - 0) = μ.restrict sᶜ + ν.restrict sᶜ - 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ

Tactic:
have h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ =
      μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ := by
    rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
    simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
rw : μ + (ν - ξ) = μ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
rw₁ : μ + (ν - ξ) = μ + ((ν - ξ).restrict s + (ν - ξ).restrict sᶜ)
rw₂ rw₃ : μ + (ν - ξ) = μ + (ν - ξ)
⊢ μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ

Tactic:
rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl, add_assoc
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ =
    μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
rw :
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
rw₁ rw₂ :
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
⊢ μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)

Tactic:
rw [h_le_s, h_le_s_compl]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) =
    (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ

Tactic:
simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
rw rw₁ : μ + ν - ξ = μ + ν - ξ
⊢ (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ = μ + ν - ξ

Tactic:
rw [restrict_add_restrict_compl hs]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
calc : μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
calc₁ :
  μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ =
    μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ)
calc₂ :
  μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
calc₃ :
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) =
    (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ
calc₄ : (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ = μ + ν - ξ
⊢ μ + (ν - ξ) = μ + ν - ξ

Tactic:
calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]

Premises used: Compl.compl, HSub.hSub, MeasureTheory.Measure.restrict, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
a_1 a : α
⊢ inst ≤ (OuterMeasure.dirac a).caratheodory

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
⊢ LE.le (α := ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
OuterMeasure.dirac_apply a s ▸ le_toMeasure_apply _ _ _

Premises used: Eq.rec, MeasureTheory.OuterMeasure.dirac_apply, MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)

Tactic:
toMeasure_apply _ _ hs

Premises used: Set.indicator, MeasureTheory.toMeasure_apply, ite
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
rw :
  Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 0 ∨
    Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 1
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← measure_toMeasurable s, dirac_apply' a (measurableSet_toMeasurable ..), indicator]

Premises used: Set.indicator, MeasureTheory.Measure.dirac_apply', MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
simp : a ∉ toMeasurable (dirac a) s ∨ a ∈ toMeasurable (dirac a) s
⊢ Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 0 ∨
    Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 1

Tactic:
simp only [Pi.one_apply, ite_eq_right_iff, one_ne_zero, imp_false, ite_eq_left_iff, zero_ne_one,
    not_not]

Premises used: ite_eq_left_iff, Classical.not_not, imp_false, Pi.one_apply, zero_ne_one, ite_eq_right_iff, one_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
tauto : ¬a ∉ toMeasurable (dirac a) s → a ∈ toMeasurable (dirac a) s
tauto₁ tauto₂ tauto₃ : a ∈ toMeasurable (dirac a) s → a ∈ toMeasurable (dirac a) s
⊢ a ∉ toMeasurable (dirac a) s ∨ a ∈ toMeasurable (dirac a) s

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
⊢ ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1

Tactic:
have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
refine : LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (indicator univ 1 a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
rw :
  LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (indicator univ 1 a : ℝ≥0∞)

Tactic:
rw [← dirac_apply' a MeasurableSet.univ]

Premises used: MeasureTheory.Measure.dirac_apply', MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
⊢ LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
measure_mono (subset_univ s)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
⊢ LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact measure_mono (subset_univ s)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
pos : ∀ (h : a ∈ s), Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
neg : ∀ (h : a ∉ s), Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Dirac
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)
pos₂ pos₃ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)

Tactic:
rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]

Premises used: Pi.one_apply, Set.indicator_of_mem, MeasureTheory.Measure.dirac_apply_of_mem
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
neg : LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)

Tactic:
rw [indicator_of_notMem h, ← nonpos_iff_eq_zero]

Premises used: Set.indicator_of_notMem, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Dirac
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∞)
    (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) {a}ᶜ : ℝ≥0∞)

Tactic:
measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.subset_compl_comm, MeasureTheory.measure_mono, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) {a}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [dirac_apply' _ (measurableSet_singleton _).compl]

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.Measure.dirac_apply', MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
dirac : Eq (α := ℝ≥0∞) (((Measure.dirac a : Measure α) : (a : Set α) → ℝ≥0∞) {a}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((Measure.dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥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]

Premises used: Iff.mpr, Set.singleton_subset_iff, Compl.compl, Set.subset_compl_comm, MeasureTheory.Measure.dirac, MeasureTheory.measure_mono, Iff.mp, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
h : Eq (α := Measure α) (dirac a) 0
⊢ False

Tactic:
simpa [h] using dirac_apply_of_mem (mem_univ a)

Premises used: MeasureTheory.Measure.dirac_apply_of_mem, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Measurable 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∞)

Tactic:
simp [hs, map_apply hf hs, hf hs, indicator_apply]

Premises used: Set.indicator_apply, MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
⊢ Eq (α := Measure β) (map f (dirac a)) (dirac (f a))

Tactic:
exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
⊢ Eq (α := Measure β) (map f (dirac a)) (dirac (f a))

Tactic:
classical
  exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
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∞)
⊢ map (fun (x : α) ↦ c) μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (dirac c)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
h :
  ((map (fun (x : α) ↦ c) μ : Measure β) : (a : Set β) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (s.indicator 1 c : ℝ≥0∞)
⊢ 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:
simp only [Measure.coe_smul, Pi.smul_apply,
    dirac_apply' _ hs, smul_eq_mul]

Premises used: MeasureTheory.Measure.dirac_apply', MeasureTheory.Measure.coe_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Dirac
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
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∞)

Tactic:
rw [Measure.map_apply measurable_const hs, Set.preimage_const]

Premises used: MeasureTheory.Measure.map_apply, Set.preimage_const, measurable_const