awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
R : Type u_6
inst_2 : NormedRing R
inst_3 : Module R G
inst_4 : IsBoundedSMul R G
inst_5 : SMulCommClass ℝ R G
c : R
f : α → G
hf : Integrable f μ
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
have pos : ∀ (hG : CompleteSpace G), ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
R : Type u_6
inst_2 : NormedRing R
inst_3 : Module R G
inst_4 : IsBoundedSMul R G
inst_5 : SMulCommClass ℝ R G
c : R
f : α → G
hf : Integrable f μ
pos : ∀ (hG : CompleteSpace G), ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
have neg : ∀ (hG : ¬CompleteSpace G), ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
have simp : setToFun μ (weightedSMul μ) sorry f = setToFun μ (weightedSMul μ) sorry g
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), ∫ (b : β), f a b ∂ν ∂μ) (∫ (a : α), ∫ (b : β), g a b ∂ν ∂μ)
have h₁ : EventuallyEq.{u_1, u_5} (β := G) (ae μ) (fun (a : α) ↦ ∫ (b : β), f a b ∂ν) fun (a : α) ↦ ∫ (b : β), g a b ∂ν
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
⊢ EventuallyEq.{u_1, u_5} (β := G) (ae μ) (fun (a : α) ↦ ∫ (b : β), f a b ∂ν) fun (a : α) ↦ ∫ (b : β), g a b ∂ν
have h₁ : ∀ (a : α) (ha : f a =ᶠ[ae ν] g a), Eq.{u_5 + 1} (α := G) (∫ (b : β), f a b ∂ν) (∫ (b : β), g a b ∂ν)
Tactic: filter_upwards [h] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a : α
ha : f a =ᶠ[ae ν] g a
⊢ f a =ᶠ[ae ν] g a
have h₁ : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x →
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x}
    a_1
Tactic: filter_upwards [ha] with _ hb using hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a : α
ha : f a =ᶠ[ae ν] g a
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x}
      a_1
⊢ f a =ᶠ[ae ν] g a
have h₂ : ∀ (a_1 : β), f a a_1 = g a a_1 → f a a_1 = g a a_1
Tactic: filter_upwards [ha] with _ hb using hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), (↑(AEEqFun.mk f ⋯) : α → G) a ∂μ) (∫ (a : α), f a ∂μ)
have simp : setToFun μ (weightedSMul μ) sorry (↑(AEEqFun.mk f sorry) : α → G) = setToFun μ (weightedSMul μ) sorry f
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp G 1 μ)) ↦
    ∫ (a : α), (↑(↑f : α →ₘ[μ] G) : α → G) a ∂μ
have simp : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp G 1 μ)) ↦
  setToFun μ (weightedSMul μ) sorry (↑(↑f : α →ₘ[μ] G) : α → G)
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have simp : ‖setToFun μ (weightedSMul μ) sorry f‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ enorm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
have simp : ‖setToFun μ (weightedSMul μ) sorry f‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ dist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal
have grw : (∫⁻ (a : α), ENNReal.ofReal ‖f a - g a‖ ∂μ).toReal ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal
Tactic: grw [dist_eq_norm, ← integral_sub hf hg, norm_integral_le_lintegral_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ edist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ
have rw : ENNReal.ofReal (dist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ
Tactic: rw [edist_dist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ι) ↦ Norm.norm.{u_5} (E := G) (∫ (x : α) in s x, f x ∂μ)) l (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ι) ↦ Norm.norm.{u_5} (E := G) (∫ (x : α) in s x, f x ∂μ)) l (𝓝 0)
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (a : ι) ↦ (↑(nnnorm.{u_5} (E := G) (∫ (x : α) in s a, f x ∂μ)) : ℝ≥0∞)) l (𝓝 0)
Tactic: simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe,
    ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
have simp : Tendsto (fun (i : ι) ↦ setToFun μ (weightedSMul μ) sorry (F i)) l (𝓝 (setToFun μ (weightedSMul μ) sorry f))
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
have refine : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
Tactic: refine tendsto_integral_of_L1 f hfi hFi ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
have refine_1 : ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)
Tactic: refine tendsto_integral_of_L1 f hfi.restrict ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
refine_1 : ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
have refine_2 : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α) in s, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
Tactic: refine tendsto_integral_of_L1 f hfi.restrict ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Integrable (F i) μ) x} x →
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Integrable (F i) (μ.restrict s)) x} x}
    a
Tactic: filter_upwards [hFi] with i hi using hi.restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Integrable (F i) μ) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Integrable (F i) (μ.restrict s)) x} x}
      a
⊢ ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)
have h₁ : ∀ (a : ι), Integrable (F a) μ → Integrable (F a) (μ.restrict s)
Tactic: filter_upwards [hFi] with i hi using hi.restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α) in s, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
have refine_2 : ∀ (hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 μ) l (𝓝 0)),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 (μ.restrict s)) l (𝓝 0)
Tactic: simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
have refine : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
Tactic: refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s x₀
⊢ ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ ∫ (a : α), F x a ∂μ) s x₀
have simp : ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) sorry (F x)) s x₀
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) x₀
⊢ ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ ∫ (a : α), F x a ∂μ) x₀
have simp : ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) sorry (F x)) x₀
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
s : Set X
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s
⊢ ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ ∫ (a : α), F x a ∂μ) s
have simp : ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) sorry (F x)) s
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ F x a
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ ∫ (a : α), F x a ∂μ
have simp : Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
  setToFun μ (weightedSMul μ) sorry (F x)
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
have rw : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal
Tactic: rw [L1.norm_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal
have e_a : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ
have e_a : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) fun (a : α) ↦
  ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) fun (a : α) ↦
    ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
have h : ∀ (a : α) (h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
  (h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a),
  ENNReal.ofReal (f a) = ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
Tactic: filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1] with _ h₁ h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ ENNReal.ofReal (f a) = ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
have h : (↑(f a).toNNReal : ℝ≥0∞) = ‖max (f a) 0‖ₑ
Tactic: rw [h₁, h₂, ENNReal.ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (↑(f a).toNNReal : ℝ≥0∞) = ‖max (f a) 0‖ₑ
have h : (f a).toNNReal = ‖max (f a) 0‖₊
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (f a).toNNReal = ‖max (f a) 0‖₊
have h : (↑(f a).toNNReal : ℝ) = (↑‖max (f a) 0‖₊ : ℝ)
Tactic: apply NNReal.eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (↑(f a).toNNReal : ℝ) = (↑‖max (f a) 0‖₊ : ℝ)
have h : (↑(f a).toNNReal : ℝ) = (↑(NNReal.mk (max (f a) 0) sorry) : ℝ)
Tactic: rw [Real.nnnorm_of_nonneg (le_max_right _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (↑(f a).toNNReal : ℝ) = (↑(NNReal.mk (max (f a) 0) ⋯) : ℝ)
have h : max (f a) 0 = (↑(NNReal.mk (max (f a) 0) sorry) : ℝ)
Tactic: rw [Real.coe_toNNReal', NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : max (f a) 0 = (↑(NNReal.mk (max (f a) 0) ⋯) : ℝ)
⊢ (↑(f a).toNNReal : ℝ) = (↑(NNReal.mk (max (f a) 0) ⋯) : ℝ)
have h₃ : max (f a) 0 = max (f a) 0
Tactic: rw [Real.coe_toNNReal', NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
have eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
Tactic: have eq₁ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖ := by
    rw [L1.norm_def]
    congr 1
    apply lintegral_congr_ae
    filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1] with _ h₁ h₂
    rw [h₁, h₂, ENNReal.ofReal]
    congr 1
    apply NNReal.eq
    rw [Real.nnnorm_of_nonneg (le_max_right _ _)]
    rw [Real.coe_toNNReal', NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
have rw : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal
Tactic: rw [L1.norm_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal
have e_a : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ
Tactic: congr 1