Theorem: Imo2013P5.fx_gt_xm1 (Compfiles/Imo2013P5.lean)

State before:
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
⊢ ↑x - 1 < f x
Tactic:
have hx0 :=
  calc (x - 1 : ℝ)
        < ⌊x⌋₊   := by exact_mod_cast Nat.sub_one_lt_floor x
      _ ≤ f ⌊x⌋₊ := H4 _ (Nat.floor_pos.2 hx)
State after:
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

State before:
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
Tactic:
obtain h_eq | h_lt := (Nat.floor_le $ zero_le_one.trans hx).eq_or_lt
State after:
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

State before:
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
Tactic:
calc (x - 1 : ℝ) < f ⌊x⌋₊ := hx0
  _ < f (x - ⌊x⌋₊) + f ⌊x⌋₊ := lt_add_of_pos_left _ (f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
  _ ≤ f (x - ⌊x⌋₊ + ⌊x⌋₊)   := H2 _ _ (sub_pos.mpr h_lt) (Nat.cast_pos.2 (Nat.floor_pos.2 hx))
  _ = f x                   := by rw [sub_add_cancel]
State after:
no goals

State before:
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
⊢ ↑x - 1 < ↑⌊x⌋₊
Tactic:
exact_mod_cast Nat.sub_one_lt_floor x
State after:
no goals

State before:
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
Tactic:
rwa [h_eq] at hx0
State after:
no goals

State before:
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
⊢ f (x - ↑⌊x⌋₊ + ↑⌊x⌋₊) = f x
Tactic:
rw [sub_add_cancel]
State after:
no goals