awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
i : ι
hi : i₀ ≤ i
convert_2 :
  ∫ (x : X) in s i₀, f x ∂μ - HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i, f x ∂μ) =
    ∫ (x : X) in s i, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s i, f x ∂μ) = ∫ (x : X) in s i, f x ∂μ
have convert_2₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s i, f x ∂μ) (∫ (x : X) in s i, f x ∂μ)
Tactic: rw [setIntegral_diff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
have suffices : Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
  (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
Tactic: suffices Tendsto (∫ x in s i₀, f x ∂μ - ∫ x in s i₀ \ s ·, f x ∂μ) atTop
      (𝓝 (∫ x in s i₀, f x ∂μ - ∫ x in ⋃ i, s i₀ \ s i, f x ∂μ)) by
    convert! this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_
    · rw [← diff_iInter, setIntegral_diff _ hi₀ (iInter_subset _ _), sub_sub_cancel]
      exact .iInter_of_antitone h_anti hsm
    · rw [setIntegral_diff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
have apply : Tendsto.{u_5, u_3} (β := E) (fun (x : ι) ↦ ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
  (𝓝 (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ))
Tactic: apply tendsto_const_nhds.sub
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (x : ι) ↦ ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ))
have refine_1 : Monotone.{u_5, u_1} (β := Set X) fun (x : ι) ↦ s i₀ \ s x
Tactic: refine tendsto_setIntegral_of_monotone (by measurability) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
refine_1 : Monotone.{u_5, u_1} (β := Set X) fun (x : ι) ↦ s i₀ \ s x
⊢ Tendsto.{u_5, u_3} (β := E) (fun (x : ι) ↦ ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ))
have refine_2 : IntegrableOn f (⋃ (n : ι), s i₀ \ s n) μ
Tactic: refine tendsto_setIntegral_of_monotone (by measurability) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (⋃ (n : ι), s i₀ \ s n) μ
have refine_2 : IntegrableOn f (s i₀ \ ⋂ (i : ι), s i) μ
Tactic: rw [← diff_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : IntegrableOn f (⋃ (i : ι), s i) μ
⊢ HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)
have simp : ∀ (hfi : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ μ.restrict (s i))),
  HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ μ.restrict (s i)) fun (x : X) ↦ f x)
Tactic: simp only [IntegrableOn, Measure.restrict_iUnion_ae hd hm] at hfi ⊢
Cleared hypotheses: hfi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
have pos : ∀ (hf : AEStronglyMeasurable f (μ.restrict t)), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
Tactic: by_cases hf : AEStronglyMeasurable f (μ.restrict t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
pos : ∀ (hf : AEStronglyMeasurable f (μ.restrict t)), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
have neg : ∀ (hf : ¬AEStronglyMeasurable f (μ.restrict t)), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
Tactic: by_cases hf : AEStronglyMeasurable f (μ.restrict t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (μ.restrict t)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
have neg : ¬Integrable f (μ.restrict t)
Tactic: rw [integral_undef]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (μ.restrict t)
⊢ ¬Integrable f (μ.restrict t)
have neg : ∀ (hf : Integrable f (μ.restrict t)), AEStronglyMeasurable f (μ.restrict t)
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0
have refine : AEStronglyMeasurable.mk f hf =ᶠ[ae (μ.restrict t)] 0
Tactic: refine integral_eq_zero_of_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ AEStronglyMeasurable.mk f hf =ᶠ[ae (μ.restrict t)] 0
have rw : ∀ᵐ (x : X) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x
Tactic: rw [EventuallyEq,
      ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x
have h : ∀ (x : X) (hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x) (h'x : x ∈ t → f x = 0) (h''x : x ∈ t),
  AEStronglyMeasurable.mk f hf x = 0 x
Tactic: filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ AEStronglyMeasurable.mk f hf x = 0 x
have h : f x = 0 x
Tactic: rw [← hx h''x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
have this : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0
Tactic: have : ∫ x in t, hf.mk f x ∂μ = 0 := by
    refine integral_eq_zero_of_ae ?_
    rw [EventuallyEq,
      ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]
    filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
    rw [← hx h''x]
    exact h'x h''x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
hU : Ne.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
⊢ ∃ x ∈ t, f x ≠ 0
have contrapose! : ∀ (hU : ∀ (x : X) (_ : x ∈ t), f x = 0), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
Tactic: contrapose! hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
⊢ MeasurableSet k
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have hk : MeasurableSet k
Tactic: have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have h's : IntegrableOn f s μ
Tactic: have h's : IntegrableOn f s μ := H.mono subset_union_left le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
Tactic: have A : ∀ u : Set X, ∫ x in u ∩ k, f x ∂μ = 0 := fun u =>
    setIntegral_eq_zero_of_forall_eq_zero fun x hx => hx.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k ∪ s \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
Tactic: rw [← integral_inter_add_diff hk h's, ← integral_inter_add_diff hk H, A, A, zero_add, zero_add,
    union_diff_distrib, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k ∪ s \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
have hst : t \ k ∪ s \ k =ᶠ[ae μ] s \ k
Tactic: apply setIntegral_congr_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
⊢ t \ k ∪ s \ k =ᶠ[ae μ] s \ k
have hst : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((t \ k) \ (s \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [union_ae_eq_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((t \ k) \ (s \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)
have hst : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null diff_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
have hst : ∀ᵐ (a : X) ∂μ, a ∉ t \ k
Tactic: rw [measure_eq_zero_iff_ae_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
⊢ ∀ᵐ (a : X) ∂μ, a ∉ t \ k
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ t → f x = 0) x} x →
        Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ a ∉ t \ k) x} x}
    a
Tactic: filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ t → f x = 0) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ a ∉ t \ k) x} x}
      a
⊢ ∀ᵐ (a : X) ∂μ, a ∉ t \ k
have h₁ : ∀ (a : X), (a ∈ t → f a = 0) → a ∉ t \ k
Tactic: filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ IntegrableOn f t μ
have apply : (fun (x : X) ↦ 0) =ᶠ[ae (μ.restrict t)] f
Tactic: apply integrableOn_zero.congr_fun_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ (fun (x : X) ↦ 0) =ᶠ[ae (μ.restrict t)] f
have symm : f =ᶠ[ae (μ.restrict t)] fun (x : X) ↦ 0
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have ht : IntegrableOn f t μ
Tactic: have ht : IntegrableOn f t μ := by apply integrableOn_zero.congr_fun_ae; symm; exact ht_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have pos : ∀ (H : IntegrableOn f (s ∪ t) μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: by_cases H : IntegrableOn f (s ∪ t) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
pos : ∀ (H : IntegrableOn f (s ∪ t) μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg : ∀ (H : ¬IntegrableOn f (s ∪ t) μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: by_cases H : IntegrableOn f (s ∪ t) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : ¬IntegrableOn f (s ∪ t) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg : ¬Integrable f (μ.restrict s)
Tactic: rw [integral_undef H, integral_undef]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : IntegrableOn f (s ∪ t) μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)
have integral_union_eq_left_of_ae_aux : ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f sorry x = 0
Tactic: apply
        integral_union_eq_left_of_ae_aux _ H.1.stronglyMeasurable_mk (H.congr_fun_ae H.1.ae_eq_mk)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : IntegrableOn f (s ∪ t) μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f ⋯ x = 0
have h : ∀ (x : X) (hx : f x = 0) (h'x : f x = AEStronglyMeasurable.mk f sorry x), AEStronglyMeasurable.mk f sorry x = 0
Tactic: filter_upwards [ht_eq,
        ae_mono (Measure.restrict_mono subset_union_right le_rfl) H.1.ae_eq_mk] with x hx h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : IntegrableOn f (s ∪ t) μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
x : X
hx : f x = 0
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
h : f x = 0
⊢ AEStronglyMeasurable.mk f ⋯ x = 0
have h₁ : Eq.{u_3 + 1} (α := E) 0 0
Tactic: rw [← h'x, hx]