awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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)
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
have inr : ∀ (h'p : 1 < 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)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0
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)
have inl : z₁ + z₂ ≤ z₁ + z₂
Tactic: simp only [rpow_one, sub_self, rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
have h : (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
have h₁ : HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
have A : p - 1 ≠ 0
Tactic: have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
have 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)
Tactic: simp only [mul_rpow, rpow_sub' A, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ 1
have h_le_one : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1
have ha : a ≤ 1
Tactic: have ha : a ≤ 1 := (self_le_add_right a b).trans hab
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1
have hb : b ≤ 1
Tactic: have hb : b ≤ 1 := (self_le_add_left b a).trans hab
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have pos : ∀ (h_zero : a + b = 0), a ^ p + b ^ p ≤ (a + b) ^ p
Tactic: by_cases h_zero : a + b = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have neg : ∀ (h_zero : ¬a + b = 0), a ^ p + b ^ p ≤ (a + b) ^ p
Tactic: by_cases h_zero : a + b = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ ¬(a = 0 ∧ b = 0)
have rwa : ∀ (h_zero : ¬(a = 0 ∧ b = 0)), ¬(a = 0 ∧ b = 0)
Tactic: rwa [add_eq_zero] at h_zero
Cleared hypotheses: h_zero
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have h_nonzero : ¬(a = 0 ∧ b = 0)
Tactic: have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero] at h_zero
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
have rw : (a + b) / (a + b) = 1
Tactic: rw [← add_div, div_self h_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have rw₁ : Eq (α := ℝ≥0) 1 1
Tactic: rw [← add_div, div_self h_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have h_add : 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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
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 ^ p + b ^ p ≤ (a + b) ^ p
have h : (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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
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 + b ^ p ≤ (a + b) ^ p
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
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 ^ p + b ^ p ≤ (a + b) ^ p
have hab_0 : (a + b) ^ p ≠ 0
Tactic: have hab_0 : (a + b) ^ p ≠ 0 := by simp [h_nonzero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
have nth_rw : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1
Tactic: nth_rw 4 [← mul_one ((a + b) ^ p)]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
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 ^ p + b ^ p ≤ (a + b) ^ p
have h_mul : (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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have 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
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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have neg₇ : ∀ (h_mul : 1 * a ^ p + 1 * 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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have neg₈ : ∀ (h_mul : a ^ p + 1 * 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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have neg₉ : ∀ (h_mul : 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
Cleared hypotheses: h_mul
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
have rw : a ^ p + b ^ p ≤ (a + b) ^ p
Tactic: rw [one_div,
    ← @NNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1]), inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q : ℝ
a_1 b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q : ℝ
a_1 b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
rw : a ^ q = a ^ (p * (q / p))
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw₁ : a ^ q = a ^ (p * (p⁻¹ * q))
Tactic: rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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))
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw₂ : a ^ q = a ^ (p * p⁻¹ * q)
Tactic: rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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)
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw₃ : a ^ q = a ^ (1 * q)
Tactic: rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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)
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw₄ : a ^ q = a ^ q
Tactic: rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
have h_rpow : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
have refine : 1 ≤ q / p
Tactic: refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
have h_rpow_add_rpow_le_add : ((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]