awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
simp : ‖(↑c : ℝ)‖ₑ * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm_const_smul]

Premises used: smul_mul_assoc, MeasureTheory.eLpNorm_const_smul, Pi.smul_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
rw : (↑c : ℝ≥0∞) * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * (eLpNorm f ∞ μ * eLpNorm g p μ)
⊢ ‖(↑c : ℝ)‖ₑ * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]

Premises used: mul_assoc, NNReal.coe_nonneg, ENNReal.ofReal_coe_nnreal, Real.enorm_eq_ofReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
⊢ (↑c : ℝ≥0∞) * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * (eLpNorm f ∞ μ * eLpNorm g p μ)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) 0 μ ≤ eLpNorm f ∞ μ * eLpNorm g 0 μ
bc₁ : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm f ∞ μ * eLpNorm g ∞ μ
bc₂ : ∀ (hp : 0 < p.toReal), eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
obtain (rfl | rfl | hp) := ENNReal.trichotomy p

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) 0 μ ≤ eLpNorm f ∞ μ * eLpNorm g 0 μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
bc :
  eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤
    eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) ∞ μ * eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖g x‖) ∞ μ
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm f ∞ μ * eLpNorm g ∞ μ

Tactic:
rw [← eLpNorm_norm f, ← eLpNorm_norm g]

Premises used: MeasureTheory.eLpNorm_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
bc :
  essSup (fun (x : α) ↦ ‖f x‖ₑ * ‖g x‖ₑ) μ ≤
    HMul.hMul (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ)
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤
    eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) ∞ μ * eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖g x‖) ∞ μ

Tactic:
simp_rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm, enorm_mul, enorm_norm]

Premises used: enorm_mul, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_eq_essSup_enorm, enorm_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ essSup (fun (x : α) ↦ ‖f x‖ₑ * ‖g x‖ₑ) μ ≤
    HMul.hMul (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ)

Tactic:
ENNReal.essSup_mul_le (‖f ·‖ₑ) (‖g ·‖ₑ)

Premises used: ENorm.enorm, ENNReal.essSup_mul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ essSup (fun (x : α) ↦ ‖f x‖ₑ * ‖g x‖ₑ) μ ≤
    HMul.hMul (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ)

Tactic:
exact ENNReal.essSup_mul_le (‖f ·‖ₑ) (‖g ·‖ₑ)

Premises used: ENorm.enorm, ENNReal.essSup_mul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
⊢ 0 < p

Tactic:
obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp

Premises used: ENNReal.toReal_pos_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
⊢ p < ∞

Tactic:
obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp

Premises used: ENNReal.toReal_pos_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
bc :
  ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp₁.ne' hp₂.ne, eLpNorm_exponent_top,
    eLpNormEssSup, one_div, ENNReal.rpow_inv_le_iff hp, enorm_mul, enorm_norm]

Premises used: enorm_mul, MeasureTheory.eLpNorm_exponent_top, ENNReal.rpow_inv_le_iff, LT.lt.ne', enorm_norm, one_div, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, MeasureTheory.eLpNormEssSup, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖g x‖ₑ ^ p.toReal) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
bc :
  ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) p.toReal * ‖g a‖ₑ ^ p.toReal ∂μ
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal

Tactic:
rw [ENNReal.mul_rpow_of_nonneg (hz := hp.le), ENNReal.rpow_inv_rpow hp.ne',
    ← lintegral_const_mul'' _ (by fun_prop)]

Premises used: ENNReal.rpow_inv_rpow, ENNReal.mul_rpow_of_nonneg, LT.lt.le, LT.lt.ne', MeasureTheory.lintegral_const_mul''
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
bc : ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤ ∫⁻ (a : α), (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal ∂μ
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) p.toReal * ‖g a‖ₑ ^ p.toReal ∂μ

Tactic:
simp only [← ENNReal.mul_rpow_of_nonneg (hz := hp.le)]

Premises used: ENNReal.mul_rpow_of_nonneg, LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
bc : ∀ᵐ (a : α) ∂μ, (‖f a‖ₑ * ‖g a‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤ ∫⁻ (a : α), (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
h₁ :
  ∀ (x : α) (hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) (hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ),
    (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g x‖ₑ) ^ p.toReal
⊢ ∀ᵐ (a : α) ∂μ, (‖f a‖ₑ * ‖g a‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal

Tactic:
filter_upwards [h, enorm_ae_le_eLpNormEssSup f μ] with x hb hf

Premises used: MeasureTheory.enorm_ae_le_eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
x : α
hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ
h₁ : ‖f x‖ₑ ≤ essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
⊢ (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g x‖ₑ) ^ p.toReal

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
x : α
hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ ‖f x‖ₑ ≤ essSup (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
hf

Premises used: MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
x : α
hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ ‖f x‖ₑ ≤ essSup (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
exact hf
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊

Tactic:
h
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
h₁ : ∀ (x : α), c * ‖g x‖₊ * ‖f x‖₊ = c * ‖f x‖₊ * ‖g x‖₊
⊢ ∀ᵐ (x : α) ∂μ, ‖flip b (g x) (f x)‖₊ ≤ c * ‖g x‖₊ * ‖f x‖₊

Tactic:
convert! h using 3 with x
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
x : α
⊢ c * ‖g x‖₊ * ‖f x‖₊ = c * ‖f x‖₊ * ‖g x‖₊

Tactic:
simp only [mul_assoc, mul_comm ‖f x‖₊]

Premises used: NNNorm.nnnorm, mul_assoc, mul_comm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
simp : (↑c : ℝ≥0∞) * (eLpNorm g ∞ μ * eLpNorm f p μ) = (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ)
⊢ (↑c : ℝ≥0∞) * eLpNorm g ∞ μ * eLpNorm f p μ = (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
rw rw₁ : (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ) = (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ)
⊢ (↑c : ℝ≥0∞) * (eLpNorm g ∞ μ * eLpNorm f p μ) = (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ)

Tactic:
rw [mul_comm (eLpNorm _ _ _)]

Premises used: mul_comm, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
simp : (∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ) ^ (1 / r) ≤ (∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ) ^ (1 / r)
⊢ eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
    eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ

Tactic:
simp only [eLpNorm']

Premises used: MeasureTheory.eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
h₁ : ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ
⊢ (∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ) ^ (1 / r) ≤ (∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ) ^ (1 / r)

Tactic:
gcongr ?_ ^ _
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ

Tactic:
lintegral_mono_ae <| h.mono fun a ha ↦ ?_

Premises used: MeasureTheory.lintegral_mono_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
h₁ : ∀ (a : α) (ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊), ‖b (f a) (g a)‖ₑ ^ r ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r
⊢ ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ

Tactic:
refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_

Premises used: MeasureTheory.lintegral_mono_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
a : α
ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊
h₁ : ‖b (f a) (g a)‖ₑ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ
⊢ ‖b (f a) (g a)‖ₑ ^ r ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
a : α
ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊
h₁ : ‖b (f a) (g a)‖₊ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖₊
⊢ ‖b (f a) (g a)‖ₑ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ

Tactic:
simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, enorm_eq_nnnorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
a : α
ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖₊ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖₊

Tactic:
simpa using ha
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
simp : ‖(↑c : ℝ)‖ₑ * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ

Tactic:
simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]

Premises used: smul_mul_assoc, MeasureTheory.eLpNorm'_const_smul, Pi.smul_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
rw : (↑c : ℝ≥0∞) * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * (eLpNorm' f p μ * eLpNorm' g q μ)
⊢ ‖(↑c : ℝ)‖ₑ * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ

Tactic:
rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]

Premises used: mul_assoc, NNReal.coe_nonneg, ENNReal.ofReal_coe_nnreal, Real.enorm_eq_ofReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
bc : eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ eLpNorm' f p μ * eLpNorm' g q μ
⊢ (↑c : ℝ≥0∞) * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * (eLpNorm' f p μ * eLpNorm' g q μ)

Tactic:
gcongr