Theorem: blah4 (HMem/Trace/Master.lean)

State before:
a b : ℕ
⊢ 0 ^ (a + b) - 0 ^ a ≤ (0 + 1) ^ (a + b) - (0 + 1) ^ a
Tactic:
cases a <;> cases b <;> simp
State after:
no goals

State before:
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a ≤ (x + 1 + 1) ^ (a + b) - (x + 1 + 1) ^ a
Tactic:
apply Nat.le_sub_of_add_le
State after:
case h
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + 1) ^ a ≤ (x + 1 + 1) ^ (a + b)

State before:
case h
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + 1) ^ a ≤ (x + 1 + 1) ^ (a + b)
Tactic:
rw [← Nat.sub_add_comm, add_comm, Nat.sub_add_comm]
State after:
case h
a b x : ℕ
⊢ (x + 1 + 1) ^ a - (x + 1) ^ a + (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

State before:
case h
a b x : ℕ
⊢ (x + 1 + 1) ^ a - (x + 1) ^ a + (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.add_le_of_le_sub _ blah3
State after:
a b x : ℕ
⊢ (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

State before:
a b x : ℕ
⊢ (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.pow_le_pow_left (Nat.le_succ _)
State after:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

State before:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.pow_le_pow_left (Nat.le_succ _)
State after:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

State before:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.pow_le_pow_right (Nat.zero_lt_succ _)
State after:
case h
a b x : ℕ
⊢ a ≤ a + b

State before:
case h
a b x : ℕ
⊢ a ≤ a + b
Tactic:
apply Nat.le_add_right
State after:
no goals