awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]

Premises used: ENNReal.rpow_eq_zero_iff, one_div, Finset.sum_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞)
⊢ (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞

Tactic:
simpa [ENNReal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos,
      ENNReal.sum_eq_top, not_or] using H'

Premises used: asymm, Real.HolderConjugate.symm, Real.HolderTriple.pos, ENNReal.rpow_eq_top_iff, not_or, ENNReal.sum_eq_top
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞)
⊢ (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞

Tactic:
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
    simpa [ENNReal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos,
      ENNReal.sum_eq_top, not_or] using H'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
⊢ (↑(∑ i ∈ s, HMul.hMul (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) ((fun (i : ι) ↦ (g i).toNNReal) i)) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) p) (1 / p) *
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (g i).toNNReal) i) q) (1 / q)) :
      ℝ≥0∞)

Tactic:
have := ENNReal.coe_le_coe.2 (@NNReal.inner_le_Lp_mul_Lq _ s (fun i => ENNReal.toNNReal (f i))
    (fun i => ENNReal.toNNReal (g i)) _ _ hpq)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  (↑(∑ i ∈ s, HMul.hMul (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) ((fun (i : ι) ↦ (g i).toNNReal) i)) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) p) (1 / p) *
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (g i).toNNReal) i) q) (1 / q)) :
      ℝ≥0∞)
⊢ ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹

Tactic:
simp [ENNReal.coe_rpow_of_nonneg, hpq.pos.le, hpq.symm.pos.le] at this

Premises used: Real.HolderConjugate.symm, ENNReal.coe_rpow_of_nonneg, Real.HolderTriple.pos, LT.lt.le
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹

Tactic:
this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))
h₁ :
  HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) =
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
convert! this using 1
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)
h₁ : 1 / p = p⁻¹
h₂ : Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)
h₃ : 1 / q = q⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) =
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹

Tactic:
congr 2
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))
h₁ : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)
h₂ : 1 / p = p⁻¹
h₃ : Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)
h₄ : 1 / q = q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
convert! this using 1 <;> [skip; congr 2]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ 1 / p = p⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ 1 / q = q⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))
h₁ : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)
h₂ : Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
convert! this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : ∀ (i : ι) (hi : i ∈ s), f i * g i = (↑(f i).toNNReal : ℝ≥0∞) * (↑(g i).toNNReal : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
i : ι
hi : i ∈ s
⊢ f i * g i = (↑(f i).toNNReal : ℝ≥0∞) * (↑(g i).toNNReal : ℝ≥0∞)

Tactic:
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul]

Premises used: And.right, And.left, WithZero.coe_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : ∀ (i : ι) (hi : i ∈ s), f i ^ p = (↑(f i).toNNReal : ℝ≥0∞) ^ p
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
i : ι
hi : i ∈ s
⊢ f i ^ p = (↑(f i).toNNReal : ℝ≥0∞) ^ p

Tactic:
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul]

Premises used: And.right, And.left, WithZero.coe_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
h : ∀ (i : ι) (hi : i ∈ s), g i ^ q = (↑(g i).toNNReal : ℝ≥0∞) ^ q
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
i : ι
hi : i ∈ s
⊢ g i ^ q = (↑(g i).toNNReal : ℝ≥0∞) ^ q

Tactic:
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul]

Premises used: And.right, And.left, WithZero.coe_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0∞
inl :
  ∀ (hp : LE.le (α := ℝ) 1 1),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (HSub.hSub (α := ℝ) 1 1⁻¹) *
        HPow.hPow (α := ℝ≥0∞) (β := ℝ) (∑ i ∈ s, w i * HPow.hPow (β := ℝ) (f i) 1) 1⁻¹
inr :
  ∀ (hp : 1 < p),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
obtain rfl | hp := hp.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w f : ι → ℝ≥0∞
hp : LE.le (α := ℝ) 1 1
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (HSub.hSub (α := ℝ) 1 1⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (β := ℝ) (∑ i ∈ s, w i * HPow.hPow (β := ℝ) (f i) 1) 1⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
⊢ 0 < p

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
⊢ 0 < p

Tactic:
have hp₀ : 0 < p := by positivity
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
⊢ p⁻¹ < 1

Tactic:
have hp₁ : p⁻¹ < 1 := inv_lt_one_of_one_lt₀ hp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
pos :
  ∀ (H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = 0 ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = 0),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
neg :
  ∀ (H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
by_cases! H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = 0 ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = 0

Premises used: HMul.hMul, HSub.hSub, Inv.inv, HPow.hPow, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = 0 ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = 0
⊢ (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0

Tactic:
simpa [hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_zero_iff_of_nonneg] using H

Premises used: Finset.sum_eq_zero_iff_of_nonneg, LT.lt.not_gt
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = 0 ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = 0
⊢ (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0

Tactic:
replace H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0 := by
      simpa [hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_zero_iff_of_nonneg] using H
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0
i : ι
hi : i ∈ s
inl : ∀ (H : ∀ i ∈ s, w i = 0), w i * f i = 0
inr : ∀ (H : ∀ i ∈ s, w i = 0 ∨ f i = 0), w i * f i = 0
⊢ w i * f i = 0

Tactic:
rcases H with H | H
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
i : ι
hi : i ∈ s
H : ∀ i ∈ s, w i = 0
⊢ w i * f i = 0

Tactic:
simp [H i hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
i : ι
hi : i ∈ s
H : ∀ i ∈ s, w i = 0 ∨ f i = 0
⊢ w i * f i = 0

Tactic:
simp [H i hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0
⊢ ∀ (i : ι) (hi : i ∈ s), w i * f i = 0

Tactic:
have (i) (hi : i ∈ s) : w i * f i = 0 := by rcases H with H | H <;> simp [H i hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0
this : ∀ (i : ι) (hi : i ∈ s), w i * f i = 0
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
simp [sum_eq_zero this]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
pos :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
neg :
  ∀
    (H' :
      ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞)),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
by_cases H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤

Premises used: HMul.hMul, HSub.hSub, Inv.inv, HPow.hPow, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞
pos :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
pos₁ :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
rcases H' with H' | H'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]

Premises used: ENNReal.rpow_eq_zero_iff, one_div, Finset.sum_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞
⊢ ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]

Premises used: ENNReal.rpow_eq_zero_iff, one_div, Finset.sum_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞)
⊢ (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞

Tactic:
simpa [rpow_eq_top_iff, hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_top, not_or] using H'

Premises used: ENNReal.rpow_eq_top_iff, not_or, LT.lt.not_gt, ENNReal.sum_eq_top