awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
⊢ AEStronglyMeasurable (m₀ := mα) f (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa using hf'.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
⊢ MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)

Tactic:
have hf' : MemLp f p (μ .univ • ν) := hf.smul_measure (by simp)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
change : MemLp (f ∘ Prod.snd) p (μ.prod ν)
⊢ MemLp (ε := ε) (fun (x : α × β) ↦ f x.2) p (μ.prod ν)

Tactic:
change MemLp (f ∘ Prod.snd) p (μ.prod ν)

Premises used: Function.comp, MeasureTheory.MemLp, MeasureTheory.Measure.prod, Prod.snd
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
⊢ AEMeasurable Prod.snd (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
rw : MemLp (m0 := mβ) f p (Measure.map Prod.snd (μ.prod ν))
rw₁ : AEStronglyMeasurable (m₀ := mβ) f (Measure.map Prod.snd (μ.prod ν))
⊢ MemLp (f ∘ Prod.snd) p (μ.prod ν)

Tactic:
rw [← memLp_map_measure_iff ?_ (by fun_prop)]

Premises used: MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
⊢ MemLp (m0 := mβ) f p (Measure.map Prod.snd (μ.prod ν))

Tactic:
simpa using hf'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
⊢ AEStronglyMeasurable (m₀ := mβ) f (Measure.map Prod.snd (μ.prod ν))

Tactic:
simpa using hf'.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
c : 𝕜
hq : 0 < q
⊢ eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ

Tactic:
eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul (Eventually.of_forall fun _ => nnnorm_smul_le ..) hq

Premises used: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, Filter.Eventually.of_forall, nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
c : 𝕜
x : α
⊢ ‖(c • f) x‖₊ ≤ ‖c‖₊ * ‖f x‖₊

Tactic:
simp [nnnorm_smul_le]

Premises used: nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
c : 𝕜
x : α
⊢ ‖(c • f) x‖₊ ≤ ‖c‖₊ * ‖f x‖₊

Tactic:
simp [nnnorm_smul_le]

Premises used: nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
hf : MemLp f p μ
c : 𝕜
⊢ MemLp (c • f) p μ

Tactic:
⟨hf.1.const_smul c, eLpNorm_const_smul_le.trans_lt (ENNReal.mul_lt_top ENNReal.coe_lt_top hf.2)⟩

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, MeasureTheory.MemLp, ENNReal.mul_lt_top, MeasureTheory.eLpNorm_const_smul_le, And.right, And.left, And.intro, LE.le.trans_lt, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_3
inst : NormedRing 𝕜
f : α → 𝕜
hf : MemLp f p μ
c : 𝕜
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ c * f x) p μ

Tactic:
hf.const_smul c

Premises used: MeasureTheory.MemLp.const_smul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_3
inst : NormedRing 𝕜
f : α → 𝕜
hf : MemLp f p μ
c : 𝕜
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ f x * c) p μ

Tactic:
hf.const_smul (MulOpposite.op c)

Premises used: MeasureTheory.MemLp.const_smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
m : MeasurableSpace α
q : ℝ
μ : Measure α
𝕜 : Type u_3
inst : NormedRing 𝕜
ε : Type u_4
inst_1 : TopologicalSpace ε
inst_2 : ESeminormedAddMonoid ε
inst_3 : SMul 𝕜 ε
inst_4 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hq : 0 < q
⊢ eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ

Tactic:
eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'
    (Eventually.of_forall fun _ ↦ le_of_eq (enorm_smul ..)) hq

Premises used: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', Filter.Eventually.of_forall, le_of_eq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_3
inst : NormedRing 𝕜
ε : Type u_4
inst_1 : TopologicalSpace ε
inst_2 : ESeminormedAddMonoid ε
inst_3 : SMul 𝕜 ε
inst_4 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
x : α
⊢ ‖(c • f) x‖ₑ ≤ ‖c‖ₑ * ‖f x‖ₑ

Tactic:
simp [enorm_smul]

Premises used: enorm_smul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_3
inst : NormedRing 𝕜
ε : Type u_4
inst_1 : TopologicalSpace ε
inst_2 : ESeminormedAddMonoid ε
inst_3 : SMul 𝕜 ε
inst_4 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
⊢ eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ

Tactic:
eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'
    (Eventually.of_forall fun _ => le_of_eq (enorm_smul ..)) _

Premises used: MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul', Filter.Eventually.of_forall, le_of_eq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_3
inst : NormedRing 𝕜
ε : Type u_4
inst_1 : TopologicalSpace ε
inst_2 : ESeminormedAddMonoid ε
inst_3 : SMul 𝕜 ε
inst_4 : ENormSMulClass 𝕜 ε
f : α → ε
inst_5 : ContinuousConstSMul 𝕜 ε
hf : MemLp f p μ
c : 𝕜
⊢ MemLp (c • f) p μ

Tactic:
⟨hf.1.const_smul c, eLpNorm_const_smul_le'.trans_lt (ENNReal.mul_lt_top ENNReal.coe_lt_top hf.2)⟩

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, MeasureTheory.MemLp, MeasureTheory.eLpNorm_const_smul_le', ENNReal.mul_lt_top, And.right, And.left, And.intro, LE.le.trans_lt, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
inl : eLpNorm' (HSMul.hSMul (α := 𝕜) 0 f) q μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm' f q μ
inr : ∀ (hc : c ≠ 0), eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm' (HSMul.hSMul (α := 𝕜) 0 f) q μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hq_pos]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_

Premises used: le_antisymm, ENNReal.mul_le_of_le_div', MeasureTheory.eLpNorm'_const_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
inr : eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
refine le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_

Premises used: le_antisymm, ENNReal.mul_le_of_le_div', MeasureTheory.eLpNorm'_const_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ

Tactic:
simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul]
    using eLpNorm'_const_smul_le (c := c⁻¹) (f := c • f) hq_pos

Premises used: MeasureTheory.eLpNorm'_const_smul_le, enorm_inv, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
simp_rw : essSup (fun (x : α) ↦ ‖(c • f) x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
simp_rw₁ : essSup (fun (x : α) ↦ ‖c • f x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
simp_rw₂ : essSup (fun (x : α) ↦ ‖c‖ₑ * ‖f x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply, enorm_smul,
    ENNReal.essSup_const_mul]

Premises used: enorm_smul, ENNReal.essSup_const_mul, MeasureTheory.eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
inl : eLpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm f p μ
inr : ∀ (hc : c ≠ 0), eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm f p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
le_antisymm eLpNorm_const_smul_le <| ENNReal.mul_le_of_le_div' ?_

Premises used: MeasureTheory.eLpNorm_const_smul_le, le_antisymm, ENNReal.mul_le_of_le_div'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
inr : eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
refine le_antisymm eLpNorm_const_smul_le <| ENNReal.mul_le_of_le_div' ?_

Premises used: MeasureTheory.eLpNorm_const_smul_le, le_antisymm, ENNReal.mul_le_of_le_div'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ

Tactic:
simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul]
    using eLpNorm_const_smul_le (c := c⁻¹) (f := c • f)

Premises used: MeasureTheory.eLpNorm_const_smul_le, enorm_inv, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
n : ℕ
f : α → F
⊢ eLpNorm (n • f) p μ = (↑n : ℝ≥0∞) * eLpNorm f p μ

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using eLpNorm_const_smul (n : ℝ) f ..

Premises used: Nat.cast, MeasureTheory.eLpNorm_const_smul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
h₁ : ∀ (a : α), ‖(f + g) a‖ₑ ≤ HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a
⊢ (∫⁻ (a : α), ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ^ q ∂μ) ^
      (1 / q)

Tactic:
gcongr with a
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
a : α
⊢ ‖(f + g) a‖ₑ ≤ HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a

Tactic:
simp only [Pi.add_apply, enorm_add_le]

Premises used: Pi.add_apply, enorm_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
h₁ : ∀ (a : α), ‖(f + g) a‖ₑ ≤ HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a
⊢ (∫⁻ (a : α), ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ^ q ∂μ) ^
      (1 / q)

Tactic:
gcongr with a
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
a : α
⊢ ‖(f + g) a‖ₑ ≤ HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a

Tactic:
simp only [Pi.add_apply, enorm_add_le]

Premises used: Pi.add_apply, enorm_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
⊢ eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

Tactic:
le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)

Premises used: ENNReal.essSup_add_le, Filter.Eventually.of_forall, essSup_mono_ae, le_trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
refine :
  ∀ (x : α),
    (fun (x : α) ↦ ‖(f + g) x‖ₑ) x ≤
      HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
⊢ eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

Tactic:
refine le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)

Premises used: ENNReal.essSup_add_le, Filter.Eventually.of_forall, essSup_mono_ae, le_trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
x : α
simp_rw : ‖f x + g x‖ₑ ≤ ‖f x‖ₑ + ‖g x‖ₑ
⊢ (fun (x : α) ↦ ‖(f + g) x‖ₑ) x ≤
    HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x

Tactic:
simp_rw [Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
x : α
⊢ ‖f x + g x‖ₑ ≤ ‖f x‖ₑ + ‖g x‖ₑ

Tactic:
enorm_add_le _ _

Premises used: enorm_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
x : α
⊢ ‖f x + g x‖ₑ ≤ ‖f x‖ₑ + ‖g x‖ₑ

Tactic:
exact enorm_add_le _ _

Premises used: enorm_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
pos : ∀ (hp0 : p = 0), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
neg : ∀ (hp0 : ¬p = 0), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : p = 0
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
simp [hp0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
neg : ∀ (hp_top : ¬p = ∞), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
simp [hp_top, eLpNormEssSup_add_le]

Premises used: MeasureTheory.eLpNormEssSup_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
rwa : ENNReal.toReal 1 ≤ p.toReal
rwa₁ rwa₂ rwa₃ rwa₄ : 1 ≤ p
⊢ 1 ≤ p.toReal

Tactic:
rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]

Premises used: ENNReal.toReal_one, ENNReal.toReal_le_toReal, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ 1 ≤ p.toReal

Tactic:
have hp1_real : 1 ≤ p.toReal := by
    rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm f p μ + eLpNorm g p μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm g p μ
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm g p μ

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'