awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : floor.{u_2} (α := R) (↑0 : R) = 0
⊢ floor.{u_2} (α := R) 0 = 0
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [← cast_zero, floor_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
⊢ floor.{u_2} (α := R) 1 = 1
have rw : floor.{u_2} (α := R) (↑1 : R) = 1
Tactic: rw [← cast_one, floor_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : floor.{u_2} (α := R) (↑1 : R) = 1
⊢ floor.{u_2} (α := R) 1 = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [← cast_one, floor_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a_1 : R
z a : ℤ
⊢ a ≤ ⌊a_1 + (↑z : R)⌋ ↔ a ≤ ⌊a_1⌋ + z
have rw : (↑a : R) ≤ a_1 + (↑z : R) ↔ a ≤ ⌊a_1⌋ + z
Tactic: rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a_1 : R
z a : ℤ
rw : (↑a : R) ≤ a_1 + (↑z : R) ↔ a ≤ ⌊a_1⌋ + z
⊢ a ≤ ⌊a_1 + (↑z : R)⌋ ↔ a ≤ ⌊a_1⌋ + z
have rw₁ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a ≤ ⌊a_1⌋ + z
Tactic: rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a_1 : R
z a : ℤ
rw : (↑a : R) ≤ a_1 + (↑z : R) ↔ a ≤ ⌊a_1⌋ + z
rw₁ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a ≤ ⌊a_1⌋ + z
⊢ a ≤ ⌊a_1 + (↑z : R)⌋ ↔ a ≤ ⌊a_1⌋ + z
have rw₂ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a - z ≤ ⌊a_1⌋
Tactic: rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a_1 : R
z a : ℤ
rw : (↑a : R) ≤ a_1 + (↑z : R) ↔ a ≤ ⌊a_1⌋ + z
rw₁ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a ≤ ⌊a_1⌋ + z
rw₂ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a - z ≤ ⌊a_1⌋
⊢ a ≤ ⌊a_1 + (↑z : R)⌋ ↔ a ≤ ⌊a_1⌋ + z
have rw₃ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ (↑(a - z) : R) ≤ a_1
Tactic: rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a_1 : R
z a : ℤ
rw : (↑a : R) ≤ a_1 + (↑z : R) ↔ a ≤ ⌊a_1⌋ + z
rw₁ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a ≤ ⌊a_1⌋ + z
rw₂ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ a - z ≤ ⌊a_1⌋
rw₃ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ (↑(a - z) : R) ≤ a_1
⊢ a ≤ ⌊a_1 + (↑z : R)⌋ ↔ a ≤ ⌊a_1⌋ + z
have rw₄ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1
Tactic: rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1
have rw : ⌊a + (↑1 : R)⌋ = ⌊a⌋ + 1
Tactic: rw [← cast_one, floor_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
rw : ⌊a + (↑1 : R)⌋ = ⌊a⌋ + 1
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1
have rw₁ : ⌊a⌋ + 1 = ⌊a⌋ + 1
Tactic: rw [← cast_one, floor_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
have rw : HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) ≤ a + b
Tactic: rw [le_floor, Int.cast_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) ≤ a + b
have h₁ : (↑⌊a⌋ : R) ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h₁ : (↑⌊a⌋ : R) ≤ a
⊢ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) ≤ a + b
have h₂ : (↑⌊b⌋ : R) ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
have rw : HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ (↑⌊b⌋ : R)
Tactic: rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ (↑⌊b⌋ : R)
have refine : HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ b - 1
Tactic: refine le_trans ?_ (sub_one_lt_floor _).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ b - 1
have rw : (↑⌊a + b⌋ : R) ≤ a + b
Tactic: rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a + (↑n : R)⌋ = ⌊a⌋ + (↑n : ℤ)
have rw : ⌊a + (↑(↑n : ℤ) : R)⌋ = ⌊a⌋ + (↑n : ℤ)
Tactic: rw [← Int.cast_natCast, floor_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
rw : ⌊a + (↑(↑n : ℤ) : R)⌋ = ⌊a⌋ + (↑n : ℤ)
⊢ ⌊a + (↑n : R)⌋ = ⌊a⌋ + (↑n : ℤ)
have rw₁ : ⌊a⌋ + (↑n : ℤ) = ⌊a⌋ + (↑n : ℤ)
Tactic: rw [← Int.cast_natCast, floor_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : R
⊢ ⌊(↑n : R) + a⌋ = (↑n : ℤ) + ⌊a⌋
have rw : ⌊(↑(↑n : ℤ) : R) + a⌋ = (↑n : ℤ) + ⌊a⌋
Tactic: rw [← Int.cast_natCast, floor_intCast_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : R
rw : ⌊(↑(↑n : ℤ) : R) + a⌋ = (↑n : ℤ) + ⌊a⌋
⊢ ⌊(↑n : R) + a⌋ = (↑n : ℤ) + ⌊a⌋
have rw₁ : (↑n : ℤ) + ⌊a⌋ = (↑n : ℤ) + ⌊a⌋
Tactic: rw [← Int.cast_natCast, floor_intCast_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊a - (↑z : R)⌋ = ⌊a + (↑(-z) : R)⌋
have rw : ⌊a - (↑z : R)⌋ = ⌊a + -(↑z : R)⌋
Tactic: rw [Int.cast_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : ⌊a - (↑z : R)⌋ = ⌊a + -(↑z : R)⌋
⊢ ⌊a - (↑z : R)⌋ = ⌊a + (↑(-z) : R)⌋
have rw₁ : ⌊a + -(↑z : R)⌋ = ⌊a + -(↑z : R)⌋
Tactic: rw [Int.cast_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a - (↑n : R)⌋ = ⌊a⌋ - (↑n : ℤ)
have rw : ⌊a - (↑(↑n : ℤ) : R)⌋ = ⌊a⌋ - (↑n : ℤ)
Tactic: rw [← Int.cast_natCast, floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
rw : ⌊a - (↑(↑n : ℤ) : R)⌋ = ⌊a⌋ - (↑n : ℤ)
⊢ ⌊a - (↑n : R)⌋ = ⌊a⌋ - (↑n : ℤ)
have rw₁ : ⌊a⌋ - (↑n : ℤ) = ⌊a⌋ - (↑n : ℤ)
Tactic: rw [← Int.cast_natCast, floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
⊢ |a - b| < 1
have inr : ∀ (this : ∀ {a b : R} (h : ⌊a⌋ = ⌊b⌋) (h0 : b ≤ a), |a - b| < 1) (h0 : ¬b ≤ a), |a - b| < 1
Tactic: wlog h0 : b ≤ a generalizing a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
inr : ∀ (this : ∀ {a b : R} (h : ⌊a⌋ = ⌊b⌋) (h0 : b ≤ a), |a - b| < 1) (h0 : ¬b ≤ a), |a - b| < 1
⊢ |a - b| < 1
have wlog : ∀ {a b : R} (h : ⌊a⌋ = ⌊b⌋) (h0 : b ≤ a), |a - b| < 1
Tactic: wlog h0 : b ≤ a generalizing a b
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R} (h : ⌊a⌋ = ⌊b⌋) (h0 : b ≤ a), |a - b| < 1
h0 : ¬b ≤ a
⊢ |a - b| < 1
have inr : |b - a| < 1
Tactic: rw [abs_sub_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - (↑⌊b⌋ : R) = 1
have rw : HAdd.hAdd (α := R) (↑⌊b⌋ : R) 1 - (↑⌊b⌋ : R) = 1
Tactic: rw [h, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
rw : HAdd.hAdd (α := R) (↑⌊b⌋ : R) 1 - (↑⌊b⌋ : R) = 1
⊢ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - (↑⌊b⌋ : R) = 1
have rw₁ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [h, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ |a - b| < 1
have calc : HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - (↑⌊b⌋ : R) = 1
Tactic: calc |a - b|
    _ = a - b := abs_of_nonneg (sub_nonneg_of_le h0)
    _ < ⌊a⌋ + 1 - b := sub_lt_sub_right (lt_floor_add_one a) _
    _ ≤ ⌊a⌋ + 1 - ⌊b⌋ := sub_le_sub_left (floor_le b) _
    _ = 1 := by rw [h, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊a * (↑n : R)⌋ / n = ⌊a⌋
have refine : ∀ (m : ℤ), m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
Tactic: refine eq_of_forall_le_iff fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
⊢ m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
have rw : m * n ≤ ⌊a * (↑n : R)⌋ ↔ m ≤ ⌊a⌋
Tactic: rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
rw : m * n ≤ ⌊a * (↑n : R)⌋ ↔ m ≤ ⌊a⌋
⊢ m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
have rw₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋
Tactic: rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
rw : m * n ≤ ⌊a * (↑n : R)⌋ ↔ m ≤ ⌊a⌋
rw₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋
⊢ m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
have rw₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
Tactic: rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
rw : m * n ≤ ⌊a * (↑n : R)⌋ ↔ m ≤ ⌊a⌋
rw₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋
rw₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
⊢ m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
have rw₃ : HMul.hMul (α := R) (↑m : R) (↑n : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
Tactic: rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
rw : m * n ≤ ⌊a * (↑n : R)⌋ ↔ m ≤ ⌊a⌋
rw₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋
rw₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
rw₃ : HMul.hMul (α := R) (↑m : R) (↑n : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
⊢ m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
have rw₄ : (↑m : R) ≤ a ↔ (↑m : R) ≤ a
Tactic: rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
x k : R
hk : 1 < k
⊢ k * fract x = 1 ↔ ∃ (n : ℤ), k * x = k * (↑n : R) + 1
have rw : k * x = k * (↑⌊x⌋ : R) + 1 ↔ ∃ (n : ℤ), k * x = k * (↑n : R) + 1
Tactic: rw [fract, mul_sub, sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
x k : R
hk : 1 < k
⊢ k * x = k * (↑⌊x⌋ : R) + 1 ↔ ∃ (n : ℤ), k * x = k * (↑n : R) + 1
have refine : (∃ (n : ℤ), k * x = k * (↑n : R) + 1) → k * x = k * (↑⌊x⌋ : R) + 1
Tactic: refine ⟨fun hx ↦ ⟨⌊x⌋, hx⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * (↑n : R) + 1
⊢ k * x = k * (↑⌊x⌋ : R) + 1
have h : ⌊x⌋ = n
Tactic: convert! hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * (↑n : R) + 1
⊢ ⌊x⌋ = n
have hk0 : 0 < k
Tactic: have hk0 : 0 < (k : R) := zero_le_one.trans_lt hk
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * (↑n : R) + 1
hk0 : 0 < k
⊢ ⌊x⌋ = n
have h : k * (↑n : R) ≤ k * (↑n : R) + 1 ∧ k * (↑n : R) + 1 < k * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [floor_eq_iff, ← mul_le_mul_iff_right₀ hk0, ← mul_lt_mul_iff_right₀ hk0, hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊(↑n : R) * a⌋ / n = ⌊a⌋
have rw : ⌊a * (↑n : R)⌋ / n = ⌊a⌋
Tactic: rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℤ
hn : 0 < n
a : R
rw : ⌊a * (↑n : R)⌋ / n = ⌊a⌋
⊢ ⌊(↑n : R) * a⌋ / n = ⌊a⌋
have rw₁ : ⌊a⌋ = ⌊a⌋
Tactic: rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊(↑n : R) * a⌋ / (↑n : ℤ) = ⌊a⌋
have rw : ⌊a * (↑n : R)⌋ / (↑n : ℤ) = ⌊a⌋
Tactic: rw [Nat.cast_comm, mul_natCast_floor_div_cancel hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
rw : ⌊a * (↑n : R)⌋ / (↑n : ℤ) = ⌊a⌋
⊢ ⌊(↑n : R) * a⌋ / (↑n : ℤ) = ⌊a⌋
have rw₁ : ⌊a⌋ = ⌊a⌋
Tactic: rw [Nat.cast_comm, mul_natCast_floor_div_cancel hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℤ
hn : 0 ≤ n
a : k
⊢ ⌊a / (↑n : k)⌋ = ⌊a⌋ / n
have inl : ∀ (hn : LE.le (α := ℤ) 0 0), ⌊a / (↑0 : k)⌋ = ⌊a⌋ / 0
Tactic: obtain rfl | hn := hn.eq_or_lt
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℤ
hn : 0 ≤ n
a : k
inl : ∀ (hn : LE.le (α := ℤ) 0 0), ⌊a / (↑0 : k)⌋ = ⌊a⌋ / 0
⊢ ⌊a / (↑n : k)⌋ = ⌊a⌋ / n
have inr : ∀ (hn : 0 < n), ⌊a / (↑n : k)⌋ = ⌊a⌋ / n
Tactic: obtain rfl | hn := hn.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℤ
hn_1 : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / (↑n : k)⌋ = ⌊a⌋ / n
have inr : ⌊a / (↑n : k)⌋ = ⌊a / (↑n : k) * (↑n : k)⌋ / n
Tactic: nth_rw 2 [← div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℤ
hn_1 : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / (↑n : k)⌋ = ⌊a / (↑n : k) * (↑n : k)⌋ / n
have inr : ⌊a / (↑n : k)⌋ = ⌊a / (↑n : k)⌋
Tactic: rw [mul_cast_floor_div_cancel_of_pos hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a b : R
⊢ fract (a + b) - fract a - fract b = (↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋) : R)
have unfold : a + b - (↑⌊a + b⌋ : R) - (a - (↑⌊a⌋ : R)) - (b - (↑⌊b⌋ : R)) = (↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋) : R)
Tactic: unfold fract
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℤ
⊢ fract (a + (↑m : R)) = fract a
have rw : a + (↑m : R) - (↑⌊a + (↑m : R)⌋ : R) = fract a
Tactic: rw [fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℕ
⊢ fract (a + (↑m : R)) = fract a
have rw : a + (↑m : R) - (↑⌊a + (↑m : R)⌋ : R) = fract a
Tactic: rw [fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
m : ℤ
a : R
⊢ fract ((↑m : R) + a) = fract a
have rw : fract (a + (↑m : R)) = fract a
Tactic: rw [add_comm, fract_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
m : ℤ
a : R
rw : fract (a + (↑m : R)) = fract a
⊢ fract ((↑m : R) + a) = fract a
have rw₁ : fract a = fract a
Tactic: rw [add_comm, fract_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : R
⊢ fract ((↑n : R) + a) = fract a
have rw : fract (a + (↑n : R)) = fract a
Tactic: rw [add_comm, fract_add_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : R
rw : fract (a + (↑n : R)) = fract a
⊢ fract ((↑n : R) + a) = fract a
have rw₁ : fract a = fract a
Tactic: rw [add_comm, fract_add_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℤ
⊢ fract (a - (↑m : R)) = fract a
have rw : a - (↑m : R) - (↑⌊a - (↑m : R)⌋ : R) = fract a
Tactic: rw [fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
⊢ fract (a - (↑n : R)) = fract a
have rw : a - (↑n : R) - (↑⌊a - (↑n : R)⌋ : R) = fract a
Tactic: rw [fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ fract (a + b) ≤ fract a + fract b
have rw : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
Tactic: rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ fract a + fract b ≤ fract (a + b) + 1
have rw : HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
Tactic: rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
⊢ Eq.{u_2 + 1} (α := R) (fract 0) 0
have rw : HSub.hSub (α := R) 0 (↑(floor.{u_2} (α := R) 0) : R) = 0
Tactic: rw [fract, floor_zero, cast_zero, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : HSub.hSub (α := R) 0 (↑(floor.{u_2} (α := R) 0) : R) = 0
⊢ Eq.{u_2 + 1} (α := R) (fract 0) 0
have rw₁ : HSub.hSub (α := R) 0 (↑0 : R) = 0
Tactic: rw [fract, floor_zero, cast_zero, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : HSub.hSub (α := R) 0 (↑(floor.{u_2} (α := R) 0) : R) = 0
rw₁ : HSub.hSub (α := R) 0 (↑0 : R) = 0
⊢ Eq.{u_2 + 1} (α := R) (fract 0) 0
have rw₂ : HSub.hSub (α := R) 0 0 = 0
Tactic: rw [fract, floor_zero, cast_zero, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : HSub.hSub (α := R) 0 (↑(floor.{u_2} (α := R) 0) : R) = 0
rw₁ : HSub.hSub (α := R) 0 (↑0 : R) = 0
rw₂ : HSub.hSub (α := R) 0 0 = 0
⊢ Eq.{u_2 + 1} (α := R) (fract 0) 0
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [fract, floor_zero, cast_zero, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
⊢ Eq.{u_2 + 1} (α := R) (fract (↑z : R)) 0
have unfold : HSub.hSub (α := R) (↑z : R) (↑(floor.{u_2} (α := R) (↑z : R)) : R) = 0
Tactic: unfold fract
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
⊢ HSub.hSub (α := R) (↑z : R) (↑(floor.{u_2} (α := R) (↑z : R)) : R) = 0
have rw : HSub.hSub (α := R) (↑z : R) (↑z : R) = 0
Tactic: rw [floor_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌊fract a⌋ = 0
have rw : 0 ≤ fract a ∧ fract a < 1
Tactic: rw [floor_eq_iff, Int.cast_zero, zero_add]