awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
⊢ ∃ (c : ℤ),
    n = c * (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num ∧
      (↑d : ℤ) = c * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ)

Tactic:
mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Premises used: Int.cast, Int.cast_natCast, Rat.num, HMul.hMul, congrArg, Rat.exists_eq_mul_div_num_and_eq_mul_div_den, cast, Rat.cast_divInt._simp_1, Rat.den, Exists, HDiv.hDiv, Ne, Nat.cast, LT.lt.ne', funext, And, congr, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
⊢ ∃ (c : ℤ),
    n = c * (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num ∧
      (↑d : ℤ) = c * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ)

Tactic:
exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Premises used: congrArg, Rat.exists_eq_mul_div_num_and_eq_mul_div_den, cast, Ne, Nat.cast, LT.lt.ne', Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
inr :
  ∀ (c : ℤ) (n_eq_c_mul_num : n = c * q.num) (d_eq_c_mul_denom : (↑d : ℤ) = c * (↑q.den : ℤ)),
    q.num / (↑q.den : ℤ) = n / (↑d : ℤ)
⊢ q.num / (↑q.den : ℤ) = n / (↑d : ℤ)

Tactic:
obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩ : ∃ c, n = c * q.num ∧ (d : ℤ) = c * q.den := by
    rw [q_eq]
    exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Premises used: Rat.num, Rat.den, Nat.cast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : (↑d : ℤ) = c * (↑q.den : ℤ)
inr : q.num / (↑q.den : ℤ) = c * q.num / (c * (↑q.den : ℤ))
⊢ q.num / (↑q.den : ℤ) = n / (↑d : ℤ)

Tactic:
rw [n_eq_c_mul_num, d_eq_c_mul_denom]
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : (↑d : ℤ) = c * (↑q.den : ℤ)
inr : 0 < c * (↑q.den : ℤ)
⊢ q.num / (↑q.den : ℤ) = c * q.num / (c * (↑q.den : ℤ))

Tactic:
refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm

Premises used: pos_of_mul_pos_left, Rat.den, Eq.symm, Int.mul_ediv_mul_of_pos, Int.natCast_nonneg
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : (↑d : ℤ) = c * (↑q.den : ℤ)
inr : LT.lt (α := ℤ) 0 (↑d : ℤ)
inr₁ inr₂ inr₃ inr₄ : 0 < d
⊢ 0 < c * (↑q.den : ℤ)

Tactic:
rwa [← d_eq_c_mul_denom, Int.natCast_pos]

Premises used: Int.natCast_pos
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
rw : -⌊HDiv.hDiv (α := ℚ) (-(↑n : ℚ)) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
rw₁ : -⌊HDiv.hDiv (α := ℚ) (↑(-n) : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
rw₂ rw₃ : -(-n / (↑d : ℤ)) = -(-n / (↑d : ℤ))
⊢ -⌊-HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))

Tactic:
rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]

Premises used: Int.cast_neg, neg_div, Rat.floor_intCast_div_natCast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
⊢ ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)

Tactic:
floor_intCast_div_natCast n d

Premises used: Nat.cast, Rat.floor_intCast_div_natCast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
⊢ ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉ = -HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)

Tactic:
ceil_intCast_div_natCast n d

Premises used: Rat.ceil_intCast_div_natCast, Nat.cast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)

Tactic:
positivity
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
rw : ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = (↑(n / d) : ℤ)
⊢ ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋₊ = n / d

Tactic:
rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]

Premises used: Int.natCast_floor_eq_floor, Int.ofNat_inj
-- Module: Mathlib.Data.Rat.Floor
Goal:
n d : ℕ
⊢ ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)

Tactic:
exact floor_intCast_div_natCast n d

Premises used: Nat.cast, Rat.floor_intCast_div_natCast
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
⊢ floor.{u_1} (α := α) (↑x : α) = ⌊x⌋

Tactic:
floor_eq_iff.2 (mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋))

Premises used: Iff.mpr, Rat.cast_lt_intCast._simp_1, Int.cast, Int.floor, congrArg, Rat.intCast_le_cast._simp_1, cast, Rat.cast, LE.le, Nat.cast, Int.floor_eq_iff, And, HAdd.hAdd, congr, LT.lt, Iff.mp, Eq.refl, Int.cast_add._simp_1, OfNat.ofNat, Eq.symm, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
rw : -ceil.{u_1} (α := α) (↑x : α) = -⌈x⌉
rw₁ : floor.{u_1} (α := α) (-(↑x : α)) = -⌈x⌉
rw₂ : floor.{u_1} (α := α) (-(↑x : α)) = ⌊-x⌋
rw₃ : floor.{u_1} (α := α) (↑(-x) : α) = ⌊-x⌋
rw₄ rw₅ : ⌊-x⌋ = ⌊-x⌋
⊢ ceil.{u_1} (α := α) (↑x : α) = ⌈x⌉

Tactic:
rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]

Premises used: Int.floor_neg, Rat.floor_cast, neg_inj, Rat.cast_neg
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
⊢ (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2

Tactic:
simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
⊢ (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2

Tactic:
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
this : (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2
rw : ⌊(↑x : α) + 1 / 2⌋ = round x
rw₁ : ⌊(↑x : α) + 1 / 2⌋ = ⌊x + 1 / 2⌋
rw₂ : floor.{u_1} (α := α) (↑(x + 1 / 2) : α) = ⌊x + 1 / 2⌋
rw₃ rw₄ : ⌊x + 1 / 2⌋ = ⌊x + 1 / 2⌋
⊢ round.{u_1} (α := α) (↑x : α) = round x

Tactic:
rw [round_eq, round_eq, ← this, floor_cast]

Premises used: Rat.floor_cast, round_eq
-- Module: Mathlib.Data.Rat.Floor
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
⊢ Eq.{u_1 + 1} (α := α) (↑(fract x) : α) (fract (↑x : α))

Tactic:
simp only [fract, cast_sub, cast_intCast, floor_cast]

Premises used: Rat.cast_intCast, Int.fract, Rat.floor_cast, Rat.cast_sub
-- Module: Mathlib.Data.Rat.Floor
Goal:
x : ℚ
⊢ (fract x).den = x.den

Tactic:
Rat.sub_intCast_den _ _

Premises used: Rat.sub_intCast_den
-- 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 : ℕ
⊢ floor.{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 (floor.{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 : ℤ
⊢ floor.{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 (floor.{u_3} (α := R) (↑m : R)) m

Tactic:
exact ⟨by simp⟩
-- 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 : α)
out :
  ⌊HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ = (↑(n / d) : ℤ)
⊢ IsNat ⌊HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ (n / d)

Tactic:
constructor
-- 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 : α)
out : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
⊢ ⌊HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ = (↑(n / d) : ℤ)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- 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 : α)
out : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
out₁ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
out₂ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = floor.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : α)
out₃ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(↑n : ℚ) : α) (↑(↑d : ℚ) : α)⌋
out₄ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑n : α) (↑(↑d : ℚ) : α)⌋
out₅ out₆ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)

Tactic:
rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, cast_natCast]

Premises used: Rat.floor_natCast_div_natCast, Rat.floor_cast, Rat.cast_div, Rat.cast_natCast, Int.ofNat_ediv_ofNat
-- 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 : α)
out :
  ⌊HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ =
    (↑(negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat) : ℤ)
⊢ IsInt ⌊HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋
    (negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat)

Tactic:
constructor
-- 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 : α)
out : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat
⊢ ⌊HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ =
    (↑(negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat) : ℤ)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]

Premises used: div_eq_mul_inv, Int.cast_id, invOf_eq_inv
-- 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 : α)
out : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat

Tactic:
rw [← ceil_intCast_div_natCast n d, Int.cast_natCast]

Premises used: Int.cast_natCast, Rat.ceil_intCast_div_natCast, Nat.cast
-- 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 : α)
out : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -ofNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
out₁ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -(↑⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat : ℤ)
out₂ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉
out₃ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -⌈HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑d : ℚ)⌉
out₄ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = - -HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)
out₅ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)
out₆ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -ofNat n / (↑d : ℤ)
out₇ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat n / (↑d : ℤ)
out₈ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := ℚ) (↑(negOfNat n) : ℚ) (↑d : ℚ)⌋
out₉ :
  ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ =
    floor.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑(negOfNat n) : ℚ) (↑d : ℚ)) : α)
out₁₀ :
  ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(↑(negOfNat n) : ℚ) : α) (↑(↑d : ℚ) : α)⌋
out₁₁ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑(↑d : ℚ) : α)⌋
out₁₂ out₁₃ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat

Tactic:
rw [@negOfNat_eq (toNat _), ofNat_eq_natCast,
    natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg)),
    ← Int.cast_natCast n, ceil_intCast_div_natCast n d, neg_neg, ← ofNat_eq_natCast, ← negOfNat_eq,
    ← floor_intCast_div_natCast (.negOfNat n) d, ← floor_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Rat.cast_intCast, Rat.ceil_intCast_div_natCast, Rat.floor_cast, Int.ofNat_eq_natCast, neg_neg, Int.ceil_nonneg, Rat.cast_div, Nat.cast, Int.natCast_toNat_eq_self, Rat.cast_natCast, Rat.floor_intCast_div_natCast, Int.negOfNat, 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 : ℕ
⊢ ceil.{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 (ceil.{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 : ℤ
⊢ ceil.{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 (ceil.{u_3} (α := R) (↑m : R)) m

Tactic:
exact ⟨by simp⟩
-- 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 : α)
out :
  ⌈HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
    (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
⊢ IsNat ⌈HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉
    (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat

Tactic:
constructor
-- 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 : α)
out : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
⊢ ⌈HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
    (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- 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 : α)
out : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑⌈HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑d : ℚ)⌉.toNat : ℤ)
out₁ :
  ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ =
    (↑(ceil.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑d : ℚ)) : α)).toNat : ℤ)
out₂ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑⌈HDiv.hDiv (α := α) (↑(↑(↑n : ℤ) : ℚ) : α) (↑(↑d : ℚ) : α)⌉.toNat : ℤ)
out₃ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑⌈HDiv.hDiv (α := α) (↑(↑n : ℤ) : α) (↑(↑d : ℚ) : α)⌉.toNat : ℤ)
out₄ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑⌈HDiv.hDiv (α := α) (↑(↑n : ℤ) : α) (↑d : α)⌉.toNat : ℤ)
out₅ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉.toNat : ℤ)
out₆ out₇ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)

Tactic:
rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast, Int.cast_natCast,
    Int.natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg))]

Premises used: Iff.mpr, Int.cast_natCast, Rat.cast_intCast, Rat.ceil_intCast_div_natCast, Int.ceil_nonneg, Rat.cast_div, Nat.cast, Int.natCast_toNat_eq_self, Rat.cast_natCast, Rat.ceil_cast
-- 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 : α)
out :
  ⌈HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
    (↑(negOfNat (n / d)) : ℤ)
⊢ IsInt ⌈HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉
    (negOfNat (n / d))

Tactic:
constructor
-- 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 : α)
out : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
⊢ ⌈HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
    (↑(negOfNat (n / d)) : ℤ)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]

Premises used: div_eq_mul_inv, Int.cast_id, invOf_eq_inv
-- 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 : α)
out : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -ofNat (n / d)
out₁ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -(↑(n / d) : ℤ)
out₂ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
out₃ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
out₄ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
out₅ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -HDiv.hDiv (α := ℤ) (- -(↑n : ℤ)) (↑d : ℤ)
out₆ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -(- -ofNat n / (↑d : ℤ))
out₇ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -(-negOfNat n / (↑d : ℤ))
out₈ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := ℚ) (↑(negOfNat n) : ℚ) (↑d : ℚ)⌉
out₉ :
  ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ =
    ceil.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑(negOfNat n) : ℚ) (↑d : ℚ)) : α)
out₁₀ :
  ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑(↑(negOfNat n) : ℚ) : α) (↑(↑d : ℚ) : α)⌉
out₁₁ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑(↑d : ℚ) : α)⌉
out₁₂ out₁₃ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)

Tactic:
rw [@negOfNat_eq (n / d), ofNat_eq_natCast, ← ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    floor_natCast_div_natCast n d, ← neg_neg (n : ℤ), ← ofNat_eq_natCast, ← negOfNat_eq,
    ← ceil_intCast_div_natCast (.negOfNat n) d, ← ceil_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast]

Premises used: Rat.cast_intCast, Rat.ceil_intCast_div_natCast, Rat.floor_natCast_div_natCast, Int.ofNat_eq_natCast, neg_neg, Rat.cast_div, Nat.cast, Rat.cast_natCast, Rat.ceil_cast, Int.ofNat_ediv_ofNat, Int.negOfNat, Int.negOfNat_eq
-- Module: Mathlib.Data.Rat.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
m : ℕ
⊢ Eq.{u_2 + 1} (α := R) (fract (↑m : R)) (↑0 : R)

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

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

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

Tactic:
exact ⟨by simp⟩
-- 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 : α)
⊢ IsNNRat (fract (HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)))
    (n % d) d

Tactic:
⟨inv, ?_⟩

Premises used: Mathlib.Meta.NormNum.IsNNRat.mk
-- 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 : α)
refine :
  fract (HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)) =
    HMul.hMul (α := α) (↑(n % d) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)
⊢ IsNNRat (fract (HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)))
    (n % d) d

Tactic:
refine ⟨inv, ?_⟩
-- 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 (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)) =
    HMul.hMul (α := α) (↑(n % d) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_natCast_eq_div_natCast_mod]

Premises used: div_eq_mul_inv, Int.fract_div_natCast_eq_div_natCast_mod, invOf_eq_inv
-- 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 : α)
⊢ IsRat
    (fract
      (HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)))
    (HMod.hMod (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)) d

Tactic:
⟨inv, ?_⟩

Premises used: Mathlib.Meta.NormNum.IsRat.mk
-- 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 : α)
refine :
  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 : α) _)
⊢ IsRat
    (fract
      (HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)))
    (HMod.hMod (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)) d

Tactic:
refine ⟨inv, ?_⟩