awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑(s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) : Set α → ℝ) i
h₂ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i -
      (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
h₃ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.real i - (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
h₄ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i
h₅ :
  ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) -
      s.toJordanDecomposition.negPart.real i =
    ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) -
      s.toJordanDecomposition.negPart.real i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
have h₆ : ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) -
    ENNReal.toReal ((s.toJordanDecomposition.negPart : (a : Set α) → ENNReal) i) =
  ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) -
    ENNReal.toReal ((s.toJordanDecomposition.negPart : (a : Set α) → ENNReal) i)
Tactic: rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)
have h₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
Tactic: refine Integrable.integrableOn ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
have h₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
Tactic: refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
have h₂ : ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ⊤
Tactic: refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)
have h₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
Tactic: refine Integrable.integrableOn ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
have h₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
Tactic: refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
have h₂ : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤
Tactic: refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ ν : Measure α
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
hf : Integrable f μ
⊢ Eq (α := VectorMeasure α E) (ν.withDensityᵥ fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) (μ.withDensityᵥ f)
have rw : Eq (α := VectorMeasure α E) ((ν.withDensity (μ.rnDeriv ν)).withDensityᵥ f) (μ.withDensityᵥ f)
Tactic: rw [withDensityᵥ_smul_eq_withDensityᵥ_withDensity' (measurable_rnDeriv μ ν).aemeasurable
    (rnDeriv_lt_top μ ν) ((integrable_rnDeriv_smul_iff hμν).mpr hf), withDensity_rnDeriv_eq μ ν hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ ν : Measure α
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
hf : Integrable f μ
rw : Eq (α := VectorMeasure α E) ((ν.withDensity (μ.rnDeriv ν)).withDensityᵥ f) (μ.withDensityᵥ f)
⊢ Eq (α := VectorMeasure α E) (ν.withDensityᵥ fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) (μ.withDensityᵥ f)
have rw₁ : Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ f)
Tactic: rw [withDensityᵥ_smul_eq_withDensityᵥ_withDensity' (measurable_rnDeriv μ ν).aemeasurable
    (rnDeriv_lt_top μ ν) ((integrable_rnDeriv_smul_iff hμν).mpr hf), withDensity_rnDeriv_eq μ ν hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s t : Set X
hs : MeasurableSet s
ht : MeasurableSet t
hdisj : Disjoint s t
⊢ cbmApplyMeasure μ B (s ∪ t) = cbmApplyMeasure μ B s + cbmApplyMeasure μ B t
have h : ∀ (x : E),
  Eq.{u_5 + 1} (α := G) ((cbmApplyMeasure μ B (s ∪ t) : (a : E) → G) x : G)
    ((cbmApplyMeasure μ B s + cbmApplyMeasure μ B t : (a : E) → G) x : G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
⊢ ‖cbmApplyMeasure μ B s‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖
have rw : ∀ (x : E), norm.{u_5} (E := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G) ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
Tactic: rw [opNorm_le_iff (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
x : E
⊢ norm.{u_5} (E := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G) ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
have grw : norm.{u_5} (E := G) ((((B : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) ((↑μ : Set X → F) s) : G) ≤
  ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
Tactic: grw [cbmApplyMeasure_apply, le_opNorm₂, mul_right_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
x : E
grw :
  norm.{u_5} (E := G) ((((B : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) ((↑μ : Set X → F) s) : G) ≤
    ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
⊢ norm.{u_5} (E := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G) ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
have grw₁ : ‖B‖ * ‖x‖ * ‖(↑μ : Set X → F) s‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
Tactic: grw [cbmApplyMeasure_apply, le_opNorm₂, mul_right_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
x : E
grw :
  norm.{u_5} (E := G) ((((B : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) ((↑μ : Set X → F) s) : G) ≤
    ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
grw₁ : ‖B‖ * ‖x‖ * ‖(↑μ : Set X → F) s‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
⊢ norm.{u_5} (E := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G) ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
have grw₂ : ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
Tactic: grw [cbmApplyMeasure_apply, le_opNorm₂, mul_right_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose 0) 0
have h : ∀ (i : Set X),
  MeasurableSet i →
    ∀ (x : E),
      Eq.{u_5 + 1} (α := G) (((↑(μ.transpose 0) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
        (((↑0 : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
⊢ μ.transpose (B + C) = μ.transpose B + μ.transpose C
have h : ∀ (i : Set X),
  MeasurableSet i →
    ∀ (x : E),
      Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (B + C)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
        (((↑(μ.transpose B + μ.transpose C) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : ι → VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)
have empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : ι → VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)
have insert : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)),
  Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ insert i s, μ i) B) (∑ i ∈ insert i s, (μ i).transpose B)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : ι → VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)
have empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : ι → VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)
have insert : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)),
  Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ insert i s, μ i) B) (∑ i ∈ insert i s, (μ i).transpose B)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))
have empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))
have insert : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))),
  Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ insert i s, B i)) (∑ i ∈ insert i s, μ.transpose (B i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))
have empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))
have insert : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))),
  Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ insert i s, B i)) (∑ i ∈ insert i s, μ.transpose (B i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ (-μ).transpose B = -μ.transpose B
have h : ∀ (i : Set X),
  MeasurableSet i →
    ∀ (x : E),
      Eq.{u_5 + 1} (α := G) (((↑((-μ).transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
        (((↑(-μ.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ μ.transpose (-B) = -μ.transpose B
have h : ∀ (i : Set X),
  MeasurableSet i →
    ∀ (x : E),
      Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (-B)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
        (((↑(-μ.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ (μ - ν).transpose B = μ.transpose B - ν.transpose B
have h : ∀ (i : Set X),
  MeasurableSet i →
    ∀ (x : E),
      Eq.{u_5 + 1} (α := G) (((↑((μ - ν).transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
        (((↑(μ.transpose B - ν.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
⊢ μ.transpose (B - C) = μ.transpose B - μ.transpose C
have h : ∀ (i : Set X),
  MeasurableSet i →
    ∀ (x : E),
      Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (B - C)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
        (((↑(μ.transpose B - μ.transpose C) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h : ¬μ.Integrable f B
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ] = 0
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h : ¬μ.Integrable f B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ] = 0
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ] = 0
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h : ¬μ.Integrable f B
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0
have pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) B) 0
Tactic: simp [integral, setToFun_undef _ h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Integral (goal)
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h : ¬μ.Integrable f B
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0
have neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) B) 0
Tactic: simp [integral, hG]