-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_arith_mean_le_arith_mean_rpow (w z : ι → ℝ≥0∞) (hw' : ∑ i ∈ s, w i = 1) {p : ℝ}
    (hp : 1 ≤ p) : (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p

Proof state:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
⊢ ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Tactic:
simp_rw [toNNReal_sum h_top_rpow, toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul,
  toNNReal_rpow]

Result:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
⊢ (∑ x ∈ s, (w x).toNNReal * (z x).toNNReal) ^ p ≤ ∑ x ∈ s, (w x).toNNReal * (z x).toNNReal ^ p

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ⊤
⊢ w i * z i ^ p ≠ ⊤

Tactic:
rwa [Ne, ← h_top_iff_rpow_top i hi]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p

Tactic:
positivity

Result:
no goals

Proof state:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
⊢ (∑ i ∈ s, w i * z i) ^ p ≠ ⊤ →
    ∑ i ∈ s, w i * z i ^ p ≠ ⊤ → ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Tactic:
intro h_top_rpow_sum _

Result:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
⊢ ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Proof state:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
⊢ (∑ x ∈ s, (w x).toNNReal * (z x).toNNReal) ^ p ≤ ∑ x ∈ s, (w x).toNNReal * (z x).toNNReal ^ p

Tactic:
refine
  NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal)
    (fun i => (z i).toNNReal) ?_ hp

Result:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
⊢ ∑ i ∈ s, (fun i => (w i).toNNReal) i = 1

Proof state:
case refine_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h : (∃ a ∈ s, w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ ∃ a ∈ s, w a * z a ^ p = ⊤

Tactic:
use a, H

Result:
case right
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h : (∃ a ∈ s, w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ w a * z a ^ p = ⊤

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
⊢ ∀ a ∈ s, w a * z a ^ p ≠ ⊤

Tactic:
intro i hi

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ⊤

Proof state:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
⊢ ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Tactic:
have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
  haveI h_top_sum : ∑ i ∈ s, w i * z i ≠ ⊤ := by
    intro h
    rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
    exact h_top_rpow_sum rfl
  fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne

Result:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h_top : ∀ a ∈ s, w a * z a ≠ ⊤
⊢ ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal