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

State before:
a b y : ℕ
⊢ (0 + y) ^ a - 0 ^ a ≤ (0 + y) ^ (a + b) - 0 ^ (a + b)
Tactic:
cases a <;> cases b <;> cases y <;>
simp [Nat.pow_add]
State after:
case succ.succ.succ
n✝² n✝¹ n✝ : ℕ
⊢ 1 ≤ Nat.succ n✝ ^ Nat.succ n✝¹

State before:
case succ.succ.succ
n✝² n✝¹ n✝ : ℕ
⊢ 1 ≤ Nat.succ n✝ ^ Nat.succ n✝¹
Tactic:
exact le_trans (Nat.pow_le_pow_right (Nat.zero_lt_succ 0) (Nat.succ_le_succ (Nat.zero_le _))) (Nat.pow_le_pow_left (Nat.succ_le_succ (Nat.zero_le _)) _)
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.pow_le_pow_right
State after:
case hx
a b y x : ℕ
⊢ x + 1 + y > 0

case a
a b y x : ℕ
⊢ a ≤ a + b

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

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

State before:
case hx
a b y x : ℕ
⊢ x + 1 + y > 0

case a
a b y x : ℕ
⊢ a ≤ a + b

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

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

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

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

State before:
case a
a b y x : ℕ
⊢ a ≤ a + b

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

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

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

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

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.pow_le_pow_right
State after:
case h.hx
a b y x : ℕ
⊢ x + 1 > 0

case h.a
a b y x : ℕ
⊢ a ≤ a + b

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

State before:
case h.hx
a b y x : ℕ
⊢ x + 1 > 0

case h.a
a b y x : ℕ
⊢ a ≤ a + b

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

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

State before:
case h.a
a b y x : ℕ
⊢ a ≤ a + b

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

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

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