cases pn with
| zero => simp [show Nat.succ 0 = 1 by rfl, pow_one]
| succ pn =>
  have hpn' := hpn pn.succ_pos
  rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
  have hxp : 0 < x := zero_lt_one.trans hx
  calc f ((x ^ (pn+1)) * x)
      ≤ f (x ^ (pn+1)) * f x := H1 (x ^ (pn+1)) x (pow_pos hxp (pn+1)) hxp
    _ ≤ (f x) ^ (pn+1) * f x := (mul_le_mul_right (f_pos_of_pos hxp H1 H4)).mpr hpn'
case succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn → f (x ^ pn) ≤ f x ^ pn
hn : 0 < pn + 1
⊢ f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
no goals