awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑c : ℝ) * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ ‖f‖ ≤ (↑c : ℝ) * ‖g‖

Tactic:
exact NNReal.coe_le_coe.mpr (nnnorm_le_mul_nnnorm_of_ae_le_mul h)

Premises used: Iff.mpr, MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
hc : c < 0
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0 ∧ eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ = 0

Tactic:
have := eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg h hc p
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
hc : c < 0
this : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ = 0 ∧ eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ = 0
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toReal ≤ c * (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toReal

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ).toReal ≤ (eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) p μ).toReal

Tactic:
exact ENNReal.toReal_mono (by finiteness) (eLpNorm_mono_ae h)

Premises used: MeasureTheory.eLpNorm_mono_ae, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ≥0
f : α →ₘ[μ] E
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑f : α → E) x‖₊ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖₊
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f

Tactic:
mem_Lp_iff_memLp.2 <| MemLp.of_nnnorm_le_mul (Lp.memLp g) f.aestronglyMeasurable h

Premises used: Iff.mpr, MeasureTheory.Lp.memLp, MeasureTheory.Lp.mem_Lp_iff_memLp, MeasureTheory.MemLp.of_nnnorm_le_mul, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
c : ℝ
f : α →ₘ[μ] E
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑f : α → E) x‖ ≤ c * ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f

Tactic:
mem_Lp_iff_memLp.2 <| MemLp.of_le_mul (Lp.memLp g) f.aestronglyMeasurable h

Premises used: Iff.mpr, MeasureTheory.Lp.memLp, MeasureTheory.MemLp.of_le_mul, MeasureTheory.Lp.mem_Lp_iff_memLp, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α →ₘ[μ] E
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑f : α → E) x‖₊ ≤ ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖₊
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f

Tactic:
mem_Lp_iff_memLp.2 <| MemLp.of_le (Lp.memLp g) f.aestronglyMeasurable h

Premises used: Iff.mpr, MeasureTheory.Lp.memLp, MeasureTheory.MemLp.of_le, MeasureTheory.Lp.mem_Lp_iff_memLp, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α →ₘ[μ] E
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖(↑f : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] F) : α → F) x‖
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f

Tactic:
mem_Lp_of_nnnorm_ae_le h

Premises used: MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : α →ₘ[μ] E
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑f : α → E) x‖₊ ≤ C
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f

Tactic:
mem_Lp_iff_memLp.2 <| MemLp.of_bound f.aestronglyMeasurable _ hfC

Premises used: Iff.mpr, MeasureTheory.Lp.mem_Lp_iff_memLp, MeasureTheory.MemLp.of_bound, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : α →ₘ[μ] E
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑f : α → E) x‖ ≤ C
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f

Tactic:
mem_Lp_iff_memLp.2 <| MemLp.of_bound f.aestronglyMeasurable _ hfC

Premises used: Iff.mpr, MeasureTheory.Lp.mem_Lp_iff_memLp, MeasureTheory.MemLp.of_bound, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
pos : ∀ (hμ : μ = 0), ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
neg : ∀ (hμ : ¬μ = 0), ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
simp [hμ, nnnorm_def]

Premises used: MeasureTheory.Lp.nnnorm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (eLpNorm_ne_top _)]

Premises used: ENNReal.coe_toNNReal, MeasureTheory.Lp.nnnorm_def, ENNReal.coe_le_coe, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)

Tactic:
(eLpNorm_le_of_ae_nnnorm_bound hfC).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg :
  C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)

Tactic:
refine (eLpNorm_le_of_ae_nnnorm_bound hfC).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ ≤ C
hμ : ¬μ = 0
neg : C • (↑(measureUnivNNReal μ) : ℝ≥0∞) ^ p.toReal⁻¹ = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₁ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)
neg₂ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) * (↑C : ℝ≥0∞)
neg₃ : C • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) = (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
neg₄ :
  (↑C : ℝ≥0∞) • (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) =
    (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
neg₅ neg₆ :
  (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞) =
    (↑C : ℝ≥0∞) * (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ≥0∞)
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ≥0∞)

Tactic:
rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]

Premises used: MeasureTheory.coe_measureUnivNNReal, ENNReal.smul_def, MeasureTheory.measureUnivNNReal_pos, ENNReal.coe_rpow_of_ne_zero, LT.lt.ne', ENNReal.coe_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ
hC : 0 ≤ C
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ C
⊢ 0 ≤ C

Tactic:
hC
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ
hC : 0 ≤ C
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ C
lift :
  ∀ (C : ℝ≥0) (hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * C

Tactic:
lift C to ℝ≥0 using hC
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
have := nnnorm_le_of_ae_bound hfC
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ (↑C : ℝ)
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
rwa :
  ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C) : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
rwa₁ :
  ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ ^ p.toReal⁻¹) : ℝ) * (↑C : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : (↑‖f‖₊ : ℝ) ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)),
    ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)
⊢ ‖f‖ ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * (↑C : ℝ)

Tactic:
rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this

Premises used: NNReal.coe_rpow, NNReal.coe_mul, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
this : ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
simpa only [ge_iff_le, enorm, ← ENNReal.coe_add, ENNReal.coe_le_coe] using this

Premises used: ge_iff_le, ENNReal.coe_le_coe, ENNReal.coe_add, ENorm.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
suffices : ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
suffices ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ by
            -- Squeezed for performance reasons
            simpa only [ge_iff_le, enorm, ← ENNReal.coe_add, ENNReal.coe_le_coe] using this
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
simp :
  eLpNorm (↑(↑(f + g) : α →ₘ[μ] E) : α → E) p μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ + eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ
⊢ ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ

Tactic:
simp only [Lp.enorm_def]

Premises used: MeasureTheory.Lp.enorm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑(↑(f + g) : α →ₘ[μ] E) : α → E) p μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ + eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ

Tactic:
(eLpNorm_congr_ae (AEEqFun.coeFn_add _ _)).trans_le
            (eLpNorm_add_le (Lp.aestronglyMeasurable _) (Lp.aestronglyMeasurable _) hp.out)

Premises used: MeasureTheory.Lp.aestronglyMeasurable, Eq.trans_le, MeasureTheory.AEEqFun.coeFn_add, MeasureTheory.eLpNorm_add_le, MeasureTheory.eLpNorm_congr_ae, Fact.out
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑(↑(f + g) : α →ₘ[μ] E) : α → E) p μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ + eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ

Tactic:
exact (eLpNorm_congr_ae (AEEqFun.coeFn_add _ _)).trans_le
            (eLpNorm_add_le (Lp.aestronglyMeasurable _) (Lp.aestronglyMeasurable _) hp.out)

Premises used: MeasureTheory.Lp.aestronglyMeasurable, Eq.trans_le, MeasureTheory.AEEqFun.coeFn_add, MeasureTheory.eLpNorm_add_le, MeasureTheory.eLpNorm_congr_ae, Fact.out
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
hp : Fact (1 ≤ p)
⊢ ∀ (r : ↥(Lp E p μ)), ‖-r‖ = ‖r‖

Tactic:
simp only [norm_neg, implies_true]

Premises used: MeasureTheory.Lp.norm_neg, implies_true
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : Fact (1 ≤ p)
⊢ Eq (α := EDist ↥(Lp E p μ)) PseudoEMetricSpace.toEDist instEDist

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : Fact (1 ≤ p)
⊢ Eq (α := EDist ↥(Lp E p μ)) PseudoEMetricSpace.toEDist instEDist

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : Fact (1 ≤ p)
⊢ Eq (α := NNNorm ↥(Lp E p μ)) SeminormedAddGroup.toNNNorm instNNNorm

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : Fact (1 ≤ p)
⊢ Eq (α := NNNorm ↥(Lp E p μ)) SeminormedAddGroup.toNNNorm instNNNorm

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
rw : eLpNorm (c • (↑(↑f : α →ₘ[μ] E) : α → E)) p μ < ∞
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (c • (↑f : α →ₘ[μ] E))

Tactic:
rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_congr_ae (AEEqFun.coeFn_smul _ _)]

Premises used: MeasureTheory.AEEqFun.coeFn_smul, MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ ‖c‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ eLpNorm (c • (↑(↑f : α →ₘ[μ] E) : α → E)) p μ < ∞

Tactic:
exact eLpNorm_const_smul_le.trans_lt <| (by finiteness)

Premises used: MeasureTheory.eLpNorm_const_smul_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedRing 𝕜
inst_3 : NormedRing 𝕜'
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜' E
inst_6 : IsBoundedSMul 𝕜 E
inst_7 : IsBoundedSMul 𝕜' E
c : 𝕜
f : α →ₘ[μ] E
hf :
  Membership.mem (γ := Set (α →ₘ[μ] E))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (Lp E p μ)))) f
⊢ Membership.mem (γ := Set (α →ₘ[μ] E))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (Lp E p μ)))) (c • f)

Tactic:
simpa using const_smul_mem_Lp c ⟨f, hf⟩

Premises used: MeasureTheory.Lp.const_smul_mem_Lp, Subtype.mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
⊢ Eq (α := AddSubgroup (α →ₘ[μ] E))
    (Submodule.toAddSubgroup (module_M := AEEqFun.instModule) (LpSubmodule 𝕜 E p μ : Submodule 𝕜 (α →ₘ[μ] E)))
    (Lp E p μ)

Tactic:
rfl

Premises used: MeasureTheory.Lp, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ (↑(↑(c • f) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] c • (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_smul _ _

Premises used: MeasureTheory.AEEqFun.coeFn_smul
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedRing 𝕜
inst_3 : NormedRing 𝕜'
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜' E
inst_6 : IsBoundedSMul 𝕜 E
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : Fact (1 ≤ p)
r : 𝕜
f : ↥(Lp E p μ)
⊢ ‖r • f‖ₑ ≤ ‖r‖ₑ * ‖f‖ₑ

Tactic:
simpa only [eLpNorm_congr_ae (coeFn_smul _ _), enorm_def]
      using eLpNorm_const_smul_le (c := r) (f := f) (p := p)

Premises used: MeasureTheory.Lp.coeFn_smul, MeasureTheory.eLpNorm_const_smul_le, MeasureTheory.Lp.enorm_def, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : α → E
c : 𝕜
hf : MemLp f p μ
⊢ toLp (c • f) ⋯ = c • toLp f hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ

Tactic:
⟨(hf.1.enorm.pow_const q.toReal).aestronglyMeasurable, ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.MemLp, ENNReal.toReal, And.left, And.intro, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
refine : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ

Tactic:
refine ⟨(hf.1.enorm.pow_const q.toReal).aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
pos : ∀ (q_top : q = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
neg : ∀ (q_top : ¬q = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞

Tactic:
by_cases q_top : q = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : q = ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞

Tactic:
simp [q_top]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
pos : ∀ (q_zero : q = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
neg : ∀ (q_zero : ¬q = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞

Tactic:
by_cases q_zero : q = 0
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
pos : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞

Tactic:
simp only [q_zero, ENNReal.toReal_zero]

Premises used: ENNReal.toReal_zero