-- Mathlib/Data/Rat/Floor.lean
theorem num_lt_succ_floor_mul_den (q : ℚ) : q.num < (⌊q⌋ + 1) * q.den

Proof state:
q : ℚ
⊢ 0 < 1 - fract q

Tactic:
have : fract q < 1 := fract_lt_one q

Result:
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q

Proof state:
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den

Tactic:
calc
  (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
  _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
  _ = q.num + (1 - fract q) * q.den := by simp

Result:
no goals

Proof state:
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Tactic:
have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
  calc
    (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
    _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
    _ = q.num + (1 - fract q) * q.den := by simp

Result:
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Proof state:
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q + (1 - fract q)) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.den

Tactic:
rw [add_mul]

Result:
no goals

Proof state:
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Tactic:
rwa [this]

Result:
no goals

Proof state:
q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Tactic:
suffices (q.num : ℚ) < (q - fract q + 1) * q.den by
  have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
  rwa [this]

Result:
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Proof state:
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

Tactic:
suffices 0 < (1 - fract q) * q.den by
  rw [← sub_lt_iff_lt_add']
  simpa

Result:
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den

Proof state:
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den

Tactic:
exact mul_pos this (by exact mod_cast q.pos)

Result:
no goals

Proof state:
q : ℚ
this : ↑q.num < (q - fract q + 1) * ↑q.den
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Tactic:
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q

Result:
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Proof state:
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ q * ↑q.den + (1 - fract q) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den

Tactic:
simp

Result:
no goals

Proof state:
q : ℚ
⊢ q.num < (⌊q⌋ + 1) * ↑q.den

Tactic:
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this

Result:
q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Proof state:
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den

Tactic:
simpa

Result:
no goals

Proof state:
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q

Tactic:
rwa [lt_sub_iff_add_lt]

Result:
no goals

Proof state:
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q

Tactic:
have : 0 + fract q < 1 := by simp [this]

Result:
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q

Proof state:
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

Tactic:
rw [← sub_lt_iff_lt_add']

Result:
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den

Proof state:
q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1

Tactic:
simp [this]

Result:
no goals

Proof state:
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = (q + (1 - fract q)) * ↑q.den

Tactic:
ring

Result:
no goals

Proof state:
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den

Tactic:
have : 0 < 1 - fract q := by
  have : fract q < 1 := fract_lt_one q
  have : 0 + fract q < 1 := by simp [this]
  rwa [lt_sub_iff_add_lt]

Result:
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den

Proof state:
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < ↑q.den

Tactic:
exact mod_cast q.pos

Result:
no goals

Proof state:
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Tactic:
suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den by
  have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
    calc
      (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
      _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
      _ = q.num + (1 - fract q) * q.den := by simp
  rwa [this]

Result:
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

Proof state:
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Tactic:
rwa [this]

Result:
no goals