awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm.{u_1, u_2} (E := E) (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i

Tactic:
lpNorm_sum_le hf hp

Premises used: MeasureTheory.lpNorm_sum_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm.{u_1, u_2} (E := E) (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i

Tactic:
exact lpNorm_sum_le hf hp

Premises used: MeasureTheory.lpNorm_sum_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p μ ≤ lpNorm g p μ
neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm f p μ ≤ lpNorm g p μ
⊢ lpNorm f p μ ≤ lpNorm g p μ

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : AEStronglyMeasurable f μ
pos : (eLpNorm f p μ).toReal ≤ (eLpNorm g p μ).toReal
⊢ lpNorm f p μ ≤ lpNorm g p μ

Tactic:
rw [← toReal_eLpNorm hf, ← toReal_eLpNorm hg.aestronglyMeasurable]

Premises used: MeasureTheory.toReal_eLpNorm, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : AEStronglyMeasurable f μ
⊢ (eLpNorm f p μ).toReal ≤ (eLpNorm g p μ).toReal

Tactic:
ENNReal.toNNReal_mono (hg.eLpNorm_ne_top) (eLpNorm_mono_real h)

Premises used: MeasureTheory.eLpNorm_mono_real, ENNReal.toNNReal_mono, ENNReal.toReal, NNReal.toReal, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : AEStronglyMeasurable f μ
⊢ (eLpNorm f p μ).toReal ≤ (eLpNorm g p μ).toReal

Tactic:
exact ENNReal.toNNReal_mono (hg.eLpNorm_ne_top) (eLpNorm_mono_real h)

Premises used: MeasureTheory.eLpNorm_mono_real, ENNReal.toNNReal_mono, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm f p μ ≤ lpNorm g p μ

Tactic:
simp [hf]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : AEStronglyMeasurable f μ
pos : (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
simp [← toReal_eLpNorm, hf, hf.smul_measure, eLpNorm_smul_measure_of_ne_zero' hc f p μ]

Premises used: MeasureTheory.AEStronglyMeasurable.smul_measure, MeasureTheory.toReal_eLpNorm, MeasureTheory.eLpNorm_smul_measure_of_ne_zero'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : AEStronglyMeasurable f μ
⊢ (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal

Tactic:
simp [ENNReal.smul_def, NNReal.smul_def]

Premises used: ENNReal.smul_def, NNReal.smul_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ

Tactic:
simpa [hc] using h.smul_measure c⁻¹

Premises used: MeasureTheory.AEStronglyMeasurable.smul_measure, Inv.inv
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
neg : 0 = HSMul.hSMul (β := ℝ) (c ^ p.toReal⁻¹) 0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
      simpa [hc] using h.smul_measure c⁻¹]

Premises used: MeasureTheory.lpNorm_of_not_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = HSMul.hSMul (β := ℝ) (c ^ p.toReal⁻¹) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : AEStronglyMeasurable f μ
pos : (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
simp [← toReal_eLpNorm, hf, hf.smul_measure, eLpNorm_smul_measure_of_ne_top' hp]

Premises used: MeasureTheory.eLpNorm_smul_measure_of_ne_top', MeasureTheory.AEStronglyMeasurable.smul_measure, MeasureTheory.toReal_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : AEStronglyMeasurable f μ
⊢ (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal

Tactic:
simp [ENNReal.smul_def, NNReal.smul_def]

Premises used: ENNReal.smul_def, NNReal.smul_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
neg : ∀ (hp : Ne (α := ℝ≥0∞) 0 ∞), lpNorm f 0 (c • μ) = c ^ (ENNReal.toReal 0)⁻¹ • lpNorm f 0 μ
neg₁ : ∀ (hp₀ : p ≠ 0), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp : Ne (α := ℝ≥0∞) 0 ∞
⊢ lpNorm f 0 (c • μ) = c ^ (ENNReal.toReal 0)⁻¹ • lpNorm f 0 μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
neg : lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HPow.hPow (α := ℝ≥0) 0 p.toReal⁻¹ • lpNorm f p μ
neg₁ : ∀ (hc : c ≠ 0), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
⊢ p.toReal⁻¹ ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, *]

Premises used: ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
neg : lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HSMul.hSMul (α := ℝ≥0) 0 (lpNorm f p μ)
⊢ lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HPow.hPow (α := ℝ≥0) 0 p.toReal⁻¹ • lpNorm f p μ

Tactic:
rw [NNReal.zero_rpow (by simp [ENNReal.toReal_eq_zero_iff, *])]

Premises used: NNReal.zero_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
⊢ lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HSMul.hSMul (α := ℝ≥0) 0 (lpNorm f p μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ

Tactic:
simpa [hc] using h.smul_measure c⁻¹

Premises used: MeasureTheory.AEStronglyMeasurable.smul_measure, Inv.inv
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
neg : 0 = HSMul.hSMul (β := ℝ) (c ^ p.toReal⁻¹) 0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
    simpa [hc] using h.smul_measure c⁻¹]

Premises used: MeasureTheory.lpNorm_of_not_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
⊢ 0 = HSMul.hSMul (β := ℝ) (c ^ p.toReal⁻¹) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
pos :
  ∀ (hf : AEStronglyMeasurable f μ),
    lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
neg :
  ∀ (hf : ¬AEStronglyMeasurable f μ),
    lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
pos :
  lpNorm (E := ℝ) (fun (x : α) ↦ norm.{u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f x : K)) p μ =
    lpNorm (E := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
pos₁ : AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ

Tactic:
rw [← lpNorm_norm hf, ← lpNorm_norm]

Premises used: MeasureTheory.lpNorm_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ lpNorm (E := ℝ) (fun (x : α) ↦ norm.{u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f x : K)) p μ =
    lpNorm (E := ℝ) (fun (x : α) ↦ ‖f x‖) p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ

Tactic:
(continuous_star.measurable.comp_aemeasurable hf.aemeasurable).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, ContinuousStar.continuous_star, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ

Tactic:
exact (continuous_star.measurable.comp_aemeasurable hf.aemeasurable).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, ContinuousStar.continuous_star, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
rw :
  ∀ (h : AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ),
    AEStronglyMeasurable f μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf ?_]

Premises used: MeasureTheory.lpNorm_of_not_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa [Function.comp_def]
      using (continuous_star.measurable.comp_aemeasurable h.aemeasurable).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, ContinuousStar.continuous_star, Function.comp_def, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
rw : ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.smul_def, smul_eq_mul,
    ENNReal.mul_rpow_of_nonneg _ _ hp.le]

Premises used: ENNReal.smul_def, ENNReal.mul_rpow_of_nonneg, LT.lt.le, ENNReal.rpow_le_rpow_iff, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
simp_rw : ∫⁻ (a : α), (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞) ∂μ
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one, enorm,
    ← ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top,
    ← ENNReal.coe_mul]

Premises used: ENNReal.rpow_mul, MeasureTheory.lintegral_const_mul', ENNReal.rpow_one, ENNReal.coe_rpow_of_nonneg, LT.lt.le, LT.lt.ne', ENNReal.coe_mul, ENorm.enorm, one_div, inv_mul_cancel₀, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
h₁ : ∀ᵐ (a : α) ∂μ, (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞)
⊢ ∫⁻ (a : α), (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞) ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
h₁ : ∀ (x : α) (hx : ‖f x‖₊ ≤ c * ‖g x‖₊), (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g x‖₊ ^ p) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ, (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞)

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
x : α
hx : ‖f x‖₊ ≤ c * ‖g x‖₊
h₁ : (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑((c * ‖g x‖₊) ^ p) : ℝ≥0∞)
⊢ (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g x‖₊ ^ p) : ℝ≥0∞)

Tactic:
rw [← NNReal.mul_rpow]

Premises used: NNReal.mul_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
x : α
hx : ‖f x‖₊ ≤ c * ‖g x‖₊
h₁ : 0 ≤ p
⊢ (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑((c * ‖g x‖₊) ^ p) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
rw : ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.smul_def, smul_eq_mul,
    ENNReal.mul_rpow_of_nonneg _ _ hp.le]

Premises used: ENNReal.smul_def, ENNReal.mul_rpow_of_nonneg, LT.lt.le, ENNReal.rpow_le_rpow_iff, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
simp_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p ∂μ
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one,
    ← ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top]

Premises used: ENNReal.rpow_mul, MeasureTheory.lintegral_const_mul', ENNReal.rpow_one, ENNReal.coe_rpow_of_nonneg, LT.lt.le, LT.lt.ne', one_div, inv_mul_cancel₀, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
h₁ : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
x : α
linarith : p < 0 → 0 - p + (p - 0) = 0
⊢ ¬p < 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
x : α
⊢ ¬p < 0

Tactic:
have : ¬(p < 0) := by linarith
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
x : α
this : ¬p < 0
⊢ (↑c : ℝ≥0∞) ^ p * ‖g x‖ₑ ^ p = ((↑c : ℝ≥0∞) * ‖g x‖ₑ) ^ p

Tactic:
simp [ENNReal.mul_rpow_eq_ite, this]

Premises used: ENNReal.mul_rpow_eq_ite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ ∀ (x : α), (↑c : ℝ≥0∞) ^ p * ‖g x‖ₑ ^ p = ((↑c : ℝ≥0∞) * ‖g x‖ₑ) ^ p

Tactic:
have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by
    have : ¬(p < 0) := by linarith
    simp [ENNReal.mul_rpow_eq_ite, this]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ
hp : 0 < p
aux : ∀ (x : α), (↑c : ℝ≥0∞) ^ p * ‖g x‖ₑ ^ p = ((↑c : ℝ≥0∞) * ‖g x‖ₑ) ^ p
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg _ hp.le, aux, ENNReal.rpow_le_rpow_iff hp]

Premises used: ENNReal.coe_rpow_of_nonneg, LT.lt.le, ENNReal.rpow_le_rpow_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
linarith : p < 0 → 0 - p + (p - 0) = 0
⊢ ¬p < 0

Tactic:
linarith