failed to unify same statement

Stream: general

[Bolton Bailey]

import analysis.special_functions.pow

lemma cube_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : (x + 1) ^ 3 ≤ exp (3 * x) :=
begin
  rw mul_comm,
  rw exp_mul,
  apply @rpow_le_rpow (x + 1) (exp x) 3,
end

I get the error message

invalid apply tactic, failed to unify
  (x + 1) ^ 3 ≤ exp x ^ 3
with
  (x + 1) ^ 3 ≤ exp x ^ 3
state:
x : ℝ,
hx : 0 ≤ x
⊢ (x + 1) ^ 3 ≤ exp x ^ 3

What is going on, how can't it unify two expression which print exactly the same. Is there something going on behind the scenes?

[Thomas Browning]

maybe one of those 3's is a nat and one is a real number?

[Eric Rodriguez]

set_option pp.notation false set_option pp.implicit true

is an easy way to see it's different

[Eric Rodriguez]

but rpow is (3:ℝ) whilst the original statement is 3:ℕ

[Kevin Buzzard]

Try convert

[Kyle Miller]

import analysis.special_functions.pow

open real

lemma cube_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : (x + 1) ^ 3 ≤ exp (3 * x) :=
begin
  rw [mul_comm, exp_mul],
  convert @rpow_le_rpow (x + 1) (exp x) 3 _ _ _ using 1,
  have : 3 = ((3 : ℕ) : ℝ) := by norm_num,
  rw [this, real.rpow_nat_cast],
  linarith,
  exact add_one_le_exp_of_nonneg hx,
  linarith,
end