-- Mathlib/Algebra/Order/Ring/Basic.lean
theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)

Tactic:
rw [pow_succ' _ n]

Result:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n

Proof state:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
have h2 := add_nonneg hx hy

Result:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
n : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n

Tactic:
rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩

Result:
case intro
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : k + 1 ≠ 0
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
exact le_add_of_nonneg_right h1

Result:
no goals

Proof state:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
let n := k.succ

Result:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
rw [pow_succ' _ n, pow_succ' _ n]

Result:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Proof state:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
calc
  x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
    rw [pow_succ' _ n, pow_succ' _ n]
    exact le_add_of_nonneg_right h1
  _ = (x + y) * (x ^ n + y ^ n) := by
    rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
      add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
  _ ≤ (x + y) ^ (n + 1) := by
    rw [pow_succ' _ n]
    exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2

Result:
no goals

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n

Tactic:
exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2

Result:
no goals

Proof state:
case intro.zero
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
hn : 0 + 1 ≠ 0
⊢ x ^ (0 + 1) + y ^ (0 + 1) ≤ (x + y) ^ (0 + 1)

Tactic:
simp only [zero_add, pow_one, le_refl]

Result:
no goals

Proof state:
case intro
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : k + 1 ≠ 0
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)

Tactic:
induction k with
| zero => simp only [zero_add, pow_one, le_refl]
| succ k ih =>
  let n := k.succ
  have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
  have h2 := add_nonneg hx hy
  calc
    x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
      rw [pow_succ' _ n, pow_succ' _ n]
      exact le_add_of_nonneg_right h1
    _ = (x + y) * (x ^ n + y ^ n) := by
      rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
        add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
    _ ≤ (x + y) ^ (n + 1) := by
      rw [pow_succ' _ n]
      exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2

Result:
no goals

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)

Tactic:
rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
  add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]

Result:
no goals

Proof state:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))

Result:
case intro.succ
R : Type u_3
inst✝ : OrderedSemiring R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)