awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have hg_ae : EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
  (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
Tactic: have hg_ae := g.coeFn_toLp 2 μ 𝕜
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have h : ∀ (a : α)
  (hf :
    Eq.{u_2 + 1} (α := 𝕜)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
      ((f : (a : α) → 𝕜) a : 𝕜))
  (hg :
    Eq.{u_2 + 1} (α := 𝕜)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
      ((g : (a : α) → 𝕜) a : 𝕜)),
  inner 𝕜 (E := 𝕜) ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
Tactic: filter_upwards [hf_ae, hg_ae] with _ hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
a : α
hf :
  Eq.{u_2 + 1} (α := 𝕜)
    ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((f : (a : α) → 𝕜) a : 𝕜)
hg :
  Eq.{u_2 + 1} (α := 𝕜)
    ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((g : (a : α) → 𝕜) a : 𝕜)
⊢ inner 𝕜 (E := 𝕜) ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have h : inner 𝕜 (E := 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) =
  HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
⊢ inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) ((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f : ↥(Lp 𝕜 2 μ))
      ((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g : ↥(Lp 𝕜 2 μ)) =
    ∫ (x : α),
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) x : 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) : 𝕜) ∂μ
have h : EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
  (fun (a : α) ↦
    inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
  fun (a : α) ↦
  HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have hf_ae : EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
  (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
Tactic: have hf_ae := f.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have hg_ae : EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
  (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
Tactic: have hg_ae := g.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have h : ∀ (a : α)
  (hf :
    Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
      ((f : (a : α) → 𝕜) a : 𝕜))
  (hg :
    Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
      ((g : (a : α) → 𝕜) a : 𝕜)),
  inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
Tactic: filter_upwards [hf_ae, hg_ae] with _ hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
a : α
hf :
  Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((f : (a : α) → 𝕜) a : 𝕜)
hg :
  Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((g : (a : α) → 𝕜) a : 𝕜)
⊢ inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have h : inner 𝕜 (E := 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) =
  HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
x : X
hx : x ∈ s
⊢ IntegrableAtFilter g (𝓝[s] x) μ
have rcases : ∀ (t : Set X) (t_mem : t ∈ 𝓝[s] x) (ht : IntegrableOn f t μ), IntegrableAtFilter g (𝓝[s] x) μ
Tactic: rcases hf x hx with ⟨t, t_mem, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
⊢ IntegrableAtFilter g (𝓝[s] x) μ
have rcases : ∀ (t : Set X) (t_mem : t ∈ 𝓝[s] x) (ht : IntegrableOn f t μ), IntegrableAtFilter g (𝓝[s] x) μ
Tactic: rcases hf x hx with ⟨t, t_mem, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) ν
have obtain : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x) (hf : IntegrableOn f t μ), IntegrableAtFilter f (𝓝[s] x) ν
Tactic: obtain ⟨t, ht, hf⟩ := hf x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
⊢ IntegrableAtFilter f (𝓝[s] x) ν
have obtain : ∀ (u : Set X) (hu : IsOpen[inst_1] u) (hxu : x ∈ u) (hut : u ∩ s ⊆ t), IntegrableAtFilter f (𝓝[s] x) ν
Tactic: obtain ⟨u, hu, hxu, hut⟩ := mem_nhdsWithin.mp ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
⊢ IntegrableAtFilter f (𝓝[s] x) ν
have refine : IntegrableOn f (u ∩ s) ν
Tactic: refine ⟨u ∩ s, inter_mem (mem_nhdsWithin.mpr ⟨u, hu, hxu, inter_subset_left⟩) self_mem_nhdsWithin,
    ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
⊢ IntegrableOn f (u ∩ s) ν
have refine : ν.restrict (u ∩ s) ≤ μ.restrict (u ∩ s)
Tactic: refine hf.mono_set hut |>.mono_measure' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
⊢ ν.restrict (u ∩ s) ≤ μ.restrict (u ∩ s)
have simp_rw : (ν.restrict s).restrict u ≤ (μ.restrict s).restrict u
Tactic: simp_rw [← restrict_restrict hu.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
⊢ IntegrableAtFilter g (𝓝[s] x) μ
have obtain : ∀ (t : Set X) (hxt : t ∈ 𝓝[s] x) (hft : IntegrableOn f t μ), IntegrableAtFilter g (𝓝[s] x) μ
Tactic: obtain ⟨t, hxt, hft⟩ := hf x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ
have refine : IntegrableOn g (s ∩ t) μ
Tactic: refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin hxt, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ IntegrableOn g (s ∩ t) μ
have refine : f =ᶠ[ae (μ.restrict (s ∩ t))] g
Tactic: refine (hft.mono_set inter_subset_right).congr ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ f =ᶠ[ae (μ.restrict (s ∩ t))] g
have refine : ae (μ.restrict (s ∩ t)) ≤ ae (μ.restrict s)
Tactic: refine h.filter_mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ ae (μ.restrict (s ∩ t)) ≤ ae (μ.restrict s)
have h₁ : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
have rcases : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x) (h't : IntegrableOn f t μ),
  ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
Tactic: rcases hf x hx with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
h't : IntegrableOn f t μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
have rcases : ∀ (u : Set X) (u_open : IsOpen[inst_1] u) (x_mem : x ∈ u) (u_sub : u ∩ s ⊆ t),
  ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
Tactic: rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
have this : ∀ (x : (↑s : Type u_1)), ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑x : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
Tactic: have : ∀ x : s, ∃ u, IsOpen u ∧ x.1 ∈ u ∧ IntegrableOn f (u ∩ s) μ := by
    rintro ⟨x, hx⟩
    rcases hf x hx with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩
    exact ⟨u, u_open, x_mem, h't.mono_set u_sub⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
this : ∀ (x : (↑s : Type u_1)), ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑x : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
have choose : ∀ (u : (x : (↑s : Type u_1)) → Set X) (u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x))
  (xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x) (hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ),
  ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
Tactic: choose u u_open xu hu using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
⊢ ∃ (T : Set (↑s : Type u_1)), T.Countable ∧ s ⊆ ⋃ i ∈ T, u i
have this : s ⊆ ⋃ (x : (↑s : Type u_1)), u x
Tactic: have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ (x : (↑s : Type u_1)), u x
⊢ ∃ (T : Set (↑s : Type u_1)), T.Countable ∧ s ⊆ ⋃ i ∈ T, u i
have obtain : ∀ (T : Set (↑s : Type u_1)) (hT_count : T.Countable)
  (hT_un : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ T, u i) (⋃ (i : (↑s : Type u_1)), u i)),
  ∃ (T : Set (↑s : Type u_1)), T.Countable ∧ s ⊆ ⋃ i ∈ T, u i
Tactic: obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
have obtain : ∀ (T : Set (↑s : Type u_1)) (T_count : T.Countable) (hT : s ⊆ ⋃ i ∈ T, u i),
  ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
Tactic: obtain ⟨T, T_count, hT⟩ : ∃ T : Set s, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i := by
    have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
    obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
    exact ⟨T, hT_count, by rwa [hT_un]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
have refine_1 : ∀ u_1 ∈ u '' T, IsOpen[inst_1] u_1
Tactic: refine ⟨u '' T, T_count.image _, ?_, by rwa [biUnion_image], ?_⟩