awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_5 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
apply : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn f fmeas s 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
apply tendsto_integral_approxOn_of_measurable hf fmeas _ _ (integrable_zero _ _ _)

Premises used: MeasureTheory.tendsto_integral_approxOn_of_measurable, MeasureTheory.integrable_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_5 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))

Premises used: Set.mem_range_self, subset_closure, Filter.Eventually.of_forall, Set.mem_union_left, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_5 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))

Premises used: Set.mem_range_self, subset_closure, Filter.Eventually.of_forall, Set.mem_union_left, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E_1 : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E_1
inst_1 : NormedDivisionRing 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
G : Type u_5
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace ℝ E_1
f_1 : α → E_1
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_8 : TopologicalSpace X
inst_9 : FirstCountableTopology X
E : Type u_7
inst_10 : NormedAddCommGroup E
inst_11 : MeasurableSpace E
inst_12 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_13 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
x : α
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
⊢ Tendsto (α := ℕ)
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
      ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
    atTop (𝓝 (ENNReal.toReal 0))

Tactic:
(tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_enorm fmeas hf)

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
h :
  ∀ (n : ℕ),
    ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ ∂μ =
      (ENNReal.toReal ∘ fun (n : ℕ) ↦
          ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
        n
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ ∂μ)
    atTop (𝓝 0)

Tactic:
convert! (tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_enorm fmeas hf) with n

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
h :
  (∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ).toReal =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n
h₁ :
  AEStronglyMeasurable.{u_1, u_7} (β := E)
    (fun (x : α) ↦ HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)) μ
⊢ ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ ∂μ =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n

Tactic:
rw [integral_norm_eq_lintegral_enorm]

Premises used: MeasureTheory.integral_norm_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
⊢ (∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ).toReal =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
h : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_7} (β := E)
    (fun (x : α) ↦ HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)) μ

Tactic:
apply (SimpleFunc.aestronglyMeasurable _).sub

Premises used: MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.SimpleFunc.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
apply : IsSeparable (range f)
⊢ AEStronglyMeasurable f μ

Tactic:
apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩).aestronglyMeasurable

Premises used: Iff.mpr, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_iff_measurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
⊢ IsSeparable (range f)

Tactic:
.mono (.of_subtype (range f ∪ {0})) subset_union_left

Premises used: TopologicalSpace.IsSeparable.of_subtype, Set.subset_union_left, TopologicalSpace.IsSeparable.mono, Set.range, Union.union, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
⊢ IsSeparable (range f)

Tactic:
exact .mono (.of_subtype (range f ∪ {0})) subset_union_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
rw : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) - (↑(-f a).toNNReal : ℝ) ∂μ)
rw₁ : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ
⊢ ∫ (a : α), f a ∂μ = HSub.hSub (α := ℝ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ)

Tactic:
rw [← integral_sub hf.real_toNNReal]

Premises used: MeasureTheory.integral_sub, MeasureTheory.Integrable.real_toNNReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) - (↑(-f a).toNNReal : ℝ) ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ

Tactic:
hf.neg.real_toNNReal

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.Integrable.real_toNNReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ

Tactic:
exact hf.neg.real_toNNReal

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.Integrable.real_toNNReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
pos : ∀ (hE : CompleteSpace E), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
neg : ∀ (hE : ¬CompleteSpace E), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : ¬CompleteSpace E
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
pos :
  ∀ (g : α → E) (hg : StronglyMeasurable g) (hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x))
    (hfg : f =ᶠ[ae ν] g), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)

Tactic:
obtain ⟨g, hg, hg_nonneg, hfg⟩ := hfi.1.exists_stronglyMeasurable_range_subset
    isClosed_Ici.measurableSet (Set.nonempty_Ici (a := 0)) hf

Premises used: IsClosed.measurableSet, And.left, Set.nonempty_Ici, MeasureTheory.AEStronglyMeasurable.exists_stronglyMeasurable_range_subset, isClosed_Ici
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
⊢ Integrable g ν

Tactic:
rw [integrable_congr hfg] at hfi

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
hfi₁ : Integrable g ν
⊢ StronglyMeasurable g

Tactic:
rw [integrable_congr hfg] at hfi

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
hfi₁ : Integrable g ν
hg₁ : StronglyMeasurable g
⊢ ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)

Tactic:
rw [integrable_congr hfg] at hfi

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
hfi₁ : Integrable g ν
hg₁ : StronglyMeasurable g
hg_nonneg₁ : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
⊢ f =ᶠ[ae ν] g

Tactic:
rw [integrable_congr hfg] at hfi

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
pos : LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)

Tactic:
simp only [integral_congr_ae hfg, integral_congr_ae (ae_mono hle hfg)]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
⊢ SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)

Tactic:
have _ := hg.separableSpace_range_union_singleton (b := 0)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))

Tactic:
have h₁ := tendsto_integral_approxOn_of_measurable_of_range_subset hg.measurable hfi _ le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
h₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂μ))

Tactic:
have h₂ := tendsto_integral_approxOn_of_measurable_of_range_subset hg.measurable
    (hfi.mono_measure hle) _ le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
h₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂μ))
pos :
  ∀ (x : ℕ),
    SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x) ≤
      SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)

Tactic:
apply le_of_tendsto_of_tendsto' h₂ h₁

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
h₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∀ (x : ℕ),
    SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x) ≤
      SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x)

Tactic:
fun n ↦ SimpleFunc.integral_mono_measure
    (Eventually.of_forall <| SimpleFunc.approxOn_range_nonneg hg_nonneg n) hle
    (SimpleFunc.integrable_approxOn_range _ hfi n)

Premises used: MeasureTheory.StronglyMeasurable.measurable, Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.integral_mono_measure, MeasureTheory.SimpleFunc.integrable_approxOn_range, MeasureTheory.SimpleFunc.approxOn_range_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
h₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∀ (x : ℕ),
    SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x) ≤
      SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x)

Tactic:
exact fun n ↦ SimpleFunc.integral_mono_measure
    (Eventually.of_forall <| SimpleFunc.approxOn_range_nonneg hg_nonneg n) hle
    (SimpleFunc.integrable_approxOn_range _ hfi n)

Premises used: Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.integral_mono_measure, MeasureTheory.SimpleFunc.integrable_approxOn_range, MeasureTheory.SimpleFunc.approxOn_range_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f : α → E
hf : 0 ≤ᶠ[ae μ] f
⊢ LE.le.{u_2} (α := E) 0 (∫ (x : α), f x ∂μ)

Tactic:
integral_eq_setToFun f ▸ setToFun_nonneg (dominatedFinMeasAdditive_weightedSMul μ)
    (fun s _ _ => weightedSMul_nonneg s) hf

Premises used: MeasureTheory.weightedSMul_nonneg, MeasureTheory.setToFun_nonneg, Eq.rec, MeasureTheory.integral_eq_setToFun, Eq.symm, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f : α → E
hf : 0 ≤ f
⊢ LE.le.{u_2} (α := E) 0 (∫ (x : α), f x ∂μ)

Tactic:
integral_nonneg_of_ae (ae_of_all _ hf)

Premises used: MeasureTheory.integral_nonneg_of_ae, MeasureTheory.ae_of_all