rw [←hae]
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
hh0 : ↑a ^ n ≤ f (a ^ n)
⊢ f a ^ n = ↑a ^ n
no goals