awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
hi : i ∈ s
hx hx₁ hx₂ : 0 ≤ w i → 0 ≤ w i * z i ^ p
hx₃ hx₄ : 0 ≤ w i → 0 ≤ z i → 0 ≤ w i * z i ^ p
⊢ 0 ≤ w i * z i ^ p

Tactic:
positivity [hw i hi, hz i hi]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
apply_rules : ∀ i ∈ s, 0 ≤ w i * z i
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)

Tactic:
apply_rules [sum_nonneg, rpow_nonneg]

Premises used: Finset.sum_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
hi : i ∈ s
positivity positivity₁ positivity₂ : 0 ≤ w i → 0 ≤ w i * z i
positivity₃ positivity₄ : 0 ≤ w i → 0 ≤ z i → 0 ≤ w i * z i
⊢ 0 ≤ w i * z i

Tactic:
positivity [hw i hi, hz i hi]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hx : ∀ i ∈ s, 0 ≤ w i * z i ^ p
⊢ 0 ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)

Tactic:
apply_rules [sum_nonneg, rpow_nonneg]

Premises used: Finset.sum_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1
n : ℕ
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * z i) n ≤ ∑ i ∈ s, w i * z i ^ n

Tactic:
mod_cast
    Real.pow_arith_mean_le_arith_mean_pow s _ _ (fun i _ => (w i).coe_nonneg)
      (mod_cast hw') (fun i _ => (z i).coe_nonneg) n

Premises used: HMul.hMul, congrArg, NNReal.coe_le_coe._simp_1, cast, Real.pow_arith_mean_le_arith_mean_pow, LE.le, Nat.cast, HPow.hPow, congr, NNReal.coe_nonneg, NNReal.coe_sum._simp_1, Eq.refl, congrFun', NNReal.coe_inj._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, NNReal.toReal, Finset.sum_congr, Finset.sum, Eq.trans
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
mod_cast
    Real.rpow_arith_mean_le_arith_mean_rpow s _ _ (fun i _ => (w i).coe_nonneg)
      (mod_cast hw') (fun i _ => (z i).coe_nonneg) hp

Premises used: HMul.hMul, congrArg, Real.rpow_arith_mean_le_arith_mean_rpow, NNReal.coe_le_coe._simp_1, cast, LE.le, Nat.cast, HPow.hPow, congr, NNReal.coe_nonneg, NNReal.coe_sum._simp_1, Eq.refl, congrFun', NNReal.coe_inj._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, NNReal.toReal, Finset.sum_congr, Finset.sum, Eq.trans
-- 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
inl :
  ∀ (hp : LE.le (α := ℝ) 1 1),
    HPow.hPow (β := ℝ) (z₁ + z₂) 1 ≤
      HPow.hPow (α := ℝ≥0) 2 (HSub.hSub (α := ℝ) 1 1) * (HPow.hPow (β := ℝ) z₁ 1 + HPow.hPow (β := ℝ) z₂ 1)
inr : ∀ (h'p : 1 < p), (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
rcases eq_or_lt_of_le hp with (rfl | h'p)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
hp : LE.le (α := ℝ) 1 1
inl : z₁ + z₂ ≤ z₁ + z₂
⊢ HPow.hPow (β := ℝ) (z₁ + z₂) 1 ≤
    HPow.hPow (α := ℝ≥0) 2 (HSub.hSub (α := ℝ) 1 1) * (HPow.hPow (β := ℝ) z₁ 1 + HPow.hPow (β := ℝ) z₂ 1)

Tactic:
simp only [rpow_one, sub_self, rpow_zero, one_mul]

Premises used: sub_self, NNReal.rpow_zero, NNReal.rpow_one, one_mul
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
hp : LE.le (α := ℝ) 1 1
⊢ z₁ + z₂ ≤ z₁ + z₂

Tactic:
rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 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₂) (add_halves 1) hp

Premises used: HMul.hMul, add_halves, HDiv.hDiv, NNReal.rpow_arith_mean_le_arith_mean2_rpow, OfNat.ofNat
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 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₂) (add_halves 1) hp using 1

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

Tactic:
simp only [one_div, inv_mul_cancel_left₀, Ne, two_ne_zero,
      not_false_iff]

Premises used: inv_mul_cancel_left₀, Ne, two_ne_zero, one_div, not_false_iff
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ p - 1 ≠ 0

Tactic:
have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
h :
  HPow.hPow (α := ℝ≥0) 2 p / 2 * (z₁ ^ p + z₂ ^ p) =
    1 / 2 * (HPow.hPow (α := ℝ≥0) 2 p * z₁ ^ p) + 1 / 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, rpow_sub' A, rpow_one]

Premises used: NNReal.rpow_sub', NNReal.rpow_one, NNReal.mul_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ HPow.hPow (α := ℝ≥0) 2 p / 2 * (z₁ ^ p + z₂ ^ p) =
    1 / 2 * (HPow.hPow (α := ℝ≥0) 2 p * z₁ ^ p) + 1 / 2 * (HPow.hPow (α := ℝ≥0) 2 p * z₂ ^ p)

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

Tactic:
mod_cast
    Real.arith_mean_le_rpow_mean s _ _ (fun i _ => (w i).coe_nonneg) (mod_cast hw')
      (fun i _ => (z i).coe_nonneg) hp

Premises used: HMul.hMul, congrArg, NNReal.coe_le_coe._simp_1, cast, HDiv.hDiv, Real.arith_mean_le_rpow_mean, LE.le, Nat.cast, HPow.hPow, congr, NNReal.coe_nonneg, NNReal.coe_sum._simp_1, Eq.refl, congrFun', NNReal.coe_inj._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, NNReal.toReal, Finset.sum_congr, Finset.sum, Eq.trans
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
⊢ ∀ x ≤ 1, x ^ p ≤ x

Tactic:
have h_le_one : ∀ x : ℝ≥0, x ≤ 1 → x ^ p ≤ x := fun x hx => rpow_le_self_of_le_one hx hp1
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
⊢ a ≤ 1

Tactic:
have ha : a ≤ 1 := (self_le_add_right a b).trans hab
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
⊢ b ≤ 1

Tactic:
have hb : b ≤ 1 := (self_le_add_left b a).trans hab
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Tactic:
(add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab

Premises used: add_le_add, LE.le.trans
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Tactic:
exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab

Premises used: add_le_add, LE.le.trans
-- 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
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
pos : ∀ (h_zero : a + b = 0), a ^ p + b ^ p ≤ (a + b) ^ p
neg : ∀ (h_zero : ¬a + b = 0), a ^ p + b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
by_cases h_zero : a + b = 0
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
simp [add_eq_zero.mp h_zero, hp_pos.ne']

Premises used: LT.lt.ne', Iff.mp, add_eq_zero
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_zero : ¬(a = 0 ∧ b = 0)), ¬(a = 0 ∧ b = 0)
⊢ ¬(a = 0 ∧ b = 0)

Tactic:
rwa [add_eq_zero] at h_zero

Premises used: add_eq_zero
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ ¬(a = 0 ∧ b = 0)

Tactic:
have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero] at h_zero
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
rw : (a + b) / (a + b) = 1
rw₁ rw₂ : Eq (α := ℝ≥0) 1 1
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
rw [← add_div, div_self h_zero]

Premises used: div_self, add_div
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
have h_add : a / (a + b) + b / (a + b) = 1 := by rw [← add_div, div_self h_zero]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
⊢ (a / (a + b)) ^ p + (b / (a + b)) ^ p ≤ 1

Tactic:
have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : (a / (a + b)) ^ p + (b / (a + b)) ^ p ≤ 1
⊢ a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1

Tactic:
rw [div_rpow a (a + b), div_rpow b (a + b)] at h

Premises used: HAdd.hAdd, NNReal.div_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
⊢ (a + b) ^ p ≠ 0

Tactic:
simp [h_nonzero]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
⊢ (a + b) ^ p ≠ 0

Tactic:
have hab_0 : (a + b) ^ p ≠ 0 := by simp [h_nonzero]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
nth_rw : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p

Tactic:
nth_rw 4 [← mul_one ((a + b) ^ p)]

Premises used: HPow.hPow, HAdd.hAdd, mul_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p

Tactic:
have h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p := by
    nth_rw 4 [← mul_one ((a + b) ^ p)]; gcongr
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p
neg :
  ∀ (h_mul : (a + b) ^ p * (a ^ p * ((a + b) ^ p)⁻¹ + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p), a ^ p + b ^ p ≤ (a + b) ^ p
neg₁ :
  ∀ (h_mul : (a + b) ^ p * (a ^ p * ((a + b) ^ p)⁻¹ + b ^ p * ((a + b) ^ p)⁻¹) ≤ (a + b) ^ p),
    a ^ p + b ^ p ≤ (a + b) ^ p
neg₂ :
  ∀ (h_mul : (a + b) ^ p * (a ^ p * ((a + b) ^ p)⁻¹) + (a + b) ^ p * (b ^ p * ((a + b) ^ p)⁻¹) ≤ (a + b) ^ p),
    a ^ p + b ^ p ≤ (a + b) ^ p
neg₃ :
  ∀ (h_mul : (a + b) ^ p * (((a + b) ^ p)⁻¹ * a ^ p) + (a + b) ^ p * (b ^ p * ((a + b) ^ p)⁻¹) ≤ (a + b) ^ p),
    a ^ p + b ^ p ≤ (a + b) ^ p
neg₄ :
  ∀ (h_mul : (a + b) ^ p * (((a + b) ^ p)⁻¹ * a ^ p) + (a + b) ^ p * (((a + b) ^ p)⁻¹ * b ^ p) ≤ (a + b) ^ p),
    a ^ p + b ^ p ≤ (a + b) ^ p
neg₅ :
  ∀ (h_mul : (a + b) ^ p * ((a + b) ^ p)⁻¹ * a ^ p + (a + b) ^ p * (((a + b) ^ p)⁻¹ * b ^ p) ≤ (a + b) ^ p),
    a ^ p + b ^ p ≤ (a + b) ^ p
neg₆ :
  ∀ (h_mul : (a + b) ^ p * ((a + b) ^ p)⁻¹ * a ^ p + (a + b) ^ p * ((a + b) ^ p)⁻¹ * b ^ p ≤ (a + b) ^ p),
    a ^ p + b ^ p ≤ (a + b) ^ p
neg₇ : ∀ (h_mul : 1 * a ^ p + 1 * b ^ p ≤ (a + b) ^ p), a ^ p + b ^ p ≤ (a + b) ^ p
neg₈ : ∀ (h_mul : a ^ p + 1 * b ^ p ≤ (a + b) ^ p), a ^ p + b ^ p ≤ (a + b) ^ p
neg₉ neg₁₀ neg₁₁ neg₁₂ : ∀ (h_mul : a ^ p + b ^ p ≤ (a + b) ^ p), a ^ p + b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ←
    mul_assoc, mul_inv_cancel₀ hab_0, one_mul, one_mul] at h_mul

Premises used: mul_inv_cancel₀, mul_assoc, div_eq_mul_inv, HPow.hPow, mul_comm, mul_add, one_mul
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ 0 < p⁻¹

Tactic:
simp [lt_of_lt_of_le zero_lt_one hp1]

Premises used: zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
rw : a ^ p + b ^ p ≤ (a + b) ^ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
rw [one_div,
    ← @NNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1]), inv_inv]

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

Tactic:
add_rpow_le_rpow_add _ _ hp1

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

Tactic:
exact add_rpow_le_rpow_add _ _ hp1

Premises used: NNReal.add_rpow_le_rpow_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a_1 b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
rw : a ^ q = a ^ (p * (q / p))
rw₁ : a ^ q = a ^ (p * (p⁻¹ * q))
rw₂ : a ^ q = a ^ (p * p⁻¹ * q)
rw₃ : a ^ q = a ^ (1 * q)
rw₄ rw₅ : a ^ q = a ^ q
⊢ a ^ q = (a ^ p) ^ (q / p)

Tactic:
rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
      one_mul]

Premises used: mul_inv_cancel₀, mul_assoc, NNReal.rpow_mul, Ne.symm, div_eq_inv_mul, one_mul, LT.lt.ne
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
⊢ ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)

Tactic:
have h_rpow : ∀ a : ℝ≥0, a ^ q = (a ^ p) ^ (q / p) := fun a => by
    rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
      one_mul]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Premises used: NNReal.rpow_add_rpow_le_add, HPow.hPow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
refine : 1 ≤ q / p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Premises used: NNReal.rpow_add_rpow_le_add, HPow.hPow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
rwa rwa₁ rwa₂ rwa₃ : p ≤ q
⊢ 1 ≤ q / p

Tactic:
rwa [one_le_div hp_pos]

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

Tactic:
have h_rpow_add_rpow_le_add :
    ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p := by
    refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
    rwa [one_le_div hp_pos]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
rw : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
rw [h_rpow a, h_rpow b, one_div p, NNReal.le_rpow_inv_iff hp_pos, ← NNReal.rpow_mul, mul_comm,
    mul_one_div]

Premises used: NNReal.rpow_mul, NNReal.le_rpow_inv_iff, mul_one_div, one_div, mul_comm
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p),
    ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p

Tactic:
rwa [one_div_div] at h_rpow_add_rpow_le_add

Premises used: one_div_div
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
inl :
  ∀ (hp : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
    HPow.hPow (β := ℝ) (a + b) 0 ≤ HPow.hPow (β := ℝ) a 0 + HPow.hPow (β := ℝ) b 0
inr : ∀ (hp_pos : 0 < p), (a + b) ^ p ≤ a ^ p + b ^ p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rcases hp.eq_or_lt with (rfl | hp_pos)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
a b : ℝ≥0
hp : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
⊢ HPow.hPow (β := ℝ) (a + b) 0 ≤ HPow.hPow (β := ℝ) a 0 + HPow.hPow (β := ℝ) b 0

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
have h := rpow_add_rpow_le a b hp_pos hp1
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [one_div_one, one_div] at h

Premises used: one_div, one_div_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [NNReal.rpow_one] at h

Premises used: NNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ a + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [NNReal.rpow_one] at h

Premises used: NNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ a + b ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [NNReal.rpow_one] at h

Premises used: NNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ a + b ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
repeat' rw [NNReal.rpow_one] at h

Premises used: NNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
(NNReal.le_rpow_inv_iff hp_pos).mp h

Premises used: NNReal.le_rpow_inv_iff, Iff.mp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
exact (NNReal.le_rpow_inv_iff hp_pos).mp h

Premises used: NNReal.le_rpow_inv_iff, Iff.mp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ 0 ≤ a

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

Tactic:
lift a to NNReal using ha

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

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

Tactic:
lift b to NNReal using hb

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

Tactic:
exact_mod_cast NNReal.add_rpow_le_rpow_add a b hp1

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

Tactic:
lift a to NNReal using ha

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

Tactic:
lift b to NNReal using hb

Premises used: NNReal