awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ μ.withDensityᵥ (f - g) = HSub.hSub (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have rw₃ : HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (-μ.withDensityᵥ g) =
  HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (-μ.withDensityᵥ g)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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ᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos : ∀ (hf : Integrable f μ), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have neg : ∀ (hf : ¬Integrable f μ), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 μ
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(μ.withDensityᵥ (r • f)) : Set α → E) i =
    (↑(HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)) : Set α → E) i
Tactic: ext1 i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ (↑(μ.withDensityᵥ (r • f)) : Set α → E) i =
    (↑(HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)) : Set α → E) i
have pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, (r • f) x ∂μ) (∫ (a : α) in i, r • f a ∂μ)
Tactic: rw [withDensityᵥ_apply (hf.smul r) hi, VectorMeasure.smul_apply, withDensityᵥ_apply hf hi, ←
      integral_smul r f]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 μ
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos : ∀ (hr : r = 0), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have neg : ∀ (hr : ¬r = 0), μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos : μ.withDensityᵥ (HSMul.hSMul (α := 𝕜) 0 f) = HSMul.hSMul (α := 𝕜) (β := VectorMeasure α E) 0 (μ.withDensityᵥ f)
Tactic: rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos₁ : μ.withDensityᵥ 0 = HSMul.hSMul (α := 𝕜) (β := VectorMeasure α E) 0 (μ.withDensityᵥ f)
Tactic: rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos₂ : Eq (α := VectorMeasure α E) (μ.withDensityᵥ 0) 0
Tactic: rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have pos₃ : Eq (α := VectorMeasure α E) 0 0
Tactic: rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ μ.withDensityᵥ (r • f) = HSMul.hSMul (β := VectorMeasure α E) r (μ.withDensityᵥ f)
have neg : ¬Integrable (r • f) μ
Tactic: rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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) μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (f • g)) ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).withDensityᵥ g)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  (↑(μ.withDensityᵥ (f • g)) : Set α → E) s =
    (↑((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).withDensityᵥ g) : Set α → E) s
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ (↑(μ.withDensityᵥ (f • g)) : Set α → E) s =
    (↑((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).withDensityᵥ g) : Set α → E) s
have h : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f • g) x ∂μ) (∫ (x : α) in s, f x • g x ∂μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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) μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal • g x) ((μ.withDensity f).withDensityᵥ g)
have rw : Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal • g x)
  (μ.withDensityᵥ (HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g))
Tactic: rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    ← withDensityᵥ_smul_eq_withDensityᵥ_withDensity hf.ennreal_toNNReal hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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) μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal • g x)
    (μ.withDensityᵥ (HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g))
have h : (fun (x : α) ↦ (f x).toReal • g x) = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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) μ
⊢ (fun (x : α) ↦ (f x).toReal • g x) = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g
have h : ∀ (x : α), (f x).toReal • g x = HSMul.hSMul (α := α → ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) g x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
have pos : ∀ (hf : Integrable f μ), μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
pos : ∀ (hf : Integrable f μ), μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
have neg : ∀ (hf : ¬Integrable f μ), μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
have pos : ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i = 0),
  (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0
Tactic: refine VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i = 0
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0
have hi₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂
Cleared hypotheses: hi₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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∞)
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0
have pos : Eq (α := ℝ) (∫ (x : α) in i, f x ∂μ) 0
Tactic: rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0
have pos₁ : Eq (α := ℝ) (@integral _ _ _ _ m 0 fun (x : α) ↦ f x) 0
Tactic: rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i = 0
have pos₂ : Eq (α := ℝ) 0 0
Tactic: rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
have neg : VectorMeasure.AbsolutelyContinuous (M := ℝ) 0 μ.toENNRealVectorMeasure
Tactic: rw [withDensityᵥ, dif_neg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
have 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 ∂μ)
Tactic: refine hf.ae_eq_of_forall_setIntegral_eq f g hg fun i hi _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
have rw : (↑(μ.withDensityᵥ f) : Set α → E) i = ∫ (x : α) in i, g x ∂μ
Tactic: rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 ∂μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
have rw₁ : (↑(μ.withDensityᵥ g) : Set α → E) i = ∫ (x : α) in i, g x ∂μ
Tactic: rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 ∂μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
have rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, g x ∂μ) (∫ (x : α) in i, g x ∂μ)
Tactic: rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have pos : ∀ (hf : Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have neg : ∀ (hf : ¬Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have pos : ∀ (i : Set α) (hi : MeasurableSet i), (↑(μ.withDensityᵥ f) : Set α → E) i = (↑(μ.withDensityᵥ g) : Set α → E) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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
⊢ (↑(μ.withDensityᵥ f) : Set α → E) i = (↑(μ.withDensityᵥ g) : Set α → E) i
have pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
Tactic: rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (hypothesis)
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 μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have hg : ¬Integrable g μ
Tactic: have hg : ¬Integrable g μ := by intro hg; exact hf (hg.congr h.symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have 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' := sorry,
      not_measurable' := sorry, m_iUnion' := sorry }
  else 0)
  (μ.withDensityᵥ g)
Tactic: rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have 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' := sorry,
      not_measurable' := sorry, m_iUnion' := sorry }
  else 0)
  (if hf : Integrable g μ then
    { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := sorry,
      not_measurable' := sorry, m_iUnion' := sorry }
  else 0)
Tactic: rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have 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' := sorry,
      not_measurable' := sorry, m_iUnion' := sorry }
  else 0)
Tactic: rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]