-- 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_1
ι : 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 : ∑ i ∈ s, w i * z i = 0 ∧ p < 0 ∨ (∃ a ∈ s, w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a ∈ s, w a * z a ^ p = ⊤

Tactic:
simp only [and_false, hp_not_neg, false_or] at h

Result:
case refine_1
ι : 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 ∈ s, w a * z a ^ p = ⊤

Proof state:
case refine_1
ι : 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 ∈ s, w a * z a ^ p = ⊤

Tactic:
rcases h.left with ⟨a, H, ha⟩

Result:
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 = ⊤

Proof state:
ι : Type u
s : Finset ι
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

Tactic:
have hp_pos : 0 < p := by positivity

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ 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 : ⊤ ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h : ∑ i ∈ s, w i * z i = ⊤
⊢ False

Tactic:
exact h_top_rpow_sum rfl

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
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 : ∑ i ∈ s, w i * z i = ⊤
⊢ False

Tactic:
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum

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 : ⊤ ≠ ⊤
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ⊤
h : ∑ i ∈ s, w i * z i = ⊤
⊢ False

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 ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
⊢ ∑ i ∈ s, w i = ∑ a ∈ s, ↑(w a).toNNReal

Tactic:
refine sum_congr rfl fun i hi => (coe_toNNReal ?_).symm

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 ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i ≠ ⊤

Proof state:
case refine_1
ι : 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 = 0 ∧ p < 0 ∨ (∃ a ∈ s, w a * z a = ⊤) ∧ 0 < p → ∃ a ∈ s, w a * z a ^ p = ⊤

Tactic:
intro h

Result:
case refine_1
ι : 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 : ∑ i ∈ s, w i * z i = 0 ∧ p < 0 ∨ (∃ a ∈ s, w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a ∈ s, 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 = ⊤
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
refine le_of_top_imp_top_of_toNNReal_le ?_ ?_

Result:
case refine_1
ι : 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 = ⊤

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

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

Tactic:
positivity

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
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 : ι
hi : i ∈ s
⊢ w i ≠ ⊤

Tactic:
refine (lt_top_of_sum_ne_top ?_ hi).ne

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 ≠ ⊤
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s, w x ≠ ⊤

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, (fun i => (w i).toNNReal) i = 1

Tactic:
have h_sum_nnreal : ∑ i ∈ s, w i = ↑(∑ i ∈ s, (w i).toNNReal) := by
  rw [coe_finset_sum]
  refine sum_congr rfl fun i hi => (coe_toNNReal ?_).symm
  refine (lt_top_of_sum_ne_top ?_ hi).ne
  exact hw'.symm ▸ ENNReal.one_ne_top

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 ≠ ⊤
h_sum_nnreal : ∑ i ∈ s, w i = ↑(∑ i ∈ s, (w i).toNNReal)
⊢ ∑ i ∈ s, (fun i => (w i).toNNReal) i = 1