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 α
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
⊢ eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ eLpNorm' f p μ * eLpNorm' g q μ

Tactic:
simpa only [eLpNorm', enorm_mul, enorm_norm] using
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm

Premises used: enorm_mul, MeasureTheory.eLpNorm', enorm_norm, MeasureTheory.AEStronglyMeasurable.enorm, ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr
-- 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
eLpNorm' :
  MeasureTheory.eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
    MeasureTheory.eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ
eLpNorm'₁ :
  MeasureTheory.eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ ≤
    (↑c : ℝ≥0∞) * MeasureTheory.eLpNorm' f p μ * MeasureTheory.eLpNorm' g q μ
⊢ MeasureTheory.eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
    (↑c : ℝ≥0∞) * MeasureTheory.eLpNorm' f p μ * MeasureTheory.eLpNorm' g q μ

Tactic:
calc
    eLpNorm' (fun x => b (f x) (g x)) r μ
      ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ := by
      simp only [eLpNorm']
      gcongr ?_ ^ _
      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
      gcongr
      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
      simpa using ha
    _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
      simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
      rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
      gcongr
      simpa only [eLpNorm', enorm_mul, enorm_norm] using
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm

Premises used: Norm.norm, HMul.hMul, MeasureTheory.eLpNorm', HSMul.hSMul, NNReal.toReal
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ 1 / r = 1 / p + 1 / q

Tactic:
have hpqr := hpqr.one_div_eq
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
inl :
  ∀ [hpqr : ENNReal.HolderTriple 0 q r] (hpqr : 1 / r = 1 / 0 + 1 / q),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f 0 μ * eLpNorm g q μ
inr :
  ∀ [hpqr : ENNReal.HolderTriple ∞ q r] (hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g q μ
inr₁ :
  ∀ (hp : 0 < p.toReal),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ

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
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : ENNReal.HolderTriple 0 q r
hpqr : 1 / r = 1 / 0 + 1 / q
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f 0 μ * eLpNorm g q μ

Tactic:
simp_all
-- 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
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : ENNReal.HolderTriple ∞ q r
hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q
⊢ r = q

Tactic:
simpa using hpqr
-- 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
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : ENNReal.HolderTriple ∞ q r
hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q
⊢ r = q

Tactic:
have : r = q := by simpa using hpqr
-- 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
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : ENNReal.HolderTriple ∞ q r
hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q
this : r = q
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g q μ

Tactic:
this ▸ eLpNorm_le_eLpNorm_top_mul_eLpNorm r f hg b c h

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm, Eq.rec
-- 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
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : ENNReal.HolderTriple ∞ q r
hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q
this : r = q
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g q μ

Tactic:
exact this ▸ eLpNorm_le_eLpNorm_top_mul_eLpNorm r f hg b c 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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
inr :
  ∀ [hpqr : p.HolderTriple 0 r] (hpqr : 1 / r = 1 / p + 1 / 0),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g 0 μ
inr₁ :
  ∀ [hpqr : p.HolderTriple ∞ r] (hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ
inr₂ :
  ∀ (hq : 0 < q.toReal),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ

Tactic:
obtain (rfl | rfl | hq) := ENNReal.trichotomy q

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
p r : ℝ≥0∞
hf : AEStronglyMeasurable 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
hpqr_1 : p.HolderTriple 0 r
hpqr : 1 / r = 1 / p + 1 / 0
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g 0 μ

Tactic:
simp_all
-- 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 r : ℝ≥0∞
hf : AEStronglyMeasurable 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
hpqr_1 : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞
⊢ r = p

Tactic:
simpa using hpqr
-- 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 r : ℝ≥0∞
hf : AEStronglyMeasurable 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
hpqr_1 : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞
⊢ r = p

Tactic:
have : r = p := by simpa using hpqr
-- 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 r : ℝ≥0∞
hf : AEStronglyMeasurable 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
hpqr_1 : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞
this : r = p
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ

Tactic:
this ▸ eLpNorm_le_eLpNorm_mul_eLpNorm_top p hf g b c h

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top, Eq.rec, Eq.symm
-- 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 r : ℝ≥0∞
hf : AEStronglyMeasurable 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
hpqr_1 : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞
this : r = p
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ

Tactic:
exact this ▸ eLpNorm_le_eLpNorm_mul_eLpNorm_top p hf g b c 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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ 0 < q

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

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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
⊢ q < ∞

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

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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
⊢ (1 / r).toReal = (1 / p + 1 / q).toReal

Tactic:
have := congr(ENNReal.toReal $(hpqr))
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p + 1 / q).toReal
⊢ 1 / p ≠ ∞

Tactic:
simpa using hp₁.ne'

Premises used: 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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p + 1 / q).toReal
⊢ 1 / q ≠ ∞

Tactic:
simpa using hq₁.ne'

Premises used: 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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p + 1 / q).toReal
⊢ (1 / r).toReal = (1 / p).toReal + (1 / q).toReal

Tactic:
rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this

Premises used: ENNReal.toReal_add
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p).toReal + (1 / q).toReal
⊢ 1 / r.toReal = 1 / p.toReal + 1 / q.toReal

Tactic:
simpa
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
⊢ 1 / r.toReal = 1 / p.toReal + 1 / q.toReal

Tactic:
have hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal := by
    have := congr(ENNReal.toReal $(hpqr))
    rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this
    simpa
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
rw : 0 < 1 / p.toReal + 1 / q.toReal
⊢ 0 < 1 / r.toReal

Tactic:
rw [hpqr']
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
⊢ 0 < 1 / p.toReal + 1 / q.toReal

Tactic:
positivity
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
⊢ 0 < r.toReal

Tactic:
have hr : 0 < r.toReal := one_div_pos.mp <| by rw [hpqr']; positivity
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
⊢ 0 < r

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

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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
⊢ r < ∞

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

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 α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
⊢ 0 < 1 / q.toReal

Tactic:
positivity
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
⊢ r.toReal < p.toReal

Tactic:
have hrp : r.toReal < p.toReal := lt_of_one_div_lt_one_div hp <|
    hpqr' ▸ lt_add_of_pos_right _ (by positivity)