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 (n / d)
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₁ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -(↑(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]
-- 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 (n / d)
out₁ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -(↑(n / d) : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₂ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -HDiv.hDiv (α := ℤ) (↑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]
-- 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 (n / d)
out₁ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -(↑(n / d) : ℤ)
out₂ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₃ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -⌊HDiv.hDiv (α := ℚ) (↑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]
-- 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 (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 : ℤ)
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₅ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = -HDiv.hDiv (α := ℤ) (- -(↑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]
-- 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 (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 : ℤ)
⊢ ⌈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]
-- 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 (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 : ℤ))
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₇ : ⌈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]
-- 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 (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 : ℤ))
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₈ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := ℚ) (↑(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]
-- 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 (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 : ℚ)⌉
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₉ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ =
  ceil.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑(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]
-- 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 (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 : ℚ)) : α)
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₁₀ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑(↑(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]
-- 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 (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 : ℚ) : α)⌉
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₁₁ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑(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]
-- 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 (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 : ℚ) : α)⌉
⊢ ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = negOfNat (n / d)
have out₁₂ : ⌈HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌉ = ⌈HDiv.hDiv (α := α) (↑(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]
-- 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 : α)
⊢ IsNNRat (fract (HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)))
    (n % d) d
have refine : fract (HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)) =
  HMul.hMul (α := α) (↑(n % d) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)
Tactic: refine ⟨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 : α)
⊢ IsRat
    (fract
      (HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)))
    (HMod.hMod (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)) d
have 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 : α) _)
Tactic: refine ⟨inv, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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)
⊢ IsInt (round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _))) res
have subst : IsInt (round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)))
  (round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)))
Tactic: subst res
Cleared hypotheses: res, hres
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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)
⊢ IsInt (round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)))
    (round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)))
have out : round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)) =
  (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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)
⊢ round (HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)) =
    (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)
have out : round (HDiv.hDiv (α := R) (↑n : R) (↑d : R)) = (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)
Tactic: rw [invOf_eq_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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)
⊢ round (HDiv.hDiv (α := R) (↑n : R) (↑d : R)) = (↑(round (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))) : ℤ)
have out : round (n /. (↑d : ℤ)) = round (n /. (↑d : ℤ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
⊢ n % (↑d : ℤ) = n - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
have rw : n - (↑d : ℤ) * (n / (↑d : ℤ)) = n - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
Tactic: rw [Int.emod_def, Rat.floor_intCast_div_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
rw : n - (↑d : ℤ) * (n / (↑d : ℤ)) = n - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
⊢ n % (↑d : ℤ) = n - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
have rw₁ : n - (↑d : ℤ) * (n / (↑d : ℤ)) = n - (↑d : ℤ) * (n / (↑d : ℤ))
Tactic: rw [Int.emod_def, Rat.floor_intCast_div_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
⊢ ((↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋).natAbs.Coprime d
have this : 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
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
this : HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ) = (↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
⊢ ((↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋).natAbs.Coprime d
have rw : (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
n d : ℕ
n_coprime_d : n.Coprime d
this : HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ) = (↑n : ℤ) - (↑d : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
⊢ (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
have this₁ : d.Coprime n
Tactic: have : d.Coprime n := n_coprime_d.symm
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
have rwa : ∀ (this : d.gcd n = 1), (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
Tactic: rwa [Nat.Coprime, Nat.gcd_rec] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
have rwa₁ : ∀ (this : (n % d).gcd d = 1), (HMod.hMod (α := ℤ) (↑n : ℤ) (↑d : ℤ)).natAbs.Coprime d
Tactic: rwa [Nat.Coprime, Nat.gcd_rec] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
⊢ q.num < (⌊q⌋ + 1) * (↑q.den : ℤ)
have suffices : (↑q.num : ℚ) < HAdd.hAdd (α := ℚ) (↑⌊q⌋ : ℚ) 1 * (↑q.den : ℚ)
Tactic: suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
this : (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < HAdd.hAdd (α := ℚ) (↑⌊q⌋ : ℚ) 1 * (↑q.den : ℚ)
have this₁ : (↑⌊q⌋ : ℚ) = q - fract q
Tactic: have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
⊢ (↑q.num : ℚ) < HAdd.hAdd (α := ℚ) (↑⌊q⌋ : ℚ) 1 * (↑q.den : ℚ)
have suffices : (↑q.num : ℚ) < (q - fract 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]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
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 : ℚ)
have rw : q * (↑q.den : ℚ) + (1 - fract q) * (↑q.den : ℚ) = q * (↑q.den : ℚ) + (1 - fract q) * (↑q.den : ℚ)
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)
have fract : (q - fract q + 1) * (↑q.den : ℚ) = (q + (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
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)
⊢ (q - Int.fract q + 1) * (↑q.den : ℚ) = (↑q.num : ℚ) + (1 - Int.fract q) * (↑q.den : ℚ)
have fract₁ : (q + (1 - Int.fract q)) * (↑q.den : ℚ) = q * (↑q.den : ℚ) + (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
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)
⊢ (q - Int.fract q + 1) * (↑q.den : ℚ) = (↑q.num : ℚ) + (1 - Int.fract q) * (↑q.den : ℚ)
have fract₂ : q * (↑q.den : ℚ) + (1 - Int.fract q) * (↑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
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
this : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
have this₁ : (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