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

State before:
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a
Tactic:
ring_nf
State after:
a x : ℕ
⊢ x * x ^ a + (1 + x) ^ a ≤ x * (1 + x) ^ a + x ^ a + (1 + x) ^ a

State before:
a x : ℕ
⊢ x * x ^ a + (1 + x) ^ a ≤ x * (1 + x) ^ a + x ^ a + (1 + x) ^ a
Tactic:
apply add_le_add_right
State after:
case bc
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a + x ^ a

State before:
case bc
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a + x ^ a
Tactic:
apply le_add_right
State after:
case bc.h
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a

State before:
case bc.h
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a
Tactic:
apply Nat.mul_le_mul_left
State after:
case bc.h.h
a x : ℕ
⊢ x ^ a ≤ (1 + x) ^ a

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

State before:
case bc.h.h.h
a x : ℕ
⊢ x ≤ 1 + x
Tactic:
apply Nat.le_add_left
State after:
no goals