awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
hp1 : 1 ≤ p
a b : ℝ≥0
⊢ ((↑a : ℝ) ^ p + (↑b : ℝ) ^ p) ^ (1 / p) ≤ (↑a : ℝ) + (↑b : ℝ)

Tactic:
exact_mod_cast NNReal.rpow_add_rpow_le_add a b hp1

Premises used: NNReal.rpow_add_rpow_le_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
⊢ 0 ≤ a

Tactic:
ha
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
lift : ∀ (a : ℝ≥0), ((↑a : ℝ) ^ q + b ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + b ^ p) ^ (1 / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
lift a to NNReal using ha

Premises used: NNReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q b : ℝ
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ 0 ≤ b

Tactic:
hb
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q b : ℝ
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
lift : ∀ (b : ℝ≥0), ((↑a : ℝ) ^ q + (↑b : ℝ) ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + (↑b : ℝ) ^ p) ^ (1 / p)
⊢ ((↑a : ℝ) ^ q + b ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + b ^ p) ^ (1 / p)

Tactic:
lift b to NNReal using hb

Premises used: NNReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
hp_pos : 0 < p
hpq : p ≤ q
a b : ℝ≥0
⊢ ((↑a : ℝ) ^ q + (↑b : ℝ) ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + (↑b : ℝ) ^ p) ^ (1 / p)

Tactic:
exact_mod_cast NNReal.rpow_add_rpow_le a b hp_pos hpq

Premises used: NNReal.rpow_add_rpow_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ 0 ≤ a

Tactic:
ha
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
lift : ∀ (a : ℝ≥0), ((↑a : ℝ) + b) ^ p ≤ (↑a : ℝ) ^ p + b ^ p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
lift a to NNReal using ha

Premises used: NNReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p b : ℝ
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
a : ℝ≥0
⊢ 0 ≤ b

Tactic:
hb
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p b : ℝ
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
a : ℝ≥0
lift : ∀ (b : ℝ≥0), ((↑a : ℝ) + (↑b : ℝ)) ^ p ≤ (↑a : ℝ) ^ p + (↑b : ℝ) ^ p
⊢ ((↑a : ℝ) + b) ^ p ≤ (↑a : ℝ) ^ p + b ^ p

Tactic:
lift b to NNReal using hb

Premises used: NNReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
hp : 0 ≤ p
hp1 : p ≤ 1
a b : ℝ≥0
⊢ ((↑a : ℝ) + (↑b : ℝ)) ^ p ≤ (↑a : ℝ) ^ p + (↑b : ℝ) ^ p

Tactic:
exact_mod_cast NNReal.rpow_add_le_add_rpow a b hp hp1

Premises used: NNReal.rpow_add_le_add_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

Tactic:
have hp_pos : 0 < p := by positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p

Tactic:
have hp_nonneg : 0 ≤ p := by positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ ¬p < 0

Tactic:
simp [hp_nonneg]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ ¬p < 0

Tactic:
have hp_not_neg : ¬p < 0 := by simp [hp_nonneg]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞

Tactic:
simp [ENNReal.mul_eq_top, hp_pos, hp_not_neg]

Premises used: ENNReal.mul_eq_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞

Tactic:
have h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤) := by
    simp [ENNReal.mul_eq_top, hp_pos, hp_not_neg]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 = ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
le_of_top_imp_top_of_toNNReal_le ?_ ?_

Premises used: ENNReal.le_of_top_imp_top_of_toNNReal_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 = ∞
refine_1 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p = ∞ → Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
refine_2 :
  HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞ →
    Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞ →
      (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
refine le_of_top_imp_top_of_toNNReal_le ?_ ?_

Premises used: ENNReal.le_of_top_imp_top_of_toNNReal_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 = ∞
refine_1 : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) 0 ∧ p < 0 ∨ (∃ a ∈ s, w a * z a = ∞) ∧ 0 < p → ∃ a ∈ s, w a * z a ^ p = ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p = ∞ → Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞

Tactic:
rw [rpow_eq_top_iff, sum_eq_top, sum_eq_top]

Premises used: ENNReal.rpow_eq_top_iff, ENNReal.sum_eq_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 = ∞
⊢ Eq (α := ℝ≥0∞) (∑ 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:
grind
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
refine_2 :
  Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞ →
    (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)
⊢ Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞ →
    (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)

Tactic:
_
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h_1 : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞
⊢ Ne (α := ℝ≥0∞) ∞ ∞

Tactic:
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum

Premises used: ENNReal.top_rpow_of_pos
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h_1 : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞
h_top_rpow_sum₁ : Ne (α := ℝ≥0∞) ∞ ∞
⊢ Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞

Tactic:
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum

Premises used: ENNReal.top_rpow_of_pos
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h_1 : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞
h_top_rpow_sum₁ : Ne (α := ℝ≥0∞) ∞ ∞
a : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞

Tactic:
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum

Premises used: ENNReal.top_rpow_of_pos
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : Ne (α := ℝ≥0∞) ∞ ∞
h_1 : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞
⊢ False

Tactic:
h_top_rpow_sum rfl

Premises used: rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : Ne (α := ℝ≥0∞) ∞ ∞
h_1 : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞
⊢ False

Tactic:
exact h_top_rpow_sum rfl

Premises used: rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
⊢ ∀ a ∈ s, w a * z a ≠ ∞

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
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
i : ι
hi : i ∈ s
⊢ w i * z i ≠ ∞

Tactic:
specialize h_top i hi
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ∞
rwa : ¬w i * z i ^ p = ∞
rwa₁ rwa₂ rwa₃ rwa₄ : ¬w i * z i = ∞
⊢ w i * z i ^ p ≠ ∞

Tactic:
rwa [Ne, ← h_top_iff_rpow_top i hi]

Premises used: Ne
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
⊢ ∀ a ∈ s, w a * z a ^ p ≠ ∞

Tactic:
have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ := by
      intro i hi
      specialize h_top i hi
      rwa [Ne, ← h_top_iff_rpow_top i hi]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 ≠ ∞
refine_2 :
  HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (w x).toNNReal * (z x).toNNReal) p ≤ ∑ x ∈ s, (w x).toNNReal * (z x).toNNReal ^ p
⊢ (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)

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

Premises used: ENNReal.toNNReal_rpow, ENNReal.toNNReal_mul, ENNReal.toNNReal_sum
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 ≠ ∞
⊢ HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (w x).toNNReal * (z x).toNNReal) p ≤ ∑ x ∈ s, (w x).toNNReal * (z x).toNNReal ^ p

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

Premises used: NNReal.rpow_arith_mean_le_arith_mean_rpow, ENNReal.toNNReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 ≠ ∞
refine_2 : Eq (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) 1
⊢ HPow.hPow (α := ℝ≥0) (∑ 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

Premises used: NNReal.rpow_arith_mean_le_arith_mean_rpow, ENNReal.toNNReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 ≠ ∞
rw : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞))
⊢ ∑ i ∈ s, w i = (↑(∑ i ∈ s, (w i).toNNReal) : ℝ≥0∞)

Tactic:
rw [coe_finsetSum]

Premises used: ENNReal.coe_finsetSum
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞))

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

Premises used: ENNReal.coe_toNNReal, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 ≠ ∞
refine : ∀ (i : ι) (hi : i ∈ s), w i ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞))

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

Premises used: ENNReal.coe_toNNReal, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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:
(lt_top_of_sum_ne_top ?_ hi).ne

Premises used: ENNReal.lt_top_of_sum_ne_top, LT.lt.ne
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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
refine : Ne (α := ℝ≥0∞) (∑ x ∈ s, w x) ∞
⊢ w i ≠ ∞

Tactic:
refine (lt_top_of_sum_ne_top ?_ hi).ne

Premises used: ENNReal.lt_top_of_sum_ne_top, LT.lt.ne
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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
⊢ Ne (α := ℝ≥0∞) (∑ x ∈ s, w x) ∞

Tactic:
hw'.symm ▸ ENNReal.one_ne_top

Premises used: Eq.rec, Eq.symm, ENNReal.one_ne_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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
⊢ Ne (α := ℝ≥0∞) (∑ x ∈ s, w x) ∞

Tactic:
exact hw'.symm ▸ ENNReal.one_ne_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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 = (↑(∑ i ∈ s, (w i).toNNReal) : ℝ≥0∞)

Tactic:
have h_sum_nnreal : ∑ i ∈ s, w i = ↑(∑ i ∈ s, (w i).toNNReal) := by
      rw [coe_finsetSum]
      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
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ 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 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ 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) : ℝ≥0∞)
refine_2 : (↑(∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) : ℝ≥0∞) = (↑1 : ℝ≥0∞)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∑ i ∈ s, w i = (↑1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) 1

Tactic:
rwa [← coe_inj, ← h_sum_nnreal]

Premises used: ENNReal.coe_inj
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
refine_2 :
  ∀
    (h :
      HPow.hPow (α := ℝ≥0∞) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) p ≤
        ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p),
    (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
refine_1 : Eq (α := ℝ≥0∞) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i) 1
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Tactic:
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  HPow.hPow (α := ℝ≥0∞) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) p ≤
    ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Tactic:
simpa [Fin.sum_univ_succ] using h

Premises used: Fin.sum_univ_succ
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ Eq (α := ℝ≥0∞) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i) 1

Tactic:
simp [hw', Fin.sum_univ_succ]

Premises used: Fin.sum_univ_succ
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p ≤ 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp

Premises used: HMul.hMul, HDiv.hDiv, ENNReal.add_halves, OfNat.ofNat, ENNReal.rpow_arith_mean_le_arith_mean2_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h : (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
h₁ : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
convert!
    rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp
      using 1

Premises used: HMul.hMul, HDiv.hDiv, ENNReal.add_halves, OfNat.ofNat, ENNReal.rpow_arith_mean_le_arith_mean2_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

Tactic:
simp [← mul_assoc, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, mul_assoc, two_ne_zero, ENNReal.inv_mul_cancel
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h :
  2⁻¹ * HPow.hPow (α := ℝ≥0∞) 2 p * (z₁ ^ p + z₂ ^ p) =
    2⁻¹ * (HPow.hPow (α := ℝ≥0∞) 2 p * z₁ ^ p) + 2⁻¹ * (HPow.hPow (α := ℝ≥0∞) 2 p * z₂ ^ p)
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero ofNat_ne_top,
      ENNReal.div_eq_inv_mul, rpow_one, mul_one]

Premises used: ENNReal.ofNat_ne_top, ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_sub, ENNReal.rpow_one, zero_le_one, two_ne_zero, LE.le.trans, mul_one, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2⁻¹ * HPow.hPow (α := ℝ≥0∞) 2 p * (z₁ ^ p + z₂ ^ p) =
    2⁻¹ * (HPow.hPow (α := ℝ≥0∞) 2 p * z₁ ^ p) + 2⁻¹ * (HPow.hPow (α := ℝ≥0∞) 2 p * z₂ ^ p)

Tactic:
ring
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p

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