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
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 [integral, hG, ← setToFun_neg']
-- 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 : 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 = HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry ν (fun (x : X) ↦ f x) B)
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_sub_vectorMeasure, coe_sub,
      transpose_eq_cbmApplyMeasure, ← setToFun_sub_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 = HSub.hSub (α := 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 : X → E
μ : VectorMeasure X F
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[0; μ] 0
have simp : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) 0) 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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
have pos : sorry μ (fun (x : X) ↦ f x) (B + C) = HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_add_cbm, coe_add, transpose_eq_cbmApplyMeasure,
      ← setToFun_add_measure (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
-- 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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
have neg : sorry μ (fun (x : X) ↦ f x) (B + C) = HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
have pos : ∀ (hG : CompleteSpace G), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
pos :
  ∀ (hG : CompleteSpace G),
    Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
have neg : ∀ (hG : ¬CompleteSpace G), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
have pos : ∀ (hs : s.Nonempty), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
pos : ∀ (hs : s.Nonempty), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
have neg : ∀ (hs : s = ∅), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
hs : s.Nonempty
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
have pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) (∑ i ∈ s, B i)) (∑ x ∈ s, sorry μ (fun (x : X) ↦ f x) (B x))
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_cbm, coe_finsetSum,
        transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
          (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure μ (B i)) 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : ¬CompleteSpace G
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
have neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) (∑ i ∈ s, B i)) (∑ x ∈ s, sorry μ (fun (x : X) ↦ f x) (B x))
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 [integral, hG, ← setToFun_neg']
-- 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 : X → E
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
have pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
have neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
have pos : sorry μ (fun (x : X) ↦ f x) (B - C) = HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
Tactic: simp only [integral, hG, ↓reduceDIte, transpose_sub_cbm, coe_sub,
      transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
-- 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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : ¬CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
have neg : sorry μ (fun (x : X) ↦ f x) (B - C) = HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
Tactic: simp [integral, hG]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (hypothesis)
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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have defQ : let Q := Finpartition.ofPairwiseDisjoint P hP₂;
Q = Finpartition.ofPairwiseDisjoint P hP₂
Tactic: set Q := Finpartition.ofPairwiseDisjoint P hP₂ with defQ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (hypothesis)
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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have defQ' : let Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) sorry sorry;
Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) sorry sorry
Tactic: set Q' := Q.ofSubset (filter_subset MeasurableSet Q.parts) rfl with defQ'
-- 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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
⊢ ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
have simp : ∀ (t : Set X), ¬t = ∅ → t ∈ P → MeasurableSet t → t ⊆ s
Tactic: simp [Q', Q]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (hypothesis)
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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
Tactic: have hQ' : ∀ t ∈ Q'.parts, t ⊆ s := by simp [Q', Q]; grind
-- 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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
⊢ LE.le (α := ℝ≥0∞)
    (∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
        ‖(↑μ : Set X → V) p‖ₑ :
      ℝ≥0∞)
    ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have simp : ∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) sorry).parts (a := s),
    ‖(↑μ : Set X → V) p‖ₑ ≤
  preVariationFun (fun (p : Set X) ↦ ‖(↑μ : Set X → V) p‖ₑ) s
Tactic: simp only [variation_apply, preVariation_apply, ennrealToMeasure_apply hs,
        ennrealPreVariation_apply]