awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ ε⁻¹ ^ ENNReal.toReal 1 < ∞

Tactic:
simpa only [ENNReal.toReal_one, ENNReal.rpow_one, ENNReal.inv_lt_top, ENNReal.ofReal_pos]
      using hε

Premises used: ENNReal.toReal_one, ENNReal.rpow_one, ENNReal.ofReal_pos, ENNReal.inv_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞

Tactic:
simpa only [ENNReal.toReal_one, ENNReal.rpow_one] using
      (memLp_one_iff_integrable.2 hf).eLpNorm_lt_top

Premises used: Iff.mpr, ENNReal.toReal_one, ENNReal.rpow_one, MeasureTheory.MemLp.eLpNorm_lt_top, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ENNReal.ofReal ε ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Integrable.measure_enorm_ge_lt_top hf (ofReal_pos.mpr hε) ofReal_ne_top

Premises used: Iff.mpr, MeasureTheory.Integrable.measure_enorm_ge_lt_top, ENNReal.ofReal_pos, ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
h : ∀ (x : α), ε ≤ ‖f x‖ ↔ ENNReal.ofReal ε ≤ ‖f x‖ₑ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
convert! Integrable.measure_enorm_ge_lt_top hf (ofReal_pos.mpr hε) ofReal_ne_top with x

Premises used: Iff.mpr, MeasureTheory.Integrable.measure_enorm_ge_lt_top, ENNReal.ofReal_pos, ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
h : ε ≤ ‖f x‖ ↔ ‖ε‖ₑ ≤ ‖f x‖ₑ
h₁ : ε ≤ ‖f x‖ ↔ ‖ε‖ ≤ ‖f x‖
h₂ h₃ : ε ≤ ‖f x‖ ↔ ε ≤ ‖f x‖
⊢ ε ≤ ‖f x‖ ↔ ENNReal.ofReal ε ≤ ‖f x‖ₑ

Tactic:
rw [← Real.enorm_of_nonneg hε.le, enorm_le_iff_norm_le, Real.norm_of_nonneg hε.le]

Premises used: LT.lt.le, enorm_le_iff_norm_le, Real.enorm_of_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
pos : ∀ (hε' : ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
neg : ∀ (hε' : ¬ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_cases hε' : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε = ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hε']
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ¬ε = ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (measure_mono (fun _ h ↦ (Set.mem_setOf_eq ▸ h).le))
    (hf.measure_enorm_ge_lt_top hε hε')

Premises used: MeasureTheory.Integrable.measure_enorm_ge_lt_top, lt_of_le_of_lt, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ¬ε = ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact lt_of_le_of_lt (measure_mono (fun _ h ↦ (Set.mem_setOf_eq ▸ h).le))
    (hf.measure_enorm_ge_lt_top hε hε')

Premises used: MeasureTheory.Integrable.measure_enorm_ge_lt_top, lt_of_le_of_lt, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε < ‖f x‖} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (measure_mono (fun _ h ↦ (Set.mem_setOf_eq ▸ h).le)) (hf.measure_norm_ge_lt_top hε)

Premises used: lt_of_le_of_lt, MeasureTheory.Integrable.measure_norm_ge_lt_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
ε : β
ε_pos : 0 < ε
positivity positivity₁ positivity₂ positivity₃ : ε ≠ 0 → 0 < ‖ε‖
⊢ 0 < ‖ε‖

Tactic:
positivity [ε_pos.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
positivity positivity₁ positivity₂ positivity₃ : c ≠ 0 → 0 < ‖c‖
⊢ 0 < ‖c‖

Tactic:
positivity [c_neg.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
⊢ 0 < ‖c‖

Tactic:
have : 0 < ‖c‖ := by positivity [c_neg.ne]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ c} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (measure_mono fun x hx => ?_) (hf.measure_norm_ge_lt_top this)

Premises used: lt_of_le_of_lt, MeasureTheory.Integrable.measure_norm_ge_lt_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
refine :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x), Membership.mem (γ := Set α) {x : α | ‖c‖ ≤ ‖f x‖} x
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ c} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine lt_of_le_of_lt (measure_mono fun x hx => ?_) (hf.measure_norm_ge_lt_top this)

Premises used: lt_of_le_of_lt, MeasureTheory.Integrable.measure_norm_ge_lt_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
simp : f x ≤ c
⊢ -c ≤ -f x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
⊢ f x ≤ c

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
⊢ -c ≤ -f x

Tactic:
have : -c ≤ -f x := by simp; grind
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this_1 : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
this : -c ≤ -f x
⊢ Membership.mem (γ := Set α) {x : α | ‖c‖ ≤ ‖f x‖} x

Tactic:
norm_le_norm_of_abs_le_abs <| abs_of_nonpos c_neg.le ▸ this.trans (neg_le_abs _)

Premises used: Set.Mem, setOf, norm_le_norm_of_abs_le_abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this_1 : 0 < ‖c‖
x : α
hx : Membership.mem (γ := Set α) {a : α | f a ≤ c} x
this : -c ≤ -f x
⊢ Membership.mem (γ := Set α) {x : α | ‖c‖ ≤ ‖f x‖} x

Tactic:
exact norm_le_norm_of_abs_le_abs <| abs_of_nonpos c_neg.le ▸ this.trans (neg_le_abs _)

Premises used: norm_le_norm_of_abs_le_abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
ε : β
ε_pos : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ε < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (measure_mono (fun _ hx ↦ (Set.mem_setOf_eq ▸ hx).le))
    (Integrable.measure_ge_lt_top hf ε_pos)

Premises used: lt_of_le_of_lt, MeasureTheory.Integrable.measure_ge_lt_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a < c} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (measure_mono (fun _ hx ↦ (Set.mem_setOf_eq ▸ hx).le))
    (Integrable.measure_le_lt_top hf c_neg)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, MeasureTheory.Integrable.measure_le_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
K K' : ℝ≥0
f : α → β
g : β → γ
hg : LipschitzWith K g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ Integrable (g ∘ f) μ ↔ Integrable f μ

Tactic:
simp [← memLp_one_iff_integrable, hg.memLp_comp_iff_of_antilipschitz hg' g0]

Premises used: LipschitzWith.memLp_comp_iff_of_antilipschitz, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
rw : ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ < ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ)) μ

Tactic:
rw [hasFiniteIntegral_iff_norm]

Premises used: MeasureTheory.hasFiniteIntegral_iff_norm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ < ∞

Tactic:
lt_of_le_of_lt ?_ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)

Premises used: lt_of_le_of_lt, Iff.mp, MeasureTheory.hasFiniteIntegral_iff_norm, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine : ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ < ∞

Tactic:
refine lt_of_le_of_lt ?_ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)

Premises used: lt_of_le_of_lt, Iff.mp, MeasureTheory.hasFiniteIntegral_iff_norm, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hfg :
  LE.le.{u_1} (α := α → ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖) fun (a : α) ↦ ENNReal.ofReal ‖f a‖
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Tactic:
apply lintegral_mono

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((fun (a : α) ↦ ENNReal.ofReal ‖(↑(f a).toNNReal : ℝ)‖) x)
    ((fun (a : α) ↦ ENNReal.ofReal ‖f a‖) x)

Tactic:
simp [abs_le, le_abs_self]

Premises used: le_abs_self, abs_le
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
h : ∀ (a : α), f a < ∞ → ENNReal.ofReal (f a).toReal = f a
⊢ (fun (x : α) ↦ ENNReal.ofReal (f x).toReal) =ᶠ[ae μ] f

Tactic:
filter_upwards [hf]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
x : α
hx : f x < ∞
⊢ ENNReal.ofReal (f x).toReal = f x

Tactic:
simp only [hx.ne, ofReal_toReal, Ne, not_false_iff]

Premises used: ENNReal.ofReal_toReal, Ne, not_false_iff, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
h : ∀ (a : α), f a < ∞ → (↑(f a).toNNReal : ℝ≥0∞) = f a
⊢ (fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)) =ᶠ[ae μ] f

Tactic:
filter_upwards [hf]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
x : α
hx : f x < ∞
⊢ (↑(f x).toNNReal : ℝ≥0∞) = f x

Tactic:
simp only [hx.ne, Ne, not_false_iff, coe_toNNReal]

Premises used: ENNReal.coe_toNNReal, Ne, not_false_iff, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
rw : (Summable (α := ℝ) fun (x : α) ↦ ‖f x‖) → AEStronglyMeasurable (m₀ := m) f Measure.count
⊢ @Integrable _ _ _ _ m f Measure.count ↔ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
rw [Integrable, hasFiniteIntegral_count_iff, and_iff_right_iff_imp]

Premises used: MeasureTheory.Integrable, and_iff_right_iff_imp, MeasureTheory.hasFiniteIntegral_count_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
⊢ (Function.support f).Countable

Tactic:
simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
      using hs.countable_support

Premises used: norm_eq_zero, Pi.zero_apply, Ne, eq_comm, Function.support, Summable.countable_support
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
⊢ (Function.support f).Countable

Tactic:
have hs' : (Function.support f).Countable := by
    simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
      using hs.countable_support
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this : MeasurableSpace β := borel β
⊢ BorelSpace β

Tactic:
haveI : BorelSpace β := ⟨rfl⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEStronglyMeasurable (m₀ := m) f Measure.count

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
refine_1 : AEMeasurable (_m := m) f Measure.count
refine_2 : ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t
⊢ AEStronglyMeasurable (m₀ := m) f Measure.count

Tactic:
refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEMeasurable (_m := m) f Measure.count

Tactic:
(measurable_zero.measurable_of_countable_ne ?_).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.measurable_of_countable_ne, measurable_zero
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
refine_1 : Set.Countable.{u_1} (α := α) {x : α | 0 x ≠ f x}
⊢ AEMeasurable (_m := m) f Measure.count

Tactic:
refine (measurable_zero.measurable_of_countable_ne ?_).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.measurable_of_countable_ne, measurable_zero
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ Set.Countable.{u_1} (α := α) {x : α | 0 x ≠ f x}

Tactic:
simpa only [Ne, Pi.zero_apply, eq_comm, Function.support] using hs'

Premises used: Pi.zero_apply, Ne, eq_comm, Function.support
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t

Tactic:
⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩

Premises used: Set.univ, MeasureTheory.ae_of_all, And.intro, Exists.intro, Set.mem_univ, Set.image, rfl
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
refine_2 : IsSeparable (f '' univ)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t

Tactic:
refine ⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
refine_2 : f '' univ ⊆ f '' Function.support f ∪ {0}
⊢ IsSeparable (f '' univ)

Tactic:
suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
      (((hs'.image f).union (countable_singleton 0)).mono this).isSeparable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
inst_1 : MeasurableSingletonClass α
f : α → β
hs : Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
hs' : (Function.support f).Countable
this_1 : MeasurableSpace β := borel β
this : BorelSpace β
⊢ f '' univ ⊆ f '' Function.support f ∪ {0}

Tactic:
grind [Function.mem_support]

Premises used: Function.mem_support
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
pos :
  ∀ (H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ),
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
      Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
neg :
  ∀ (H : ¬AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ),
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
      Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ

Premises used: HSMul.hSMul, NNReal.toReal, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
pos : (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) < ∞ ↔ ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, hasFiniteIntegral_iff_enorm, H,
      true_and]

Premises used: MeasureTheory.Integrable, MeasureTheory.hasFiniteIntegral_iff_enorm, true_and, aestronglyMeasurable_withDensity_iff