awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ_1 : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := E) (if MeasurableSet (s n) then ∫ (x : α) in s n, f x ∂μ else 0) (∫ (x : α) in s n, f x ∂μ)
h₁ :
  Eq.{u_2 + 1} (α := E)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), s i) then ∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ else 0)
    (∫ (x : α) in ⋃ (n : ℕ), s n, f x ∂μ)
⊢ HasSum.{u_2, 0} (α := E) (fun (i : ℕ) ↦ if MeasurableSet (s i) then ∫ (x : α) in s i, f x ∂μ else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), s i) then ∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ else 0)

Tactic:
convert! hasSum_integral_iUnion hs₁ hs₂ hf.integrableOn with n

Premises used: MeasureTheory.hasSum_integral_iUnion, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ_1 : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
n : ℕ
h h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s n, f x ∂μ) (∫ (x : α) in s n, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (if MeasurableSet (s n) then ∫ (x : α) in s n, f x ∂μ else 0) (∫ (x : α) in s n, f x ∂μ)

Tactic:
rw [if_pos (hs₁ n)]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ_1 : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
h h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ) (∫ (x : α) in ⋃ (n : ℕ), s n, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), s i) then ∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ else 0)
    (∫ (x : α) in ⋃ (n : ℕ), s n, f x ∂μ)

Tactic:
rw [if_pos (MeasurableSet.iUnion hs₁)]

Premises used: if_pos, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
rw :
  Eq.{u_2 + 1} (α := E)
    ((↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ } :
        Set α → E)
      s)
    (∫ (x : α) in s, f x ∂μ)
⊢ (↑(μ.withDensityᵥ f) : Set α → E) s = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [withDensityᵥ, dif_pos hf]

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E)
    ((↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ } :
        Set α → E)
      s)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
dif_pos hs

Premises used: dif_pos, dite, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E)
    ((↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ } :
        Set α → E)
      s)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
exact dif_pos hs

Premises used: dif_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h :
  ∀ (s : Set α) (hs : MeasurableSet s), Eq.{u_2 + 1} (α := E) ((↑(μ.withDensityᵥ 0) : Set α → E) s) ((↑0 : Set α → E) s)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ 0) 0

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
h : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, 0 ∂μ) ((↑0 : Set α → E) s)
⊢ Eq.{u_2 + 1} (α := E) ((↑(μ.withDensityᵥ 0) : Set α → E) s) ((↑0 : Set α → E) s)

Tactic:
rw [Pi.zero_def, withDensityᵥ_apply (integrable_zero α E μ) hs]

Premises used: MeasureTheory.integrable_zero, Pi.zero_def, 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
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, 0 ∂μ) ((↑0 : Set α → E) s)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
pos : ∀ (hf : Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
neg : ∀ (hf : ¬Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)

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 : α → E
hf : Integrable f μ
pos :
  ∀ (i : Set α) (hi : MeasurableSet i), (↑(μ.withDensityᵥ (-f)) : Set α → E) i = (↑(-μ.withDensityᵥ f) : Set α → E) i
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)

Tactic:
ext1 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 : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, (-f) x ∂μ) (∫ (a : α) in i, -f a ∂μ)
⊢ (↑(μ.withDensityᵥ (-f)) : Set α → E) i = (↑(-μ.withDensityᵥ f) : Set α → E) i

Tactic:
rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
      withDensityᵥ_apply hf.neg hi]

Premises used: MeasureTheory.VectorMeasure.neg_apply, MeasureTheory.Integrable.neg, MeasureTheory.integral_neg, 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 : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, (-f) x ∂μ) (∫ (a : α) in i, -f a ∂μ)

Tactic:
simp only [Pi.neg_apply]

Premises used: Pi.neg_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 : α → E
hf : ¬Integrable f μ
neg : ¬Integrable (-f) μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)

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

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg, neg_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
hf neg neg₁ neg₂ neg₃ : ¬Integrable f μ
⊢ ¬Integrable (-f) μ

Tactic:
rwa [integrable_neg_iff]

Premises used: MeasureTheory.integrable_neg_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ -f x) (-μ.withDensityᵥ f)

Tactic:
withDensityᵥ_neg

Premises used: MeasureTheory.withDensityᵥ_neg
-- 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
hf : Integrable f μ
hg : Integrable g μ
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(μ.withDensityᵥ (f + g)) : Set α → E) i =
      (↑(HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)) : Set α → E) i
⊢ μ.withDensityᵥ (f + g) = HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
ext1 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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
h : ∫ (x : α) in i, (f + g) x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
⊢ (↑(μ.withDensityᵥ (f + g)) : Set α → E) i =
    (↑(HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)) : Set α → E) i

Tactic:
rw [withDensityᵥ_apply (hf.add hg) hi, VectorMeasure.add_apply, withDensityᵥ_apply hf hi,
    withDensityᵥ_apply hg hi]

Premises used: MeasureTheory.withDensityᵥ_apply, MeasureTheory.Integrable.add, MeasureTheory.VectorMeasure.add_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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
h : ∫ (x : α) in i, f x + g x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
⊢ ∫ (x : α) in i, (f + g) x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)

Tactic:
simp_rw [Pi.add_apply]

Premises used: Pi.add_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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
h : Integrable f (μ.restrict i)
h₁ : Integrable g (μ.restrict i)
⊢ ∫ (x : α) in i, f x + g x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)

Tactic:
rw [integral_add]

Premises used: MeasureTheory.integral_add
-- 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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable f (μ.restrict i)

Tactic:
hf.integrableOn

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.integrableOn
-- 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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable f (μ.restrict i)

Tactic:
exact hf.integrableOn

Premises used: MeasureTheory.Integrable.integrableOn
-- 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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable g (μ.restrict i)

Tactic:
hg.integrableOn

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.integrableOn
-- 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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable g (μ.restrict i)

Tactic:
exact hg.integrableOn

Premises used: MeasureTheory.Integrable.integrableOn
-- 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
hf : Integrable f μ
hg : Integrable g μ
⊢ (μ.withDensityᵥ fun (x : α) ↦ f x + g x) = HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
withDensityᵥ_add hf hg

Premises used: MeasureTheory.withDensityᵥ_add
-- 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
hf : Integrable f μ
hg : Integrable g μ
rw : μ.withDensityᵥ (f + -g) = HSub.hSub (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
rw₁ : μ.withDensityᵥ (f + -g) = HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (-μ.withDensityᵥ g)
rw₂ :
  HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ (-g)) =
    HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (-μ.withDensityᵥ g)
rw₃ rw₄ :
  HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (-μ.withDensityᵥ g) =
    HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (-μ.withDensityᵥ g)
⊢ μ.withDensityᵥ (f - g) = HSub.hSub (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]

Premises used: MeasureTheory.Integrable.neg, sub_eq_add_neg, MeasureTheory.withDensityᵥ_neg, MeasureTheory.withDensityᵥ_add
-- 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
hf : Integrable f μ
hg : Integrable g μ
⊢ (μ.withDensityᵥ fun (x : α) ↦ f x - g x) = HSub.hSub (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)

Tactic:
withDensityᵥ_sub hf hg

Premises used: MeasureTheory.withDensityᵥ_sub
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
pos : ∀ (hf : Integrable f μ), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
neg : ∀ (hf : ¬Integrable f μ), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)

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
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f μ
pos :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(μ.withDensityᵥ (r • f)) : Set α → E) i =
      (↑(HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)) : Set α → E) i
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)

Tactic:
ext1 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
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, (r • f) x ∂μ) (∫ (a : α) in i, r • f a ∂μ)
⊢ (↑(μ.withDensityᵥ (r • f)) : Set α → E) i =
    (↑(HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)) : Set α → E) i

Tactic:
rw [withDensityᵥ_apply (hf.smul r) hi, VectorMeasure.smul_apply, withDensityᵥ_apply hf hi, ←
      integral_smul r f]

Premises used: MeasureTheory.VectorMeasure.smul_apply, MeasureTheory.Integrable.smul, MeasureTheory.integral_smul, 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
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, (r • f) x ∂μ) (∫ (a : α) in i, r • f a ∂μ)

Tactic:
simp only [Pi.smul_apply]

Premises used: Pi.smul_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
pos : ∀ (hr : r = 0), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
neg : ∀ (hr : ¬r = 0), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : r = 0
pos : μ.withDensityᵥ (HSMul.hSMul (α := 𝕜) 0 f) = HSMul.hSMul (α := 𝕜) (β := VectorMeasure α E) 0 (μ.withDensityᵥ f)
pos₁ : μ.withDensityᵥ 0 = HSMul.hSMul (α := 𝕜) (β := VectorMeasure α E) 0 (μ.withDensityᵥ f)
pos₂ : Eq (α := VectorMeasure α E) (μ.withDensityᵥ 0) 0
pos₃ pos₄ : Eq (α := VectorMeasure α E) 0 0
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)

Tactic:
rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]

Premises used: zero_smul, MeasureTheory.withDensityᵥ_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
neg : ¬Integrable (r • f) μ
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)

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

Premises used: MeasureTheory.Measure.withDensityᵥ, smul_zero, 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
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
neg neg₁ neg₂ neg₃ : ¬Integrable f μ
⊢ ¬Integrable (r • f) μ

Tactic:
rwa [integrable_smul_iff hr f]

Premises used: MeasureTheory.integrable_smul_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
⊢ (μ.withDensityᵥ fun (x : α) ↦ r • f x) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)

Tactic:
withDensityᵥ_smul f r

Premises used: MeasureTheory.withDensityᵥ_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    (↑(μ.withDensityᵥ (f • g)) : Set α → E) s =
      (↑((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).withDensityᵥ g) : Set α → E) s
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (f • g)) ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).withDensityᵥ g)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
h : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f • g) x ∂μ) (∫ (x : α) in s, f x • g x ∂μ)
⊢ (↑(μ.withDensityᵥ (f • g)) : Set α → E) s =
    (↑((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).withDensityᵥ g) : Set α → E) s

Tactic:
rw [withDensityᵥ_apply hfg hs,
    withDensityᵥ_apply ((integrable_withDensity_iff_integrable_smul₀ hf).mpr hfg) hs,
    setIntegral_withDensity_eq_setIntegral_smul₀ hf.restrict _ hs]

Premises used: Iff.mpr, setIntegral_withDensity_eq_setIntegral_smul₀, MeasureTheory.integrable_withDensity_iff_integrable_smul₀, AEMeasurable.restrict, 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 : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f • g) x ∂μ) (∫ (x : α) in s, f x • g x ∂μ)

Tactic:
simp only [Pi.smul_apply']

Premises used: Pi.smul_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 : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
hfg : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
rw :
  Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal • g x)
    (μ.withDensityᵥ (HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g))
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal • g x) ((μ.withDensity f).withDensityᵥ g)

Tactic:
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    ← withDensityᵥ_smul_eq_withDensityᵥ_withDensity hf.ennreal_toNNReal hfg]

Premises used: AEMeasurable.ennreal_toNNReal, MeasureTheory.coe_toNNReal_ae_eq, MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity, MeasureTheory.withDensity_congr_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 : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
hfg : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
h : (fun (x : α) ↦ (f x).toReal • g x) = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal • g x)
    (μ.withDensityᵥ (HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
hfg : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
h : ∀ (x : α), (f x).toReal • g x = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g x
⊢ (fun (x : α) ↦ (f x).toReal • g x) = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g

Tactic:
ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
hfg : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
x : α
⊢ (f x).toReal • g x = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g x

Tactic:
simp [NNReal.smul_def, ENNReal.coe_toNNReal_eq_toReal]

Premises used: ENNReal.coe_toNNReal_eq_toReal, NNReal.smul_def