awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn f s μ
have refine : HasFiniteIntegral f (μ.restrict s)
Tactic: refine ⟨hf.aestronglyMeasurable_of_subset_isCompact hK hs h's, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HasFiniteIntegral f (μ.restrict s)
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ s < ∞) := ⟨mus.lt_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ HasFiniteIntegral f (μ.restrict s)
have obtain : ∀ (C : ℝ) (hC : ∀ x ∈ f '' K, ‖x‖ ≤ C), HasFiniteIntegral f (μ.restrict s)
Tactic: obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
    IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ HasFiniteIntegral f (μ.restrict s)
have apply : ∀ᵐ (a : X) ∂μ.restrict s, ‖f a‖ ≤ C
Tactic: apply HasFiniteIntegral.of_bounded (C := C)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.restrict s, ‖f a‖ ≤ C
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ s) x} x →
        Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ ‖f a‖ ≤ C) x} x}
    a
Tactic: filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ s) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ ‖f a‖ ≤ C) x} x}
      a
⊢ ∀ᵐ (a : X) ∂μ.restrict s, ‖f a‖ ≤ C
have h₁ : ∀ a ∈ s, ‖f a‖ ≤ C
Tactic: filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
⊢ MemLp f ∞ (μ.restrict s)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MemLp f ∞ (μ.restrict s)
have hbelow : BddBelow (f '' s)
Tactic: have hbelow : BddBelow (f '' s) := ⟨f a, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono ha.1 hy (ha.2 hy)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hbelow : BddBelow (f '' s)
⊢ MemLp f ∞ (μ.restrict s)
have habove : BddAbove (f '' s)
Tactic: have habove : BddAbove (f '' s) := ⟨f b, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono hy hb.1 (hb.2 hy)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
⊢ MemLp f ∞ (μ.restrict s)
have this : Bornology.IsBounded (f '' s)
Tactic: have : IsBounded (f '' s) := Metric.isBounded_of_bddAbove_of_bddBelow habove hbelow
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
⊢ MemLp f ∞ (μ.restrict s)
have rcases : ∀ (C : ℝ) (hC : ∀ x ∈ f '' s, ‖x‖ ≤ C), MemLp f ∞ (μ.restrict s)
Tactic: rcases isBounded_iff_forall_norm_le.mp this with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
⊢ MemLp f ∞ (μ.restrict s)
have A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
Tactic: have A : MemLp (fun _ => C) ⊤ (μ.restrict s) := memLp_top_const _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
⊢ MemLp f ∞ (μ.restrict s)
have apply : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖
Tactic: apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖
have apply : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ ‖C‖
Tactic: apply (ae_restrict_iff' h's).mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ ‖C‖
have apply : ∀ (y : X) (hy : y ∈ s), ‖f y‖ ≤ ‖C‖
Tactic: apply ae_of_all _ fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
⊢ MemLp f p (μ.restrict s)
have inl : ∀ (hs : IsCompact.{u_1} (X := X) ∅) (hmono : MonotoneOn f ∅), MemLp f p (μ.restrict ∅)
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs, hmono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
inl : ∀ (hs : IsCompact.{u_1} (X := X) ∅) (hmono : MonotoneOn f ∅), MemLp f p (μ.restrict ∅)
⊢ MemLp f p (μ.restrict s)
have inr : ∀ (h : s.Nonempty), MemLp f p (μ.restrict s)
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
⊢ IntegrableAtFilter f (𝓝 x) μ
have rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 x) (h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)),
  IntegrableAtFilter f (𝓝 x) μ
Tactic: rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableAtFilter f (𝓝 x) μ
have obtain : ∀ (a b : X) (xab : x ∈ Icc a b) (hab : Icc a b ∈ 𝓝 x) (abU : Icc a b ⊆ U), IntegrableAtFilter f (𝓝 x) μ
Tactic: obtain ⟨a, b, xab, hab, abU⟩ : ∃ a b : X, x ∈ Icc a b ∧ Icc a b ∈ 𝓝 x ∧ Icc a b ⊆ U :=
    exists_Icc_mem_subset_of_mem_nhds hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
⊢ IntegrableAtFilter f (𝓝 x) μ
have ab : a ≤ b
Tactic: have ab : a ≤ b := xab.1.trans xab.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableAtFilter f (𝓝 x) μ
have refine : IntegrableOn f (Icc a b) μ
Tactic: refine ⟨Icc a b, hab, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : IntegrableOn g A μ
hg' : ContinuousOn g' K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ
have rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖g' x‖ ≤ C), IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ
Tactic: rcases IsCompact.exists_bound_of_continuousOn hK hg' with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
A K : Set X
inst_3 : NormedRing R
inst_4 : SecondCountableTopologyEither X R
g g' : X → R
hg : ContinuousOn g K
hg' : IntegrableOn g' A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
⊢ IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ
have rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖g x‖ ≤ C), IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * g' x) A μ
Tactic: rcases IsCompact.exists_bound_of_continuousOn hK hg with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X 𝕜
f : X → 𝕜
hf : ContinuousOn f K
g : X → E
hg : IntegrableOn g A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ
have rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖f x‖ ≤ C), IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ
Tactic: rcases IsCompact.exists_bound_of_continuousOn hK hf with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : SecondCountableTopologyEither X E
f : X → 𝕜
hf : IntegrableOn f A μ
g : X → E
hg : ContinuousOn g K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
⊢ IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ
have rcases : ∀ (C : ℝ) (hC : ∀ x ∈ K, ‖g x‖ ≤ C), IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) A μ
Tactic: rcases IsCompact.exists_bound_of_continuousOn hK hg with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * f x) s μ
have rw : ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s),
  ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ g x * f x) k μ
Tactic: rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
Cleared hypotheses: hf, hg, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
R : Type u_8
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
inst_3 : LocallyCompactSpace X
inst_4 : T2Space X
inst_5 : NormedRing R
inst_6 : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ f x * g x) s μ
have rw : ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s),
  ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_8} (ε := R) (fun (x : X) ↦ f x * g x) k μ
Tactic: rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
Cleared hypotheses: hf, hg, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X 𝕜
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ g x • f x) s μ
have rw : ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s),
  ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ g x • f x) k μ
Tactic: rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X E
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) s μ
have rw : ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (hg : ContinuousOn g s),
  ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) k μ
Tactic: rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f g : ↥(Lp E p μ)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔ f ≤ g
have rw : (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔ (↑f : α →ₘ[μ] E) ≤ (↑g : α →ₘ[μ] E)
Tactic: rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f g : ↥(Lp E p μ)
rw : (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔ (↑f : α →ₘ[μ] E) ≤ (↑g : α →ₘ[μ] E)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔ f ≤ g
have rw₁ : (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔
  (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)
Tactic: rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ 0 ≤ f
have rw : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: rw [← coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
have h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
Tactic: have h0 := Lp.coeFn_zero E p μ