awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
pos : ∀ (hf : Integrable f μ), μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
neg : ∀ (hf : ¬Integrable f μ), μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
pos :
  ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i = 0),
    (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
refine VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂

Premises used: MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
pos : Eq (α := ℝ) (∫ (x : α) in i, f x ∂μ) 0
pos₁ : Eq (α := ℝ) (@integral _ _ _ _ m 0 fun (x : α) ↦ f x) 0
pos₂ pos₃ : Eq (α := ℝ) 0 0
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0

Tactic:
rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]

Premises used: MeasureTheory.withDensityᵥ_apply, MeasureTheory.Measure.restrict_zero_set, MeasureTheory.integral_zero_measure
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
neg : VectorMeasure.AbsolutelyContinuous (M := ℝ) 0 μ.toENNRealVectorMeasure
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
rw [withDensityᵥ, dif_neg hf]

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ VectorMeasure.AbsolutelyContinuous (M := ℝ) 0 μ.toENNRealVectorMeasure

Tactic:
VectorMeasure.AbsolutelyContinuous.zero _

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ VectorMeasure.AbsolutelyContinuous (M := ℝ) 0 μ.toENNRealVectorMeasure

Tactic:
exact VectorMeasure.AbsolutelyContinuous.zero _

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
⊢ f =ᶠ[ae μ] g

Tactic:
hf.ae_eq_of_forall_setIntegral_eq f g hg fun i hi _ => ?_

Premises used: MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
refine :
  ∀ (i : Set α) (hi : MeasurableSet i),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
⊢ f =ᶠ[ae μ] g

Tactic:
refine hf.ae_eq_of_forall_setIntegral_eq f g hg fun i hi _ => ?_

Premises used: MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
i : Set α
hi : MeasurableSet i
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (↑(μ.withDensityᵥ f) : Set α → E) i = ∫ (x : α) in i, g x ∂μ
rw₁ : (↑(μ.withDensityᵥ g) : Set α → E) i = ∫ (x : α) in i, g x ∂μ
rw₂ rw₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, g x ∂μ) (∫ (x : α) in i, g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)

Tactic:
rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]

Premises used: MeasureTheory.withDensityᵥ_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
pos : ∀ (hf : Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
neg : ∀ (hf : ¬Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
pos : ∀ (i : Set α) (hi : MeasurableSet i), (↑(μ.withDensityᵥ f) : Set α → E) i = (↑(μ.withDensityᵥ g) : Set α → E) i
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
⊢ (↑(μ.withDensityᵥ f) : Set α → E) i = (↑(μ.withDensityᵥ g) : Set α → E) i

Tactic:
rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]

Premises used: MeasureTheory.withDensityᵥ_apply, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)

Tactic:
integral_congr_ae (ae_restrict_of_ae h)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)

Tactic:
exact integral_congr_ae (ae_restrict_of_ae h)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : Integrable g μ
⊢ False

Tactic:
hf (hg.congr h.symm)

Premises used: MeasureTheory.Integrable.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : Integrable g μ
⊢ False

Tactic:
exact hf (hg.congr h.symm)

Premises used: MeasureTheory.Integrable.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
⊢ ¬Integrable g μ

Tactic:
have hg : ¬Integrable g μ := by intro hg; exact hf (hg.congr h.symm)
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
neg :
  Eq (α := VectorMeasure α E)
    (if hf : Integrable f μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
    (μ.withDensityᵥ g)
neg₁ :
  Eq (α := VectorMeasure α E)
    (if hf : Integrable f μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
    (if hf : Integrable g μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
neg₂ :
  Eq (α := VectorMeasure α E) 0
    (if hf : Integrable g μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
neg₃ neg₄ : Eq (α := VectorMeasure α E) 0 0
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g) ↔ f =ᶠ[ae μ] g

Tactic:
⟨fun hfg => hf.ae_eq_of_withDensityᵥ_eq hg hfg, fun h => WithDensityᵥEq.congr_ae h⟩

Premises used: MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.WithDensityᵥEq.congr_ae, Iff.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ

Tactic:
have hfi := integrable_toReal_of_lintegral_ne_top hfm hf
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
⊢ IsFiniteMeasure (μ.withDensity f)

Tactic:
haveI := isFiniteMeasure_withDensity hf
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) : Set α → ℝ) i = (↑(μ.withDensity f).toSignedMeasure : Set α → ℝ) i
⊢ (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) = (μ.withDensity f).toSignedMeasure

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
h : ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞
⊢ (↑(μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) : Set α → ℝ) i = (↑(μ.withDensity f).toSignedMeasure : Set α → ℝ) i

Tactic:
rw [withDensityᵥ_apply hfi hi, toSignedMeasure_apply_measurable hi, measureReal_def,
    withDensity_apply _ hi, integral_toReal hfm.restrict]

Premises used: AEMeasurable.restrict, MeasureTheory.withDensityᵥ_apply, MeasureTheory.Measure.toSignedMeasure_apply_measurable, MeasureTheory.measureReal_def, MeasureTheory.integral_toReal, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞

Tactic:
ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf ?_)

Premises used: AEMeasurable.restrict, ne_top_of_le_ne_top, MeasureTheory.ae_lt_top'
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
h : ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞

Tactic:
refine ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf ?_)

Premises used: AEMeasurable.restrict, ne_top_of_le_ne_top, MeasureTheory.ae_lt_top'
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
rw : ∫⁻ (x : α) in Set.univ, f x ∂μ
| ∫⁻ (x : α), f x ∂μ

Tactic:
rw [← setLIntegral_univ]

Premises used: MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
h : ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
conv_rhs => rw [← setLIntegral_univ]

Premises used: MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ

Tactic:
lintegral_mono_set (Set.subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.lintegral_mono_set
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ

Tactic:
exact lintegral_mono_set (Set.subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.lintegral_mono_set
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
      (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
              (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
          Set α → ℝ)
        i
⊢ μ.withDensityᵥ f =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
rw : (↑(μ.withDensityᵥ f) : Set α → ℝ) i = ∫ (x : α) in i, f x ∂μ
rw₁ rw₂ : Eq (α := ℝ) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, f x ∂μ)
⊢ (↑(VectorMeasure.trim (μ.withDensityᵥ f) hm) : Set α → ℝ) i = ∫ (x : α) in i, f x ∂μ

Tactic:
rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]

Premises used: MeasureTheory.VectorMeasure.trim_measurableSet_eq, MeasureTheory.withDensityᵥ_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
⊢ VectorMeasure.trim (μ.withDensityᵥ f) hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure

Tactic:
VectorMeasure.AbsolutelyContinuous.mk fun j hj₁ hj₂ => ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
refine :
  ∀ (j : Set α) (hj₁ : MeasurableSet j) (hj₂ : (↑(μ.trim hm).toENNRealVectorMeasure : Set α → ℝ≥0∞) j = 0),
    (↑(VectorMeasure.trim (μ.withDensityᵥ f) hm) : Set α → E) j = 0
⊢ VectorMeasure.trim (μ.withDensityᵥ f) hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure

Tactic:
refine VectorMeasure.AbsolutelyContinuous.mk fun j hj₁ hj₂ => ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : (↑(μ.trim hm).toENNRealVectorMeasure : Set α → ℝ≥0∞) j = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) j : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.toENNRealVectorMeasure_apply_measurable hj₁, trim_measurableSet_eq hm hj₁] at hj₂

Premises used: MeasureTheory.trim_measurableSet_eq, MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) j : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in j, f x ∂μ) 0
⊢ (↑(VectorMeasure.trim (μ.withDensityᵥ f) hm) : Set α → E) j = 0

Tactic:
rw [VectorMeasure.trim_measurableSet_eq hm hj₁, withDensityᵥ_apply hfi (hm _ hj₁)]

Premises used: MeasureTheory.VectorMeasure.trim_measurableSet_eq, MeasureTheory.withDensityᵥ_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) j : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in j, f x ∂μ) 0

Tactic:
simp only [Measure.restrict_eq_zero.mpr hj₂, integral_zero_measure]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.integral_zero_measure
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
ax : FieldAxiom
addAssoc : K ⊨ FieldAxiom.addAssoc.toSentence ↔ toProp K FieldAxiom.addAssoc
zeroAdd : K ⊨ FieldAxiom.zeroAdd.toSentence ↔ toProp K FieldAxiom.zeroAdd
negAddCancel : K ⊨ FieldAxiom.negAddCancel.toSentence ↔ toProp K FieldAxiom.negAddCancel
mulAssoc : K ⊨ FieldAxiom.mulAssoc.toSentence ↔ toProp K FieldAxiom.mulAssoc
mulComm : K ⊨ FieldAxiom.mulComm.toSentence ↔ toProp K FieldAxiom.mulComm
oneMul : K ⊨ FieldAxiom.oneMul.toSentence ↔ toProp K FieldAxiom.oneMul
existsInv : K ⊨ FieldAxiom.existsInv.toSentence ↔ toProp K FieldAxiom.existsInv
leftDistrib : K ⊨ FieldAxiom.leftDistrib.toSentence ↔ toProp K FieldAxiom.leftDistrib
existsPairNE : K ⊨ FieldAxiom.existsPairNE.toSentence ↔ toProp K FieldAxiom.existsPairNE
⊢ K ⊨ ax.toSentence ↔ toProp K ax

Tactic:
cases ax
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ addAssoc.toSentence ↔ toProp K addAssoc

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ zeroAdd.toSentence ↔ toProp K zeroAdd

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ negAddCancel.toSentence ↔ toProp K negAddCancel

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ mulAssoc.toSentence ↔ toProp K mulAssoc

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ mulComm.toSentence ↔ toProp K mulComm

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ oneMul.toSentence ↔ toProp K oneMul

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Field.Basic
Goal:
K : Type u_2
inst : Add K
inst_1 : Mul K
inst_2 : Neg K
inst_3 : Zero K
inst_4 : One K
inst_5 : CompatibleRing K
⊢ K ⊨ existsInv.toSentence ↔ toProp K existsInv

Tactic:
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Premises used: FirstOrder.Language.Sentence.Realize, Fin.snoc, FirstOrder.Language.Formula.Realize