have h2 := calc f x + f (a^N - x)
              ≤ f (x + (a^N - x)) := H2 x (a^N - x) hxp (zero_lt_one.trans h_big_enough)
            _ = f (a^N)           := by ring_nf
            _ = (a^N : ℝ)         := fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae
            _ = (x:ℝ) + ((a^N:ℝ) - (x:ℝ))     := by ring
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
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
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x = ↑x