awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
n d : ℤ
⊢ HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = n /. d
have rw : HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
Tactic: rw [divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d
have pos : ∀ (hd : d = 0), n /. x * (x /. d) = n /. d
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
pos : ∀ (hd : d = 0), n /. x * (x /. d) = n /. d
⊢ n /. x * (x /. d) = n /. d
have neg : ∀ (hd : ¬d = 0), n /. x * (x /. d) = n /. d
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d
have pos : n /. x * (x /. 0) = n /. 0
Tactic: rw [hd]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
have neg : n * x /. (x * d) = n /. d
Tactic: rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
neg : n * x /. (x * d) = n /. d
⊢ n /. x * (x /. d) = n /. d
have neg₁ : n * x /. (d * x) = n /. d
Tactic: rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
neg : n * x /. (x * d) = n /. d
neg₁ : n * x /. (d * x) = n /. d
⊢ n /. x * (x /. d) = n /. d
have neg₂ : n /. d = n /. d
Tactic: rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
hq : q.den = 1
| q
have rw : q.num /. (↑1 : ℤ)
Tactic: rw [← num_divInt_den q, hq]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
hq : q.den = 1
⊢ (↑q.num : ℚ) = q
have conv_rhs : (↑q.num : ℚ) = q.num /. (↑1 : ℤ)
Tactic: conv_rhs => rw [← num_divInt_den q, hq]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
hq : q.den = 1
⊢ (↑q.num : ℚ) = q.num /. (↑1 : ℤ)
have rw : q.num /. 1 = q.num /. (↑1 : ℤ)
Tactic: rw [intCast_eq_divInt]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (hypothesis)
Goal:
q : ℚ
h : q.isInt = true
⊢ q = (↑q.num : ℚ)
have h₁ : q.den = 1
Tactic: rw [Rat.isInt, Nat.beq_eq_true_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q a_1 b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C { num := n, den := d, den_nz := nz, reduced := red }
have rw : C (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑(↑d : ℤ) : ℚ))
Tactic: rw [Rat.mk_eq_divInt, Rat.divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
⊢ ⌈q⌉ = -(-q.num / (↑q.den : ℤ))
have change : -⌊-q⌋ = -(-q.num / (↑q.den : ℤ))
Tactic: change -⌊-q⌋ = _
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
⊢ -⌊-q⌋ = -(-q.num / (↑q.den : ℤ))
have rw : -((-q).num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
Tactic: rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
rw : -((-q).num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
⊢ -⌊-q⌋ = -(-q.num / (↑q.den : ℤ))
have rw₁ : -(-q.num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
Tactic: rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
rw : -((-q).num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
rw₁ : -(-q.num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
⊢ -⌊-q⌋ = -(-q.num / (↑q.den : ℤ))
have rw₂ : -(-q.num / (↑q.den : ℤ)) = -(-q.num / (↑q.den : ℤ))
Tactic: rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
⊢ ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = n / (↑d : ℤ)
have rw : (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
Tactic: rw [Rat.floor_def']
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
⊢ (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
have inl : (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).den : ℤ) = n / (↑0 : ℤ)
Tactic: obtain rfl | hd := eq_zero_or_pos (a := d)
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
inl : (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).den : ℤ) = n / (↑0 : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
have inr : ∀ (hd : 0 < d),
  (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
Tactic: obtain rfl | hd := eq_zero_or_pos (a := d)
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
hd : 0 < d
⊢ (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
have inr : let q := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ);
∀ (q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)), q.num / (↑q.den : ℤ) = n / (↑d : ℤ)
Tactic: set q := (n : ℚ) / d with q_eq
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
⊢ q.num / (↑q.den : ℤ) = n / (↑d : ℤ)
have 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 : ℤ)
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')
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ q.num / (↑q.den : ℤ) = n / (↑d : ℤ)
have inr : q.num / (↑q.den : ℤ) = c * q.num / (c * (↑q.den : ℤ))
Tactic: rw [n_eq_c_mul_num, d_eq_c_mul_denom]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ q.num / (↑q.den : ℤ) = c * q.num / (c * (↑q.den : ℤ))
have inr : 0 < c * (↑q.den : ℤ)
Tactic: refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ 0 < c * (↑q.den : ℤ)
have inr : LT.lt (α := ℤ) 0 (↑d : ℤ)
Tactic: rwa [← d_eq_c_mul_denom, Int.natCast_pos]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
⊢ -⌊-HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
have rw : -⌊HDiv.hDiv (α := ℚ) (-(↑n : ℚ)) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
Tactic: rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
rw : -⌊HDiv.hDiv (α := ℚ) (-(↑n : ℚ)) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
⊢ -⌊-HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
have rw₁ : -⌊HDiv.hDiv (α := ℚ) (↑(-n) : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
Tactic: rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n : ℤ
d : ℕ
rw : -⌊HDiv.hDiv (α := ℚ) (-(↑n : ℚ)) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
rw₁ : -⌊HDiv.hDiv (α := ℚ) (↑(-n) : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
⊢ -⌊-HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = -(-n / (↑d : ℤ))
have rw₂ : -(-n / (↑d : ℤ)) = -(-n / (↑d : ℤ))
Tactic: rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
n d : ℕ
⊢ ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋₊ = n / d
have rw : ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = (↑(n / d) : ℤ)
Tactic: rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]
-- 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 α
x : ℚ
⊢ ceil.{u_1} (α := α) (↑x : α) = ⌈x⌉
have rw : -ceil.{u_1} (α := α) (↑x : α) = -⌈x⌉
Tactic: rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
-- 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 α
x : ℚ
rw : -ceil.{u_1} (α := α) (↑x : α) = -⌈x⌉
⊢ ceil.{u_1} (α := α) (↑x : α) = ⌈x⌉
have rw₁ : floor.{u_1} (α := α) (-(↑x : α)) = -⌈x⌉
Tactic: rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
-- 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 α
x : ℚ
rw : -ceil.{u_1} (α := α) (↑x : α) = -⌈x⌉
rw₁ : floor.{u_1} (α := α) (-(↑x : α)) = -⌈x⌉
⊢ ceil.{u_1} (α := α) (↑x : α) = ⌈x⌉
have rw₂ : floor.{u_1} (α := α) (-(↑x : α)) = ⌊-x⌋
Tactic: rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
-- 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 α
x : ℚ
rw : -ceil.{u_1} (α := α) (↑x : α) = -⌈x⌉
rw₁ : floor.{u_1} (α := α) (-(↑x : α)) = -⌈x⌉
rw₂ : floor.{u_1} (α := α) (-(↑x : α)) = ⌊-x⌋
⊢ ceil.{u_1} (α := α) (↑x : α) = ⌈x⌉
have rw₃ : floor.{u_1} (α := α) (↑(-x) : α) = ⌊-x⌋
Tactic: rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
-- 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 α
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⌋
⊢ ceil.{u_1} (α := α) (↑x : α) = ⌈x⌉
have rw₄ : ⌊-x⌋ = ⌊-x⌋
Tactic: rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : ℚ
⊢ round.{u_1} (α := α) (↑x : α) = round x
have this : (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2
Tactic: have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
-- 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 α
x : ℚ
this : (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2
⊢ round.{u_1} (α := α) (↑x : α) = round x
have rw : ⌊(↑x : α) + 1 / 2⌋ = round x
Tactic: rw [round_eq, round_eq, ← this, floor_cast]
-- 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 α
x : ℚ
this : (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2
rw : ⌊(↑x : α) + 1 / 2⌋ = round x
⊢ round.{u_1} (α := α) (↑x : α) = round x
have rw₁ : ⌊(↑x : α) + 1 / 2⌋ = ⌊x + 1 / 2⌋
Tactic: rw [round_eq, round_eq, ← this, floor_cast]
-- 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 α
x : ℚ
this : (↑(x + 1 / 2) : α) = (↑x : α) + 1 / 2
rw : ⌊(↑x : α) + 1 / 2⌋ = round x
rw₁ : ⌊(↑x : α) + 1 / 2⌋ = ⌊x + 1 / 2⌋
⊢ round.{u_1} (α := α) (↑x : α) = round x
have rw₂ : floor.{u_1} (α := α) (↑(x + 1 / 2) : α) = ⌊x + 1 / 2⌋
Tactic: rw [round_eq, round_eq, ← this, floor_cast]
-- 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 α
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⌋
⊢ round.{u_1} (α := α) (↑x : α) = round x
have rw₃ : ⌊x + 1 / 2⌋ = ⌊x + 1 / 2⌋
Tactic: rw [round_eq, round_eq, ← this, floor_cast]
-- 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 : α) _)⌋ (n / d)
have out : ⌊HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ = (↑(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 (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ = (↑(n / d) : ℤ)
have out : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
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 : α)⌋ = (↑(n / d) : ℤ)
have out : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
Tactic: rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, 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 (α := α) (↑n : α) (↑d : α)⌋ = HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
⊢ ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
have out₁ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
Tactic: rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, 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 (α := α) (↑n : α) (↑d : α)⌋ = HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑d : ℤ)
out₁ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
have out₂ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = floor.{u_1} (α := α) (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : α)
Tactic: rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, 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 (α := α) (↑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 : ℚ)) : α)
⊢ ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
have out₃ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑(↑n : ℚ) : α) (↑(↑d : ℚ) : α)⌋
Tactic: rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, 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 (α := α) (↑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 : ℚ) : α)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
have out₄ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑n : α) (↑(↑d : ℚ) : α)⌋
Tactic: rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, 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 (α := α) (↑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 : ℚ) : α)⌋
⊢ ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = (↑(n / d) : ℤ)
have out₅ : ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋ = ⌊HDiv.hDiv (α := α) (↑n : α) (↑d : α)⌋
Tactic: rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, 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 : α)
⊢ IsInt ⌊HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋
    (negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat)
have out : ⌊HMul.hMul (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ =
  (↑(negOfNat (-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 (α := α) (↑(negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)⌋ =
    (↑(negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat) : ℤ)
have out : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat
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 (-HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)).toNat
have out : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
Tactic: rw [← ceil_intCast_div_natCast n d, Int.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 : α)
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -ofNat ⌈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]
-- 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
⊢ ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = negOfNat ⌈HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌉.toNat
have out₁ : ⌊HDiv.hDiv (α := α) (↑(negOfNat n) : α) (↑d : α)⌋ = -(↑⌈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]
-- 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 : ℤ)
⊢ ⌊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 : ℚ)⌉
⊢ ⌊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]