-- Mathlib/Data/Nat/Cast/Order/Ring.lean
lemma mul_le_pow {a : ℕ} (ha : a ≠ 1) (b : ℕ) :
    a * b ≤ a ^ b

Proof state:
case succ.succ.zero
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
ha : 0 + 1 ≠ 1
⊢ (0 + 1) * b + (0 + 1) ≤ (0 + 1) ^ b * (0 + 1)

Tactic:
simp at ha

Result:
no goals

Proof state:
case succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a ≠ 1
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
rw [mul_add_one, pow_succ]

Result:
case succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a ≠ 1
⊢ a * b + a ≤ a ^ b * a

Proof state:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≤ (a + 1 + 1) * (a + 1 + 1) ^ b

Tactic:
exact le_mul_of_one_le_right' (one_le_pow _ _ (by simp))

Result:
no goals

Proof state:
case succ.zero
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
ha : 0 ≠ 1
⊢ 0 * b + 0 ≤ 0 ^ b * 0

Tactic:
simp

Result:
no goals

Proof state:
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ.succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a + 1 + 1 ≠ 1
⊢ (a + 1 + 1) * b + (a + 1 + 1) ≤ (a + 1 + 1) ^ b * (a + 1 + 1)

Tactic:
rw [mul_add_one, mul_add_one, add_comm (_ * a), add_assoc _ (_ * a)]

Result:
case succ.succ.succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a + 1 + 1 ≠ 1
⊢ (a + 1 + 1) * b + (a + 1 + 1) ≤ (a + 1 + 1) ^ b + ((a + 1 + 1) ^ b * a + (a + 1 + 1) ^ b)

Proof state:
case succ.succ.succ.zero
a : ℕ
ha : a + 1 + 1 ≠ 1
hb : ∀ {a : ℕ}, a ≠ 1 → a * 0 ≤ a ^ 0
⊢ (a + 1 + 1) * 0 + (a + 1 + 1) ≤ (a + 1 + 1) ^ 0 + ((a + 1 + 1) ^ 0 * a + (a + 1 + 1) ^ 0)

Tactic:
simp [add_assoc, add_comm]

Result:
no goals

Proof state:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≤ (a + 1 + 1) * (a + 1 + 1) ^ b * a + (a + 1 + 1) * (a + 1 + 1) ^ b

Tactic:
refine (le_add_left ?_ ?_).trans' ?_

Result:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≤ (a + 1 + 1) * (a + 1 + 1) ^ b

Proof state:
case zero
a : ℕ
ha : a ≠ 1
⊢ a * 0 ≤ a ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ (a + 1 + 1) * (b + 1) + (a + 1 + 1) ≤ (a + 1 + 1) ^ (b + 1) + ((a + 1 + 1) ^ (b + 1) * a + (a + 1 + 1) ^ (b + 1))

Tactic:
refine add_le_add (hb (by simp)) ?_

Result:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≤ (a + 1 + 1) ^ (b + 1) * a + (a + 1 + 1) ^ (b + 1)

Proof state:
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ 0 < a + 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ.succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a + 1 + 1 ≠ 1
⊢ (a + 1 + 1) * b + (a + 1 + 1) ≤ (a + 1 + 1) ^ b + ((a + 1 + 1) ^ b * a + (a + 1 + 1) ^ b)

Tactic:
rcases b with (_|b)

Result:
case succ.succ.succ.zero
a : ℕ
ha : a + 1 + 1 ≠ 1
hb : ∀ {a : ℕ}, a ≠ 1 → a * 0 ≤ a ^ 0
⊢ (a + 1 + 1) * 0 + (a + 1 + 1) ≤ (a + 1 + 1) ^ 0 + ((a + 1 + 1) ^ 0 * a + (a + 1 + 1) ^ 0)

case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ (a + 1 + 1) * (b + 1) + (a + 1 + 1) ≤ (a + 1 + 1) ^ (b + 1) + ((a + 1 + 1) ^ (b + 1) * a + (a + 1 + 1) ^ (b + 1))

Proof state:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≤ (a + 1 + 1) ^ (b + 1) * a + (a + 1 + 1) ^ (b + 1)

Tactic:
rw [pow_succ']

Result:
case succ.succ.succ.succ
a : ℕ
ha : a + 1 + 1 ≠ 1
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * (b + 1) ≤ a ^ (b + 1)
⊢ a + 1 + 1 ≤ (a + 1 + 1) * (a + 1 + 1) ^ b * a + (a + 1 + 1) * (a + 1 + 1) ^ b

Proof state:
case succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a ≠ 1
⊢ a * b + a ≤ a ^ b * a

Tactic:
rcases a with (_|_|a)

Result:
case succ.zero
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
ha : 0 ≠ 1
⊢ 0 * b + 0 ≤ 0 ^ b * 0

case succ.succ.zero
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
ha : 0 + 1 ≠ 1
⊢ (0 + 1) * b + (0 + 1) ≤ (0 + 1) ^ b * (0 + 1)

case succ.succ.succ
b : ℕ
hb : ∀ {a : ℕ}, a ≠ 1 → a * b ≤ a ^ b
a : ℕ
ha : a + 1 + 1 ≠ 1
⊢ (a + 1 + 1) * b + (a + 1 + 1) ≤ (a + 1 + 1) ^ b * (a + 1 + 1)