awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), 0 ∂[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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), 0 ∂[B; μ] = 0
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), 0 ∂[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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0
have pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ 0) B) 0
Tactic: simp only [integral, hG]
-- 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
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0
have neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ 0) B) 0
Tactic: simp [integral, hG]
-- 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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
⊢ ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
⊢ ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
have pos : sorry μ (fun (x : X) ↦ f x + g x) B = HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
Tactic: simp only [integral, hG]
-- 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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
have neg : sorry μ (fun (x : X) ↦ f x + g x) B = HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
Tactic: simp [integral, hG]
-- 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 ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
Tactic: by_cases hG : CompleteSpace G
-- 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 ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
Tactic: by_cases hG : CompleteSpace G
-- 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 ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
have pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ ∑ i ∈ s, f i x) B) (∑ x ∈ s, sorry μ (fun (x_1 : X) ↦ f x x_1) B)
Tactic: simp only [integral, hG]
-- 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 ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
have neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ ∑ i ∈ s, f i x) B) (∑ x ∈ s, sorry μ (fun (x_1 : X) ↦ f x x_1) B)
Tactic: simp [integral, hG]
-- 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
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
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
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
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
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
have pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ -f x) B) (-sorry μ (fun (x : X) ↦ f x) B)
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_eq_cbmApplyMeasure]
-- 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
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
have neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ -f x) B) (-sorry μ (fun (x : X) ↦ f x) B)
Tactic: simp [integral, hG]
-- 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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
have pos : sorry μ (fun (x : X) ↦ f x - g x) B = HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
Tactic: simp only [integral, hG]
-- 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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
have neg : sorry μ (fun (x : X) ↦ f x - g x) B = HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
Tactic: simp [integral, hG]
-- 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
c : ℝ
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
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
c : ℝ
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
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
c : ℝ
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
have pos : sorry μ (fun (x : X) ↦ c • f x) B = HSMul.hSMul (β := G) c (sorry μ (fun (x : X) ↦ f x) B)
Tactic: simp only [integral, hG]
-- 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
c : ℝ
hG : CompleteSpace G
⊢ ∀ (c : ℝ) (s : Set X) (x : E),
    (?m.112 s : (a : E) → ?m.104) (c • x) = HSMul.hSMul (β := ?m.104) c ((?m.112 s : (a : E) → ?m.104) x : ?m.104)
have simp : ∀ (c : ℝ) (s : Set X) (x : E),
  HSMul.hSMul (β := ?m.104) c ((?m.112 s : (a : E) → ?m.104) x : ?m.104) =
    HSMul.hSMul (β := ?m.104) c ((?m.112 s : (a : E) → ?m.104) x : ?m.104)
Tactic: simp
-- 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
c : ℝ
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
have neg : sorry μ (fun (x : X) ↦ c • f x) B = HSMul.hSMul (β := G) c (sorry μ (fun (x : X) ↦ f x) B)
Tactic: simp [integral, hG]
-- 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
B : E →L[ℝ] F →L[ℝ] G
⊢ ∫ᵛ (x : X), f x ∂[B; 0] = 0
have simp : Eq.{u_5 + 1} (α := G) (sorry 0 (fun (x : X) ↦ f x) B) 0
Tactic: simp [integral]
-- 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
hν : ν.Integrable f B
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
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
hν : ν.Integrable f B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
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
hν : ν.Integrable f B
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
have pos : sorry (μ + ν) (fun (x : X) ↦ f x) B = HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry ν (fun (x : X) ↦ f x) B)
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_add_vectorMeasure, coe_add,
      transpose_eq_cbmApplyMeasure, ← setToFun_add_measure
        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ 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
hν : ν.Integrable f B
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
have neg : sorry (μ + ν) (fun (x : X) ↦ f x) B = HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry ν (fun (x : X) ↦ f x) B)
Tactic: simp [integral, hG]
-- 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
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
Tactic: by_cases hG : CompleteSpace G
-- 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
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
Tactic: by_cases hG : CompleteSpace G
-- 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
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
have pos : ∀ (hs : s.Nonempty), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
Tactic: by_cases! hs : s.Nonempty
-- 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
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
pos : ∀ (hs : s.Nonempty), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
have neg : ∀ (hs : s = ∅), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
Tactic: by_cases! hs : s.Nonempty
-- 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
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
hs : s.Nonempty
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
have pos : Eq.{u_5 + 1} (α := G) (sorry (∑ i ∈ s, μ i) (fun (x : X) ↦ f x) B) (∑ x ∈ s, sorry (μ x) (fun (x : X) ↦ f x) B)
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_vectorMeasure, coe_finsetSum,
        transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
          (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure (μ i) B) hf]
-- 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
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
have neg : Eq.{u_5 + 1} (α := G) (sorry (∑ i ∈ s, μ i) (fun (x : X) ↦ f x) B) (∑ x ∈ s, sorry (μ x) (fun (x : X) ↦ f x) B)
Tactic: simp [integral, hG]