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

State before:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
apply (Nat.exists_eq_add_of_le hab).elim
State after:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), b = a + a_1 → y ^ a - x ^ a ≤ y ^ b - x ^ b

State before:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), b = a + a_1 → y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
apply (Nat.exists_eq_add_of_le hxy).elim
State after:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), y = x + a_1 → ∀ (a_3 : ℕ), b = a + a_3 → y ^ a - x ^ a ≤ y ^ b - x ^ b

State before:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), y = x + a_1 → ∀ (a_3 : ℕ), b = a + a_3 → y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
intro _ hxy _ hab
State after:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b

State before:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
rw [hxy, hab]
State after:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ (x + a✝¹) ^ a - x ^ a ≤ (x + a✝¹) ^ (a + a✝) - x ^ (a + a✝)

State before:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ (x + a✝¹) ^ a - x ^ a ≤ (x + a✝¹) ^ (a + a✝) - x ^ (a + a✝)
Tactic:
exact blah6
State after:
no goals