q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
q : ℚ
⊢ q.num < (⌊q⌋ + 1) * ↑q.den
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den by exact_mod_cast this
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
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]
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
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
  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]
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
suffices 0 < (1 - fract q) * q.den by
  rw [← sub_lt_iff_lt_add']
  simpa
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den
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]
no goals
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den
exact mul_pos this (by exact_mod_cast q.pos)
no goals
q : ℚ
this : ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
⊢ q.num < (⌊q⌋ + 1) * ↑q.den
exact_mod_cast this
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
q : ℚ
this : ↑q.num < (q - fract q + 1) * ↑q.den
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
no goals
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
rwa [this]
case this
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den

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
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den
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
case this
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den

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
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
no goals
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
rwa [this]
no goals
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = (q + (1 - fract q)) * ↑q.den
ring
no goals
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
rw [add_mul]
no goals
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
simp
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
rw [← sub_lt_iff_lt_add']
no goals
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den
simpa
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q
q : ℚ
⊢ 0 < 1 - fract q
have : fract q < 1 := fract_lt_one q
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q
have : 0 + fract q < 1 := by simp [this]
no goals
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q
rwa [lt_sub_iff_add_lt]
no goals
q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1
simp [this]
no goals
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < ↑q.den
exact_mod_cast q.pos