awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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∞))
⊢ ∑ 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)
have 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⁻¹
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ 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⁻¹
have h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ 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⁻¹
have h₁ : 1 / p = p⁻¹
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ 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⁻¹
have h₂ : Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ 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⁻¹
have h₃ : 1 / q = q⁻¹
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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 ∈ 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)
have h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))
Tactic: convert! this using 1 <;> [skip; congr 2]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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∞))
⊢ ∑ 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)
have h₁ : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)
Tactic: convert! this using 1 <;> [skip; congr 2]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ ∑ 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)
have h₂ : 1 / p = p⁻¹
Tactic: convert! this using 1 <;> [skip; congr 2]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ ∑ 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)
have h₃ : Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)
Tactic: convert! this using 1 <;> [skip; congr 2]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ ∑ 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)
have h₄ : 1 / q = q⁻¹
Tactic: convert! this using 1 <;> [skip; congr 2]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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 ∈ 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)
have h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))
Tactic: convert! this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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∞))
⊢ ∑ 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)
have h₁ : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p)
Tactic: convert! this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ ∑ 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)
have h₂ : Eq (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q)
Tactic: convert! this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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∞))
have h : ∀ (i : ι) (hi : i ∈ s), f i * g i = (↑(f i).toNNReal : ℝ≥0∞) * (↑(g i).toNNReal : ℝ≥0∞)
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
have h : ∀ (i : ι) (hi : i ∈ s), f i ^ p = (↑(f i).toNNReal : ℝ≥0∞) ^ p
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
have h : ∀ (i : ι) (hi : i ∈ s), g i ^ q = (↑(g i).toNNReal : ℝ≥0∞) ^ q
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥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⁻¹
have 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⁻¹
Tactic: obtain rfl | hp := hp.eq_or_lt
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ ∑ 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⁻¹
have 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⁻¹
Tactic: obtain rfl | hp := hp.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
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⁻¹
have hp₀ : 0 < p
Tactic: have hp₀ : 0 < p := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < 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⁻¹
have hp₁ : p⁻¹ < 1
Tactic: have hp₁ : p⁻¹ < 1 := inv_lt_one_of_one_lt₀ hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
⊢ ∑ 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⁻¹
have 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⁻¹
Tactic: by_cases! H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = 0 ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ ∑ 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⁻¹
have 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⁻¹
Tactic: by_cases! H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = 0 ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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 * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have H₁ : (∀ 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
have inl : ∀ (H : ∀ i ∈ s, w i = 0), w i * f i = 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * f i = 0
have inr : ∀ (H : ∀ i ∈ s, w i = 0 ∨ f i = 0), w i * f i = 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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 ∈ 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⁻¹
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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 * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have 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⁻¹
Tactic: by_cases H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ ∑ 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⁻¹
have 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⁻¹
Tactic: by_cases H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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 * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have 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⁻¹
Tactic: rcases H' with H' | H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
⊢ ∑ 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⁻¹
have 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⁻¹
Tactic: rcases H' with H' | H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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 * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have H'₁ : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
Tactic: replace H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤ := by
    simpa [rpow_eq_top_iff, hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_top, not_or] using H'
Cleared hypotheses: H'