have hfqn := calc f q.num = f (q * q.den) := by rw [←Rat.mul_den_eq_num]
                  _ ≤ f q * f q.den := H1 q q.den hq (Nat.cast_pos.mpr q.pos)
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
⊢ 0 < f q
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
⊢ 0 < f q