awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞)
have refine : (↑i.parts : Set (Subtype MeasurableSet)).PairwiseDisjoint (Subtype.val (p := MeasurableSet))
Tactic: refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [sup_set_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ i.parts, ‖(↑μ : Set X → V) (↑x : Set X)‖ₑ : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have x : Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
  ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
Tactic: calc
    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum (fun s hs => h s s.property)
    _ = m (i.parts.sup Subtype.val) := by
      rw [sup_set_eq_biUnion]
      refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm
      intro a ha b hb hab
      simpa [disjoint_iff, Subtype.ext_iff] using i.disjoint ha hb hab
    _ ≤ m s := by
      rw [sup_set_eq_biUnion]
      exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
x :
  Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ i.parts, ‖(↑μ : Set X → V) (↑x : Set X)‖ₑ : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have x₁ : LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
  ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: calc
    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum (fun s hs => h s s.property)
    _ = m (i.parts.sup Subtype.val) := by
      rw [sup_set_eq_biUnion]
      refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm
      intro a ha b hb hab
      simpa [disjoint_iff, Subtype.ext_iff] using i.disjoint ha hb hab
    _ ≤ m s := by
      rw [sup_set_eq_biUnion]
      exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
⊢ (μ + ν).variation ≤ μ.variation + ν.variation
have refine : ∀ (E : Set X), MeasurableSet E → ‖(↑(μ + ν) : Set X → V) E‖ₑ ≤ (μ.variation + ν.variation : (a : Set X) → ℝ≥0∞) E
Tactic: refine variation_le_of_forall_enorm_le fun E _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑μ : Set X → V) E‖ₑ + ‖(↑ν : Set X → V) E‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
      ((ν.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
have h₁ : ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
h₁ : ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
⊢ ‖(↑μ : Set X → V) E‖ₑ + ‖(↑ν : Set X → V) E‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
      ((ν.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
have h₂ : ‖(↑ν : Set X → V) E‖ₑ ≤ (ν.variation : (a : Set X) → ℝ≥0∞) E
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑(μ + ν) : Set X → V) E‖ₑ ≤ (μ.variation + ν.variation : (a : Set X) → ℝ≥0∞) E
have _ : ‖(↑μ : Set X → V) E‖ₑ + ‖(↑ν : Set X → V) E‖ₑ ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
    ((ν.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
Tactic: calc
    _ ≤ ‖μ E‖ₑ + ‖ν E‖ₑ := enorm_add_le _ _
    _ ≤ μ.variation E + ν.variation E := by
      gcongr <;> exact enorm_measure_le_variation _ E
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
s : Finset ι
μ : ι → VectorMeasure X V
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)
have empty : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
s : Finset ι
μ : ι → VectorMeasure X V
empty : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)
have insert : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (ih : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)),
  LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ insert i s, μ i))
    (∑ i ∈ insert i s, (μ i).variation)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
s : Finset ι
μ : ι → VectorMeasure X V
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)
have empty : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
s : Finset ι
μ : ι → VectorMeasure X V
empty : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)
have insert : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (ih : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)),
  LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ insert i s, μ i))
    (∑ i ∈ insert i s, (μ i).variation)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ : VectorMeasure X V
E : Set X
hE : Ne (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖(↑μ : Set X → V) E‖ ≤ μ.variation.real E
have rw : ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
Tactic: rw [measureReal_def, ← toReal_enorm, ENNReal.toReal_le_toReal (enorm_ne_top) hE]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ ν : VectorMeasure X V
⊢ (μ - ν).variation ≤ μ.variation + ν.variation
have grw : (μ + -ν).variation ≤ μ.variation + ν.variation
Tactic: grw [sub_eq_add_neg, variation_add_le, variation_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ ν : VectorMeasure X V
grw : (μ + -ν).variation ≤ μ.variation + ν.variation
⊢ (μ - ν).variation ≤ μ.variation + ν.variation
have grw₁ : μ.variation + (-ν).variation ≤ μ.variation + ν.variation
Tactic: grw [sub_eq_add_neg, variation_add_le, variation_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ ν : VectorMeasure X V
grw : (μ + -ν).variation ≤ μ.variation + ν.variation
grw₁ : μ.variation + (-ν).variation ≤ μ.variation + ν.variation
⊢ (μ - ν).variation ≤ μ.variation + ν.variation
have grw₂ : μ.variation + ν.variation ≤ μ.variation + ν.variation
Tactic: grw [sub_eq_add_neg, variation_add_le, variation_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Defs (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
V : Type u_2
inst_1 : TopologicalSpace V
inst_2 : ENormedAddCommMonoid V
inst_3 : T2Space V
μ : VectorMeasure X V
s : ℕ → { t : Set X // MeasurableSet t }
hs : Pairwise (Function.onFun Disjoint (Subtype.val (p := fun (t : Set X) ↦ MeasurableSet t) ∘ s))
⊢ LE.le (α := ℝ≥0∞) ((fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) (⋃ (i : ℕ), (↑(s i) : Set X)))
    (∑' (i : ℕ), (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) (↑(s i) : Set X))
have hmeas : ∀ (i : ℕ), MeasurableSet (↑(s i) : Set X)
Tactic: have hmeas : ∀ i, MeasurableSet (s i).val := fun i => (s i).prop
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ 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)
have 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 ∂μ)
Tactic: convert! hasSum_integral_iUnion hs₁ hs₂ hf.integrableOn with n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 ∂μ)
⊢ 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)
have 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 ∂μ)
Tactic: convert! hasSum_integral_iUnion hs₁ hs₂ hf.integrableOn with n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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 : ℕ
⊢ Eq.{u_2 + 1} (α := E) (if MeasurableSet (s n) then ∫ (x : α) in s n, f x ∂μ else 0) (∫ (x : α) in s n, f x ∂μ)
have h : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s n, f x ∂μ) (∫ (x : α) in s n, f x ∂μ)
Tactic: rw [if_pos (hs₁ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
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)
⊢ 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 ∂μ)
have h : Eq.{u_2 + 1} (α := E) (∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ) (∫ (x : α) in ⋃ (n : ℕ), s n, f x ∂μ)
Tactic: rw [if_pos (MeasurableSet.iUnion 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 : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ (↑(μ.withDensityᵥ f) : Set α → E) s = ∫ (x : α) in s, f x ∂μ
have rw : Eq.{u_2 + 1} (α := E)
  ((↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := sorry,
          not_measurable' := sorry, m_iUnion' := sorry } :
      Set α → E)
    s)
  (∫ (x : α) in s, f x ∂μ)
Tactic: rw [withDensityᵥ, dif_pos 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
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ 0) 0
have h : ∀ (s : Set α) (hs : MeasurableSet s), Eq.{u_2 + 1} (α := E) ((↑(μ.withDensityᵥ 0) : Set α → E) s) ((↑0 : Set α → E) s)
Tactic: ext1 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
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) ((↑(μ.withDensityᵥ 0) : Set α → E) s) ((↑0 : Set α → E) s)
have h : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, 0 ∂μ) ((↑0 : Set α → E) s)
Tactic: rw [Pi.zero_def, withDensityᵥ_apply (integrable_zero α E μ) 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 : α → E
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
have pos : ∀ (hf : Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.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
f : α → E
pos : ∀ (hf : Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
have neg : ∀ (hf : ¬Integrable f μ), Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.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
f : α → E
hf : Integrable f μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
have pos : ∀ (i : Set α) (hi : MeasurableSet i), (↑(μ.withDensityᵥ (-f)) : Set α → E) i = (↑(-μ.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
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ (↑(μ.withDensityᵥ (-f)) : Set α → E) i = (↑(-μ.withDensityᵥ f) : Set α → E) i
have pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in i, (-f) x ∂μ) (∫ (a : α) in i, -f a ∂μ)
Tactic: rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
      withDensityᵥ_apply hf.neg 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 : α → E
hf : ¬Integrable f μ
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ (-f)) (-μ.withDensityᵥ f)
have neg : ¬Integrable (-f) μ
Tactic: rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_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 g : α → E
hf : Integrable f μ
hg : Integrable g μ
⊢ μ.withDensityᵥ (f + g) = HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(μ.withDensityᵥ (f + g)) : Set α → E) i =
    (↑(HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)) : 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ (↑(μ.withDensityᵥ (f + g)) : Set α → E) i =
    (↑(HAdd.hAdd (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)) : Set α → E) i
have h : ∫ (x : α) in i, (f + g) x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
Tactic: rw [withDensityᵥ_apply (hf.add hg) hi, VectorMeasure.add_apply, withDensityᵥ_apply hf hi,
    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
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (f + g) x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
have h : ∫ (x : α) in i, f x + g x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
Tactic: simp_rw [Pi.add_apply]
-- 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 μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x + g x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
have h : Integrable f (μ.restrict i)
Tactic: rw [integral_add]
-- 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 μ
i : Set α
hi : MeasurableSet i
h : Integrable f (μ.restrict i)
⊢ ∫ (x : α) in i, f x + g x ∂μ = HAdd.hAdd (α := E) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, g x ∂μ)
have h₁ : Integrable g (μ.restrict i)
Tactic: rw [integral_add]
-- 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 μ
⊢ μ.withDensityᵥ (f - g) = HSub.hSub (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have rw : μ.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]
-- 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)
⊢ μ.withDensityᵥ (f - g) = HSub.hSub (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have rw₁ : μ.withDensityᵥ (f + -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
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)
⊢ μ.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]