obtain h_eq | h_lt := (Nat.floor_le $ zero_le_one.trans hx).eq_or_lt
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
hx0 : ↑x - 1 < f ↑⌊x⌋₊
⊢ ↑x - 1 < f x
case inl
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
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_eq : ↑⌊x⌋₊ = x
⊢ ↑x - 1 < f x

case inr
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
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_lt : ↑⌊x⌋₊ < x
⊢ ↑x - 1 < f x