-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma add_pow_le (ha : 0 ≤ a) (hb : 0 ≤ b) : ∀ n, (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by
    rw [pow_succ]
    calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Proof state:
case inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hba : b ≤ a
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
exact mul_add_mul_le_mul_add_mul' (pow_le_pow_left₀ hb hba _) hba

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 0 ≤ 2 ^ (0 - 1) * (a ^ 0 + b ^ 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 1 ≤ 2 ^ (1 - 1) * (a ^ 1 + b ^ 1)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ (n + 1) * (a ^ (n + 2) + b ^ (n + 2)) = 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 1) * (a + b) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
calc
  _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
      mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
  _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
      rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
        add_add_add_comm, add_comm (_ * a)]
  _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) :=
      mul_le_mul_of_nonneg_left (add_le_add_left ?_ _) <| pow_nonneg (zero_le_two (α := R)) _
  _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) =
    2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
simp only [← pow_succ, ← two_mul, ← mul_assoc]

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ (n + 1) * (a ^ (n + 2) + b ^ (n + 2)) = 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
obtain hab | hba := le_total a b

Result:
case inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hab : a ≤ b
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

case inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hba : b ≤ a
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Proof state:
case inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hab : a ≤ b
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
exact mul_add_mul_le_mul_add_mul (pow_le_pow_left₀ ha hab _) hab

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 2) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
rw [pow_succ]

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 1) * (a + b) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Tactic:
rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
  add_add_add_comm, add_comm (_ * a)]

Result:
no goals