awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
g : α → ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a
⊢ Integrable f μ

Tactic:
⟨hf, hg.hasFiniteIntegral.mono' h⟩

Premises used: MeasureTheory.HasFiniteIntegral.mono', MeasureTheory.Integrable, And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
ε' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
hf : Integrable f μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ
⊢ Integrable g μ

Tactic:
⟨hg, hf.hasFiniteIntegral.congr'_enorm h⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.congr'_enorm, And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
hf : Integrable f μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖
⊢ Integrable g μ

Tactic:
⟨hg, hf.hasFiniteIntegral.congr' h⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.congr', And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
ε' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ
⊢ Integrable f μ ↔ Integrable g μ

Tactic:
⟨fun h2f => h2f.congr'_enorm hg h, fun h2g => h2g.congr'_enorm hf <| EventuallyEq.symm h⟩

Premises used: Iff.intro, MeasureTheory.Integrable.congr'_enorm, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖
⊢ Integrable f μ ↔ Integrable g μ

Tactic:
integrable_congr'_enorm hf hg <| h.mono fun _x hx ↦ enorm_eq_iff_norm_eq.mpr hx

Premises used: Iff.mpr, Filter.Eventually.mono, enorm_eq_iff_norm_eq, MeasureTheory.integrable_congr'_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f g : α → ε
hf : Integrable f μ
h : f =ᶠ[ae μ] g
⊢ Integrable g μ

Tactic:
⟨hf.1.congr h, hf.2.congr h⟩

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Integrable, And.right, And.left, And.intro, MeasureTheory.HasFiniteIntegral.congr
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f g : α → ε
h : f =ᶠ[ae μ] g
⊢ Integrable f μ ↔ Integrable g μ

Tactic:
⟨fun hf => hf.congr h, fun hg => hg.congr h.symm⟩

Premises used: MeasureTheory.Integrable.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ

Tactic:
have : AEStronglyMeasurable (fun _ : α => c) μ := aestronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
this : AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ
rw :
  AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ ∧
      HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔
    ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
rw₁ : HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
rw₂ rw₃ : ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ

Tactic:
rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff_enorm hc]

Premises used: MeasureTheory.Integrable, and_iff_right, MeasureTheory.hasFiniteIntegral_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
c : β
rw : ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ ↔ c = 0 ∨ IsFiniteMeasure μ
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
rw [integrable_const_iff_enorm enorm_ne_top]

Premises used: MeasureTheory.integrable_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
c : β
⊢ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ 0
hc' : ‖c‖ₑ ≠ ∞
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [integrable_const_iff_enorm hc', hc, isFiniteMeasure_iff]

Premises used: MeasureTheory.isFiniteMeasure_iff, MeasureTheory.integrable_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
c : β
hc : c ≠ 0
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [integrable_const_iff, hc, isFiniteMeasure_iff]

Premises used: MeasureTheory.isFiniteMeasure_iff, MeasureTheory.integrable_const_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
hX : AEMeasurable X μ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ Integrable X μ

Tactic:
⟨hX.aestronglyMeasurable, .of_mem_Icc_of_ne_top ha hb h⟩

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.of_mem_Icc_of_ne_top, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
hX : AEMeasurable X μ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ Integrable X μ

Tactic:
⟨hX.aestronglyMeasurable, .of_mem_Icc a b h⟩

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, MeasureTheory.HasFiniteIntegral.of_mem_Icc, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ

Tactic:
(integrable_const_iff_enorm hc).2 <| .inr ‹_›

Premises used: Iff.mpr, MeasureTheory.integrable_const_iff_enorm, Or.inr
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
c : β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ c) μ

Tactic:
integrable_const_iff.2 <| .inr ‹_›

Premises used: Iff.mpr, MeasureTheory.integrable_const_iff, Or.inr
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Finite α
inst_2 : MeasurableSingletonClass α
inst_3 : IsFiniteMeasure μ
f : α → β
⊢ Integrable f μ

Tactic:
⟨.of_discrete, .of_finite⟩

Premises used: MeasureTheory.HasFiniteIntegral.of_finite, MeasureTheory.Integrable, MeasureTheory.AEStronglyMeasurable.of_discrete, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsEmpty α
f : α → β
⊢ Integrable f μ

Tactic:
.of_finite

Premises used: MeasureTheory.Integrable.of_finite
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Subsingleton α
inst_2 : IsFiniteMeasure μ
f : α → β
⊢ Integrable f μ

Tactic:
.of_finite

Premises used: MeasureTheory.Integrable.of_finite
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ

Tactic:
hf.enorm_rpow hp_ne_zero hp_ne_top

Premises used: MeasureTheory.MemLp.enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ

Tactic:
exact hf.enorm_rpow hp_ne_zero hp_ne_top

Premises used: MeasureTheory.MemLp.enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ

Tactic:
hf.norm_rpow hp_ne_zero hp_ne_top

Premises used: MeasureTheory.MemLp.norm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ

Tactic:
exact hf.norm_rpow hp_ne_zero hp_ne_top

Premises used: MeasureTheory.MemLp.norm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
pos : ∀ (h_zero : p = 0), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
neg : ∀ (h_zero : ¬p = 0), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
by_cases h_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : p = 0
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
simp [h_zero]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
pos : ∀ (h_top : p = ∞), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
neg : ∀ (h_top : ¬p = ∞), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : p = ∞
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
simp [h_top]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : ¬p = ∞
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
hf.integrable_enorm_rpow h_zero h_top

Premises used: MeasureTheory.MemLp.integrable_enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : ¬p = ∞
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
exact hf.integrable_enorm_rpow h_zero h_top

Premises used: MeasureTheory.MemLp.integrable_enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
pos : ∀ (h_zero : p = 0), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
neg : ∀ (h_zero : ¬p = 0), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
by_cases h_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : p = 0
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
simp [h_zero]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
pos : ∀ (h_top : p = ∞), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
neg : ∀ (h_top : ¬p = ∞), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : p = ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
simp [h_top]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : ¬p = ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
hf.integrable_norm_rpow h_zero h_top

Premises used: MeasureTheory.MemLp.integrable_norm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : ¬p = ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
exact hf.integrable_norm_rpow h_zero h_top

Premises used: MeasureTheory.MemLp.integrable_norm_rpow
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p : ℝ≥0∞) μ
hp : p ≠ 0
⊢ Ne (α := ℝ≥0∞) (↑p : ℝ≥0∞) ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p : ℝ≥0∞) μ
hp : p ≠ 0
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p) μ

Tactic:
simpa using hf.integrable_enorm_rpow (mod_cast hp) (by simp)

Premises used: congrArg, cast, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, MeasureTheory.MemLp.integrable_enorm_rpow, Eq.symm, Not, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p : ℝ≥0∞) μ
hp : p ≠ 0
⊢ Ne (α := ℝ≥0∞) (↑p : ℝ≥0∞) ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p : ℝ≥0∞) μ
hp : p ≠ 0
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
simpa using hf.integrable_norm_rpow (mod_cast hp) (by simp)

Premises used: congrArg, cast, Ne, MeasureTheory.MemLp.integrable_norm_rpow, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℕ
hf : MemLp f (↑p : ℝ≥0∞) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p) μ

Tactic:
simpa using hf.integrable_enorm_rpow'

Premises used: MeasureTheory.MemLp.integrable_enorm_rpow'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℕ
hf : MemLp f (↑p : ℝ≥0∞) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
simpa using hf.integrable_norm_rpow'

Premises used: MeasureTheory.MemLp.integrable_norm_rpow'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
rw :
  Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔
    MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
rw₁ :
  MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ ↔
    MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
rw₂ rw₃ :
  MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ

Tactic:
rw [← memLp_enorm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]

Premises used: ENNReal.div_self, MeasureTheory.memLp_enorm_rpow_iff, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
rw : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
rw₁ : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
rw₂ rw₃ : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ

Tactic:
rw [← memLp_norm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]

Premises used: ENNReal.div_self, MeasureTheory.memLp_norm_rpow_iff, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
inl : ∀ (hp : LE.le (α := ℝ) 0 0) (hpq : 0 ≤ q), Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ
inr : ∀ (hp : 0 < p), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
rcases hp.eq_or_lt with (rfl | hp)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
q : ℝ
hq : 0 ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : LE.le (α := ℝ) 0 0
hpq : 0 ≤ q
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
inr :
  ∀ (hq : LE.le (α := ℝ) 0 0) (hpq : p ≤ 0) (hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ),
    Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
inr₁ : ∀ (hq : 0 < q), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
rcases hq.eq_or_lt with (rfl | hq)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p : ℝ
hp_1 : 0 ≤ p
hp : 0 < p
hq : LE.le (α := ℝ) 0 0
hpq : p ≤ 0
hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ ENNReal.ofReal p ≠ 0

Tactic:
simp [hp]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ ENNReal.ofReal p ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
inr : MemLp f (ENNReal.ofReal p) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
rw [← ENNReal.toReal_ofReal hp.le, integrable_norm_rpow_iff hf (by simp [hp]) (by simp)]

Premises used: MeasureTheory.integrable_norm_rpow_iff, LT.lt.le, ENNReal.toReal_ofReal