awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
pos : ∀ (hp0 : p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
neg : ∀ (hp0 : ¬p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp [hp0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_ne_top c

Premises used: _private.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_ne_top c

Premises used: _private.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
⊢ 0 ≤ p.toReal⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
⊢ 0 ≤ p.toReal⁻¹

Tactic:
have : 0 ≤ p.toReal⁻¹ := by positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
this : 0 ≤ p.toReal⁻¹
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
(eLpNorm_smul_measure_of_ne_top hp ..).trans ?_

Premises used: MeasureTheory.eLpNorm_smul_measure_of_ne_top, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
this : 0 ≤ p.toReal⁻¹
refine : (↑c : ℝ≥0∞) ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
refine (eLpNorm_smul_measure_of_ne_top hp ..).trans ?_

Premises used: MeasureTheory.eLpNorm_smul_measure_of_ne_top, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
this : 0 ≤ p.toReal⁻¹
⊢ (↑c : ℝ≥0∞) ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
simp [ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg, this]

Premises used: ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
rw : c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ
hp_ne_top : Ne (α := ℝ≥0∞) 1 ∞
⊢ eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ

Tactic:
rw [eLpNorm_smul_measure_of_ne_top]

Premises used: MeasureTheory.eLpNorm_smul_measure_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
⊢ c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ MemLp f p μ'

Tactic:
⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.MemLp, MeasureTheory.Measure.absolutelyContinuous_of_le_smul, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
refine : eLpNorm f p μ' < ∞
⊢ MemLp f p μ'

Tactic:
refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ eLpNorm f p μ' < ∞

Tactic:
(eLpNorm_mono_measure f hμ'_le).trans_lt ?_

Premises used: MeasureTheory.eLpNorm_mono_measure, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
refine : eLpNorm f p (c • μ) < ∞
⊢ eLpNorm f p μ' < ∞

Tactic:
refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_

Premises used: MeasureTheory.eLpNorm_mono_measure, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
pos : ∀ (hc0 : c = 0), eLpNorm f p (c • μ) < ∞
neg : ∀ (hc0 : ¬c = 0), eLpNorm f p (c • μ) < ∞
⊢ eLpNorm f p (c • μ) < ∞

Tactic:
by_cases hc0 : c = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : c = 0
⊢ eLpNorm f p (c • μ) < ∞

Tactic:
simp [hc0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : ¬c = 0
neg : c ^ (1 / p).toReal * eLpNorm f p μ < ∞
⊢ eLpNorm f p (c • μ) < ∞

Tactic:
rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul]

Premises used: smul_eq_mul, MeasureTheory.eLpNorm_smul_measure_of_ne_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal * eLpNorm f p μ < ∞

Tactic:
ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2

Premises used: ENNReal.mul_lt_top, And.right, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : ¬c = 0
neg : c ^ (1 / p).toReal ≠ ∞
⊢ c ^ (1 / p).toReal * eLpNorm f p μ < ∞

Tactic:
refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2

Premises used: ENNReal.mul_lt_top, And.right, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal ≠ ∞

Tactic:
simp [hc, hc0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
hf : MemLp f p μ
hc : c ≠ ∞
⊢ MemLp f p (c • μ)

Tactic:
hf.of_measure_le_smul hc le_rfl

Premises used: le_rfl, MeasureTheory.MemLp.of_measure_le_smul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst : ENorm ε
f : α → ε
μ ν : Measure α
simp_rw : ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
⊢ eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst : ENorm ε
f : α → ε
μ ν : Measure α
rw rw₁ : ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
rw [lintegral_add_measure _ μ ν]

Premises used: MeasureTheory.lintegral_add_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ eLpNorm f p (μ + ν)

Tactic:
eLpNorm_mono_measure f <| Measure.le_add_right <| le_refl _

Premises used: le_refl, MeasureTheory.Measure.le_add_right, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p ν ≤ eLpNorm f p (μ + ν)

Tactic:
eLpNorm_mono_measure f <| Measure.le_add_left <| le_refl _

Premises used: le_refl, MeasureTheory.Measure.le_add_left, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : ENorm ε
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → ε
⊢ eLpNormEssSup f μ = ⨆ (a : α), ‖f a‖ₑ

Tactic:
essSup_eq_iSup hμ _

Premises used: essSup_eq_iSup, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst : ENorm ε
inst_1 : MeasurableSingletonClass α
f : α → ε
⊢ eLpNormEssSup (m0 := m0) f Measure.count = ⨆ (a : α), ‖f a‖ₑ

Tactic:
essSup_count _

Premises used: essSup_count, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f p (μ + ν)
⊢ MemLp f p μ

Tactic:
h.mono_measure <| Measure.le_add_right <| le_refl _

Premises used: le_refl, MeasureTheory.MemLp.mono_measure, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f p (μ + ν)
⊢ MemLp f p ν

Tactic:
h.mono_measure <| Measure.le_add_left <| le_refl _

Premises used: le_refl, MeasureTheory.MemLp.mono_measure, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f p μ
simp_rw : eLpNorm f p μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ < ∞

Tactic:
simp_rw [MeasureTheory.eLpNorm_enorm, h.eLpNorm_lt_top]

Premises used: MeasureTheory.eLpNorm_enorm, MeasureTheory.MemLp.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
h : MemLp f p μ
x : α
⊢ ‖‖f x‖‖ ≤ ‖f x‖

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
rw : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [← eLpNorm_enorm]

Premises used: MeasureTheory.eLpNorm_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ < ∞

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ < ∞

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
rw : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [← eLpNorm_norm]

Premises used: MeasureTheory.eLpNorm_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ < ∞

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ < ∞

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
hq0_lt : 0 < q
hf_zero : f =ᶠ[ae μ] 0
rw : eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ eLpNorm' f q μ = 0

Tactic:
rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero hq0_lt]

Premises used: MeasureTheory.eLpNorm'_zero, MeasureTheory.eLpNorm'_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
f : α → ε
hf_zero : f =ᶠ[ae μ] 0
rw : eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ eLpNorm' f q μ = 0

Tactic:
rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero' hq0_ne hμ]

Premises used: MeasureTheory.eLpNorm'_zero', MeasureTheory.eLpNorm'_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
hf : f =ᶠ[ae μ] 0
rw : eLpNorm f p μ = eLpNorm.{u_1, u_7} (ε := ε) 0 p μ
⊢ eLpNorm f p μ = 0

Tactic:
rw [← eLpNorm_zero (p := p) (μ := μ) (α := α) (ε := ε)]

Premises used: MeasureTheory.eLpNorm_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
hf : f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = eLpNorm.{u_1, u_7} (ε := ε) 0 p μ

Tactic:
eLpNorm_congr_ae hf

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
hf : f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = eLpNorm.{u_1, u_7} (ε := ε) 0 p μ

Tactic:
exact eLpNorm_congr_ae hf

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
p : ℝ
hp : 0 < p
hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
rw : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = enorm.{u_7} (E := ε) (0 x)
⊢ eLpNorm' f p μ = 0

Tactic:
rw [← eLpNorm'_zero hp (μ := μ) (ε := ε), eLpNorm'_congr_enorm_ae]

Premises used: MeasureTheory.eLpNorm'_congr_enorm_ae, MeasureTheory.eLpNorm'_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
p : ℝ
hp : 0 < p
hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = enorm.{u_7} (E := ε) (0 x)

Tactic:
simp only [hf, Pi.zero_apply, enorm_zero]

Premises used: Pi.zero_apply, enorm_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : ENorm ε
f : α → ε
⊢ ∀ᵐ (y : α) ∂μ, ‖f y‖ₑ ≤ eLpNormEssSup f μ

Tactic:
ae_le_essSup

Premises used: ae_le_essSup, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
simp_rw : ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (↑x : ℝ≥0∞) ≤ eLpNormEssSup f μ
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x (eLpNormEssSup f μ).toNNReal

Tactic:
simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_le_coe, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (↑x : ℝ≥0∞) ≤ eLpNormEssSup f μ

Tactic:
ae_le_eLpNormEssSup

Premises used: Set.Mem, Filter.Eventually, setOf, NNReal, MeasureTheory.ae_le_eLpNormEssSup, Set.preimage
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (↑x : ℝ≥0∞) ≤ eLpNormEssSup f μ

Tactic:
exact ae_le_eLpNormEssSup

Premises used: MeasureTheory.ae_le_eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hC : ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x C
⊢ eLpNormEssSup f μ < ∞

Tactic:
eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

Premises used: MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hC : ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x C
⊢ eLpNormEssSup f μ < ∞

Tactic:
exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

Premises used: MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : ENorm ε
f : α → ε
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | eLpNormEssSup f μ < ‖f y‖ₑ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
meas_essSup_lt

Premises used: meas_essSup_lt, setOf, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
inl : eLpNorm f 0 μ < ∞
inr : ∀ (hp₀ : p ≠ 0), eLpNorm f p μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
obtain rfl | hp₀ := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
⊢ eLpNorm f 0 μ < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
inr : ∀ (hp₀ : Ne (α := ℝ≥0∞) ∞ 0), eLpNorm f ∞ μ < ∞
inr₁ : ∀ (hp : p ≠ ∞), eLpNorm f p μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
obtain rfl | hp := eq_or_ne p ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : Ne (α := ℝ≥0∞) ∞ 0
inr : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) fun (x : α) ↦ ‖f x‖₊
⊢ eLpNorm f ∞ μ < ∞

Tactic:
simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) fun (x : α) ↦ ‖f x‖₊

Tactic:
.le_of_finite

Premises used: Filter.IsBoundedUnder.le_of_finite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) fun (x : α) ↦ ‖f x‖₊

Tactic:
exact .le_of_finite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
inr : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp]

Premises used: MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_

Premises used: IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal