awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ

Tactic:
eLpNorm_mono_ae ?_

Premises used: MeasureTheory.eLpNorm_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
refine : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ

Tactic:
refine eLpNorm_mono_ae ?_

Premises used: MeasureTheory.eLpNorm_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
h :
  ∀ (x : α) (hx : (↑(↑|f| : α →ₘ[μ] E) : α → E) x ≤ (↑(↑|g| : α →ₘ[μ] E) : α → E) x)
    (hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|)
    (hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|),
    ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖

Tactic:
filter_upwards [hfg, Lp.coeFn_abs f, Lp.coeFn_abs g] with x hx hxf hxg

Premises used: MeasureTheory.Lp.coeFn_abs
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
x : α
hx : (↑(↑|f| : α →ₘ[μ] E) : α → E) x ≤ (↑(↑|g| : α →ₘ[μ] E) : α → E) x
hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|
⊢ |(↑(↑f : α →ₘ[μ] E) : α → E) x| ≤ |(↑(↑g : α →ₘ[μ] E) : α → E) x|

Tactic:
rw [hxf, hxg] at hx
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
x : α
hx : (↑(↑|f| : α →ₘ[μ] E) : α → E) x ≤ (↑(↑|g| : α →ₘ[μ] E) : α → E) x
hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|
hx₁ : |(↑(↑f : α →ₘ[μ] E) : α → E) x| ≤ |(↑(↑g : α →ₘ[μ] E) : α → E) x|
⊢ (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|

Tactic:
rw [hxf, hxg] at hx
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
x : α
hx : (↑(↑|f| : α →ₘ[μ] E) : α → E) x ≤ (↑(↑|g| : α →ₘ[μ] E) : α → E) x
hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|
hx₁ : |(↑(↑f : α →ₘ[μ] E) : α → E) x| ≤ |(↑(↑g : α →ₘ[μ] E) : α → E) x|
hxf₁ : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
⊢ (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|

Tactic:
rw [hxf, hxg] at hx
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
x : α
hx : |(↑(↑f : α →ₘ[μ] E) : α → E) x| ≤ |(↑(↑g : α →ₘ[μ] E) : α → E) x|
hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|
⊢ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖

Tactic:
HasSolidNorm.solid hx

Premises used: HasSolidNorm.solid
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
x : α
hx : |(↑(↑f : α →ₘ[μ] E) : α → E) x| ≤ |(↑(↑g : α →ₘ[μ] E) : α → E) x|
hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|
⊢ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖

Tactic:
exact HasSolidNorm.solid hx

Premises used: HasSolidNorm.solid
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : TopologicalSpace ε
f : α → ε
hfp : MemLp f p μ
⊢ eLpNorm f p μ < ∞

Tactic:
hfp.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : TopologicalSpace ε
f : α → ε
hfp : MemLp f p μ
⊢ eLpNorm f p μ ≠ ∞

Tactic:
hfp.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
rw : eLpNorm' f q μ ^ q < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ∞

Tactic:
rw [lintegral_rpow_enorm_eq_rpow_eLpNorm' hq0_lt]

Premises used: MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
⊢ eLpNorm' f q μ ^ q < ∞

Tactic:
ENNReal.rpow_lt_top_of_nonneg (le_of_lt hq0_lt) (ne_of_lt hfq)

Premises used: le_of_lt, ENNReal.rpow_lt_top_of_nonneg, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
⊢ eLpNorm' f q μ ^ q < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (le_of_lt hq0_lt) (ne_of_lt hfq)

Premises used: le_of_lt, ENNReal.rpow_lt_top_of_nonneg, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
hq0_lt : 0 < p.toReal
hfq : eLpNorm' f p.toReal μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
apply lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top

Premises used: MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
⊢ 0 < p.toReal

Tactic:
ENNReal.toReal_pos hp_ne_zero hp_ne_top

Premises used: ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
⊢ 0 < p.toReal

Tactic:
exact ENNReal.toReal_pos hp_ne_zero hp_ne_top

Premises used: ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
simpa [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top] using hfp

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
⊢ 0 < p.toReal

Tactic:
have hp' := ENNReal.toReal_pos hp_ne_zero hp_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
hp' : 0 < p.toReal
⊢ 0 < 1 / p.toReal

Tactic:
have : 0 < 1 / p.toReal := div_pos zero_lt_one hp'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
hp' : 0 < p.toReal
this : 0 < 1 / p.toReal
⊢ eLpNorm f p μ < ∞

Tactic:
simpa [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top] using
      ENNReal.rpow_lt_top_of_nonneg (le_of_lt this) (ne_of_lt h)

Premises used: le_of_lt, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, ENNReal.rpow_lt_top_of_nonneg, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
rw : (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) ^ (1 / 0) = 1
rw₁ : HPow.hPow (β := ℝ) (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) 0 = 1
rw₂ rw₃ : Eq (α := ℝ≥0∞) 1 1
⊢ eLpNorm' f 0 μ = 1

Tactic:
rw [eLpNorm', div_zero, ENNReal.rpow_zero]

Premises used: MeasureTheory.eLpNorm', ENNReal.rpow_zero, div_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
⊢ eLpNorm f 0 μ = 0

Tactic:
simp [eLpNorm]

Premises used: MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : TopologicalSpace ε
f : α → ε
⊢ MemLp f 0 μ ↔ AEStronglyMeasurable f μ

Tactic:
simp [MemLp, eLpNorm_exponent_zero]

Premises used: MeasureTheory.eLpNorm_exponent_zero, MeasureTheory.MemLp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
hp0_lt : 0 < q
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hp0_lt]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- 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
inl : ∀ (hq0 : 0 ≤ q), eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
inr : ∀ (hq_neg : q < 0), eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0

Tactic:
rcases le_or_gt 0 q with hq0 | hq_neg

Premises used: le_or_gt, OfNat.ofNat
-- 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
hq0 : 0 ≤ q
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0

Tactic:
eLpNorm'_zero (lt_of_le_of_ne hq0 hq0_ne.symm)

Premises used: Ne.symm, MeasureTheory.eLpNorm'_zero, lt_of_le_of_ne
-- 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
hq0 : 0 ≤ q
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0

Tactic:
exact eLpNorm'_zero (lt_of_le_of_ne hq0 hq0_ne.symm)

Premises used: Ne.symm, MeasureTheory.eLpNorm'_zero, lt_of_le_of_ne
-- 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
hq_neg : q < 0
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hμ, hq_neg]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) 0 μ = 0

Tactic:
simp [eLpNormEssSup, ← bot_eq_zero', essSup_const_bot]

Premises used: essSup_const_bot, MeasureTheory.eLpNormEssSup, bot_eq_zero'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
pos : ∀ (h0 : p = 0), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
neg : ∀ (h0 : ¬p = 0), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : p = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
neg : ∀ (h_top : ¬p = ∞), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0

Tactic:
simp only [h_top, eLpNorm_exponent_top, eLpNormEssSup_zero]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ p ≠ 0

Tactic:
rw [← Ne] at h0

Premises used: Ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
h_top : ¬p = ∞
h0₁ : p ≠ 0
⊢ ¬p = ∞

Tactic:
rw [← Ne] at h0

Premises used: Ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top, ENNReal.toReal_pos h0 h_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ eLpNorm.{u_1, u_7} (ε := ε) (fun (x : α) ↦ 0) p μ = 0

Tactic:
eLpNorm_zero

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 ε
rw : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ < ∞

Tactic:
rw [eLpNorm_zero]

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 ε
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ MemLp.{u_1, u_7} (ε := ε) (fun (x : α) ↦ 0) p μ

Tactic:
MemLp.zero

Premises used: MeasureTheory.MemLp.zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
q : ℝ
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : MeasurableSpace α
f : α → ε
hq_pos : 0 < q
⊢ @eLpNorm' _ _ _ inst_2 f q 0 = 0

Tactic:
simp [eLpNorm', hq_pos]

Premises used: MeasureTheory.eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : MeasurableSpace α
f : α → ε
⊢ @eLpNorm' _ _ _ inst_2 f 0 0 = 1

Tactic:
simp [eLpNorm']

Premises used: MeasureTheory.eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
q : ℝ
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : MeasurableSpace α
f : α → ε
hq_neg : q < 0
⊢ @eLpNorm' _ _ _ inst_2 f q 0 = ∞

Tactic:
simp [eLpNorm', hq_neg]

Premises used: MeasureTheory.eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
f : α → ε
⊢ eLpNormEssSup (m0 := m0) f 0 = 0

Tactic:
simp [eLpNormEssSup]

Premises used: MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
pos : ∀ (h0 : p = 0), @eLpNorm _ _ _ m0 f p 0 = 0
neg : ∀ (h0 : ¬p = 0), @eLpNorm _ _ _ m0 f p 0 = 0
⊢ @eLpNorm _ _ _ m0 f p 0 = 0

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : p = 0
⊢ @eLpNorm _ _ _ m0 f p 0 = 0

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), @eLpNorm _ _ _ m0 f p 0 = 0
neg : ∀ (h_top : ¬p = ∞), @eLpNorm _ _ _ m0 f p 0 = 0
⊢ @eLpNorm _ _ _ m0 f p 0 = 0

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : p = ∞
⊢ @eLpNorm _ _ _ m0 f p 0 = 0

Tactic:
simp [h_top]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ p ≠ 0

Tactic:
rw [← Ne] at h0

Premises used: Ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ∞
h0₁ : p ≠ 0
⊢ ¬p = ∞

Tactic:
rw [← Ne] at h0

Premises used: Ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ @eLpNorm _ _ _ m0 f p 0 = 0

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', ENNReal.toReal_pos h0 h_top]

Premises used: MeasureTheory.eLpNorm', MeasureTheory.eLpNorm_eq_eLpNorm', ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
⊢ MemLp (m0 := m0) f p 0

Tactic:
simp [MemLp]

Premises used: MeasureTheory.MemLp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
q : ℝ
μ : Measure α
⊢ eLpNorm' (-f) q μ = eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
pos : ∀ (h0 : p = 0), eLpNorm (-f) p μ = eLpNorm f p μ
neg : ∀ (h0 : ¬p = 0), eLpNorm (-f) p μ = eLpNorm f p μ
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm (-f) p μ = eLpNorm f p μ
neg : ∀ (h_top : ¬p = ∞), eLpNorm (-f) p μ = eLpNorm f p μ
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [h_top, eLpNormEssSup_eq_essSup_enorm]

Premises used: MeasureTheory.eLpNormEssSup_eq_essSup_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (f - g) p μ = eLpNorm (g - f) p μ

Tactic:
simp [← eLpNorm_neg (f := f - g)]

Premises used: HSub.hSub, MeasureTheory.eLpNorm_neg
-- 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 : MemLp f p μ
⊢ eLpNorm (-f) p μ < ∞

Tactic:
simp [hf.right]

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
⊢ MemLp (-f) p μ ↔ MemLp f p μ

Tactic:
⟨fun h => neg_neg f ▸ h.neg, MemLp.neg⟩

Premises used: Eq.rec, neg_neg, MeasureTheory.MemLp.neg, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
⊢ 0 ≤ 1 / q

Tactic:
simp [hq_pos.le]

Premises used: LT.lt.le