awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ fract (HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)) =
    HMul.hMul (α := α) (↑(HMod.hMod (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)) : α)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_intCast_eq_div_intCast_mod,
    negOfNat_eq, ofNat_eq_natCast]

Premises used: Int.ofNat_eq_natCast, div_eq_mul_inv, invOf_eq_inv, Int.fract_div_intCast_eq_div_intCast_mod, Int.negOfNat_eq
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
m : ℕ
⊢ round.{u_3} (α := R) (↑m : R) = (↑m : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
m : ℕ
⊢ IsNat (round.{u_3} (α := R) (↑m : R)) m

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
m : ℤ
⊢ round.{u_3} (α := R) (↑m : R) = (↑m : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
m : ℤ
⊢ IsInt (round.{u_3} (α := R) (↑m : R)) m

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
d : ℕ
res : ℤ
hres : round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = res
inv : Invertible (α := R) (↑d : R)
subst :
  IsInt (round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)))
    (round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)))
⊢ IsInt (round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _))) res

Tactic:
subst res
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
d : ℕ
inv : Invertible (α := R) (↑d : R)
out :
  round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)) =
    (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)
⊢ IsInt (round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)))
    (round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)))

Tactic:
constructor
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
d : ℕ
inv : Invertible (α := R) (↑d : R)
out : round (HDiv.hDiv (α := R) (↑n : R) (↑d : R)) = (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)
⊢ round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)) =
    (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)

Tactic:
rw [invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
d : ℕ
inv : Invertible (α := R) (↑d : R)
out out₁ out₂ out₃ : round (n /. (↑d : ℤ)) = round (n /. (↑d : ℤ))
⊢ round (HDiv.hDiv (α := R) (↑n : R) (↑d : R)) = (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
rw : n - (↑d : ℤ) * (n / (↑d : ℤ)) = n - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
rw₁ rw₂ : n - (↑d : ℤ) * (n / (↑d : ℤ)) = n - (↑d : ℤ) * (n / (↑d : ℤ))
⊢ n % (↑d : ℤ) = n - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋

Tactic:
rw [Int.emod_def, Rat.floor_intCast_div_natCast]

Premises used: Int.emod_def, Rat.floor_intCast_div_natCast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
⊢ HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ) = (↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋

Tactic:
have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
this : HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ) = (↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
rw : (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
⊢ ((↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋).natAbs.Coprime d

Tactic:
rw [← this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
this : HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ) = (↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
⊢ d.Coprime n

Tactic:
have : d.Coprime n := n_coprime_d.symm
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
this_1 : HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ) = (↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
this : d.Coprime n
rwa : ∀ (this : d.gcd n = 1), (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (n % d).gcd d = 1), (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
⊢ (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d

Tactic:
rwa [Nat.Coprime, Nat.gcd_rec] at this

Premises used: Nat.Coprime, Nat.gcd_rec
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
suffices : (↑q.num : ℚ) < HAdd.hAdd (α := ℚ) (↑⌊q⌋ : ℚ) 1 * (↑q.den : ℚ)
⊢ q.num < (⌊q⌋ + 1) * (↑q.den : ℤ)

Tactic:
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
⊢ (↑⌊q⌋ : ℚ) = q - fract q

Tactic:
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this_1 : (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
this : (↑⌊q⌋ : ℚ) = q - fract q
rwa rwa₁ rwa₂ rwa₃ : (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < HAdd.hAdd (α := ℚ) (↑⌊q⌋ : ℚ) 1 * (↑q.den : ℚ)

Tactic:
rwa [this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
suffices : (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < HAdd.hAdd (α := ℚ) (↑⌊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]
-- Module: Mathlib.Data.Rat.Floor
Goal:
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
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
rw rw₁ : q * (↑q.den : ℚ) + (1 - fract q) * (↑q.den : ℚ) = q * (↑q.den : ℚ) + (1 - fract q) * (↑q.den : ℚ)
⊢ (q + (1 - fract q)) * (↑q.den : ℚ) = q * (↑q.den : ℚ) + (1 - fract q) * (↑q.den : ℚ)

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Data.Rat.Floor
Goal:
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
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - Int.fract q) * (↑q.den : ℚ)
fract : (q - Int.fract q + 1) * (↑q.den : ℚ) = (q + (1 - Int.fract q)) * (↑q.den : ℚ)
fract₁ : (q + (1 - Int.fract q)) * (↑q.den : ℚ) = q * (↑q.den : ℚ) + (1 - Int.fract q) * (↑q.den : ℚ)
fract₂ : q * (↑q.den : ℚ) + (1 - Int.fract q) * (↑q.den : ℚ) = (↑q.num : ℚ) + (1 - Int.fract q) * (↑q.den : ℚ)
⊢ (q - Int.fract q + 1) * (↑q.den : ℚ) = (↑q.num : ℚ) + (1 - Int.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

Premises used: Rat.num, Int.fract, HSub.hSub, Rat.den, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Rat.Floor
Goal:
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:
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
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this_1 : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
this : (q - fract q + 1) * (↑q.den : ℚ) = (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
rwa rwa₁ rwa₂ rwa₃ : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)

Tactic:
rwa [this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
suffices : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
⊢ (↑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]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : 0 < (1 - fract q) * (↑q.den : ℚ)
rw : HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.num : ℚ) < (1 - fract q) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)

Tactic:
rw [← sub_lt_iff_lt_add']

Premises used: sub_lt_iff_lt_add'
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : 0 < (1 - fract q) * (↑q.den : ℚ)
⊢ HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.num : ℚ) < (1 - fract q) * (↑q.den : ℚ)

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
suffices : 0 < (1 - fract q) * (↑q.den : ℚ)
⊢ (↑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
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
⊢ fract q < 1

Tactic:
have : fract q < 1 := fract_lt_one q
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1

Tactic:
simp [this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1

Tactic:
have : 0 + fract q < 1 := by simp [this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this_1 : fract q < 1
this : 0 + fract q < 1
rwa rwa₁ rwa₂ rwa₃ : 0 + fract q < 1
⊢ 0 < 1 - fract q

Tactic:
rwa [lt_sub_iff_add_lt]

Premises used: lt_sub_iff_add_lt
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
⊢ 0 < 1 - fract q

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]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : 0 < 1 - fract q
⊢ LT.lt (α := ℚ) 0 (↑q.den : ℚ)

Tactic:
mod_cast q.pos

Premises used: Rat.pos, congrArg, Nat.cast_lt._simp_1, cast, Rat.den, Nat.cast, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : 0 < 1 - fract q
⊢ LT.lt (α := ℚ) 0 (↑q.den : ℚ)

Tactic:
exact mod_cast q.pos

Premises used: Rat.pos
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * (↑q.den : ℚ)

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

Premises used: mul_pos
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
⊢ 0 < q.num

Tactic:
have q_num_pos : 0 < q.num := Rat.num_pos.mpr q_pos
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
⊢ (↑q.num.natAbs : ℤ) = q.num

Tactic:
have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
⊢ let q_inv := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ);
  q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)

Tactic:
set q_inv : ℚ := q.den / q.num with q_inv_def

Premises used: Rat.num, Rat.den
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
rw : q⁻¹ = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
rw₁ : (↑q.den : ℤ) /. q.num = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
rw₂ : HDiv.hDiv (α := ℚ) (↑(↑q.den : ℤ) : ℚ) (↑q.num : ℚ) = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
rw₃ rw₄ : HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ) = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
⊢ q⁻¹ = q_inv

Tactic:
rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]

Premises used: Int.cast_natCast, Rat.divInt_eq_div, Rat.inv_def
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
⊢ q⁻¹ = q_inv

Tactic:
have q_inv_eq : q⁻¹ = q_inv := by rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (q_inv - (↑⌊q_inv⌋ : ℚ)).num < q.num
rwa rwa₁ rwa₂ rwa₃ : (fract q_inv).num < q.num
⊢ (fract q⁻¹).num < q.num

Tactic:
rwa [q_inv_eq]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
suffices : (q_inv - (↑⌊q_inv⌋ : ℚ)).num < q.num
⊢ (fract q⁻¹).num < q.num

Tactic:
suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
simp :
  (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ) - (↑⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)⌋ : ℚ)).num < q.num
⊢ (q_inv - (↑⌊q_inv⌋ : ℚ)).num < q.num

Tactic:
simp only [gt_iff_lt, q_inv]

Premises used: gt_iff_lt
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
field_simp :
  (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)⌋ : ℚ)) /
        (↑q.num : ℚ)).num <
    q.num
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ) - (↑⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)⌋ : ℚ)).num < q.num

Tactic:
field_simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)⌋ : ℚ)) /
        (↑q.num : ℚ)).num <
    q.num

Tactic:
simp [q_inv, this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
suffices : (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
⊢ (q_inv - (↑⌊q_inv⌋ : ℚ)).num < q.num

Tactic:
suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by
    simp only [gt_iff_lt, q_inv]
    field_simp
    simp [q_inv, this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
suffices : ((↑q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num = (↑q.den : ℤ) - q.num * ⌊q_inv⌋

Tactic:
suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den : ℤ) - (↑q.num.natAbs : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num.natAbs : ℚ)⌋).natAbs.Coprime
    q.num.natAbs

Tactic:
have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
tmp :
  ((↑q.den : ℤ) - (↑q.num.natAbs : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num.natAbs : ℚ)⌋).natAbs.Coprime
    q.num.natAbs
⊢ ((↑q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs

Tactic:
simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp

Premises used: Nat.cast_natAbs, LT.lt.le, abs_of_nonneg
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num = (↑q.den : ℤ) - q.num * ⌊q_inv⌋

Tactic:
have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this_1 : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
this :
  (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num = (↑q.den : ℤ) - q.num * ⌊q_inv⌋
rwa rwa₁ rwa₂ rwa₃ : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num

Tactic:
rwa [this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
suffices : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num

Tactic:
suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
    rwa [this]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
⊢ q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)

Tactic:
have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
rwa :
  ∀ (this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + HMul.hMul (α := ℤ) 1 (↑q⁻¹.den : ℤ)),
    q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)), q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)

Tactic:
rwa [right_distrib, one_mul] at this

Premises used: right_distrib, one_mul
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)

Tactic:
have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
this_1 : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)), q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)

Tactic:
rwa [← sub_lt_iff_lt_add'] at this

Premises used: sub_lt_iff_lt_add'
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
⊢ q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)

Tactic:
have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den := by
    have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
    have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
    rwa [← sub_lt_iff_lt_add'] at this
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
⊢ q.den.Coprime q.num.natAbs

Tactic:
have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm