awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)⌉
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₄ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = - -HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₅ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₆ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -ofNat n / (↑d : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₇ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat n / (↑d : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₈ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := ℚ) (↑(negOfNat n) : ℚ) (↑d : ℚ)⌋
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₉ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ =
  floor.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑(negOfNat n) : ℚ) (↑d : ℚ)) : α)
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)) : α)
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₁₀ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(↑(negOfNat n) : ℚ) : α) (↑(↑d : ℚ) : α)⌋
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ) : α)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₁₁ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑(↑d : ℚ) : α)⌋
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ) : α)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₁₂ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ IsNat ⌈HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉
    (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat
have out : ⌈HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
  (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ ⌈HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
    (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
Tactic: simp only [invOf_eq_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out : ⌈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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out₁ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ =
  (↑(ceil.{u_1} (α := α) (↑(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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out₂ : ⌈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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out₃ : ⌈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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out₄ : ⌈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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out₅ : ⌈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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = (↑(-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat : ℤ)
have out₆ : ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌉
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))]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ IsInt ⌈HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉
    (negOfNat (n / d))
have out : ⌈HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
  (↑(negOfNat (n / d)) : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ ⌈HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌉ =
    (↑(negOfNat (n / d)) : ℤ)
have out : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
Tactic: simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -ofNat (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]