have hNp : 0 < N := by
  by_contra H; push_neg at H; rw [le_zero_iff.mp H] at hN; linarith
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ f x = ↑x
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f x = ↑x