awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌊a - OfNat.ofNat n⌋ = ⌊a⌋ - OfNat.ofNat n

Tactic:
floor_sub_natCast a n

Premises used: Int.floor_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
wlog : ∀ {a b : R} (h : ⌊a⌋ = ⌊b⌋) (h0 : b ≤ a), |a - b| < 1
⊢ |a - b| < 1

Tactic:
wlog h0 : b ≤ a generalizing a b
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
inr : |b - a| < 1
⊢ |a - b| < 1

Tactic:
rw [abs_sub_comm]

Premises used: abs_sub_comm
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
⊢ |b - a| < 1

Tactic:
this h.symm (le_of_not_ge h0)

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
⊢ |b - a| < 1

Tactic:
exact this h.symm (le_of_not_ge h0)

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Algebra.Order.Floor.Ring
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| = a - b

Tactic:
abs_of_nonneg (sub_nonneg_of_le h0)

Premises used: sub_nonneg_of_le, abs_of_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 < HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - b

Tactic:
sub_lt_sub_right (lt_floor_add_one a) _

Premises used: Int.lt_floor_add_one, sub_lt_sub_right
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - (↑⌊b⌋ : R)

Tactic:
sub_le_sub_left (floor_le b) _

Premises used: sub_le_sub_left, Int.floor_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 1 1
⊢ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - (↑⌊b⌋ : R) = 1

Tactic:
rw [h, add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
calc : HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1 - (↑⌊b⌋ : R) = 1
⊢ |a - b| < 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]

Premises used: sub_nonneg_of_le, Int.lt_floor_add_one, abs_of_nonneg, sub_le_sub_left, Int.floor_le, sub_lt_sub_right
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ (↑⌊a⌋ : R) = a ↔ Membership.mem (γ := Set R) (range Int.cast) a

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ (↑⌊a⌋ : R) < a ↔ a ∉ range Int.cast

Tactic:
(floor_le a).lt_iff_ne.trans <| (floor_eq_self_iff_mem _).not

Premises used: Iff.not, Int.floor_eq_self_iff_mem, LE.le.lt_iff_ne, Iff.trans, Int.floor_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
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⌋

Tactic:
eq_of_forall_le_iff fun m ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
refine : ∀ (m : ℤ), m ≤ ⌊a * (↑n : R)⌋ / n ↔ m ≤ ⌊a⌋
⊢ ⌊a * (↑n : R)⌋ / n = ⌊a⌋

Tactic:
refine eq_of_forall_le_iff fun m ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
rw₄ rw₅ : (↑m : R) ≤ a ↔ (↑m : R) ≤ a
⊢ m ≤ ⌊a * (↑n : R)⌋ / n ↔ 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)]

Premises used: Iff.mpr, mul_le_mul_iff_of_pos_right, Int.le_ediv_iff_mul_le, Int.cast_mul, Int.le_floor, Int.cast_pos
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
⊢ LT.lt (α := ℤ) 0 (↑n : ℤ)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
⊢ ⌊a * (↑n : R)⌋ / (↑n : ℤ) = ⌊a⌋

Tactic:
simpa using mul_cast_floor_div_cancel_of_pos (n := n) (by positivity) a

Premises used: Int.mul_cast_floor_div_cancel_of_pos
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
rw : k * x = k * (↑⌊x⌋ : R) + 1 ↔ ∃ (n : ℤ), k * x = k * (↑n : R) + 1
⊢ k * fract x = 1 ↔ ∃ (n : ℤ), k * x = k * (↑n : R) + 1

Tactic:
rw [fract, mul_sub, sub_eq_iff_eq_add']

Premises used: mul_sub, Int.fract, sub_eq_iff_eq_add'
-- Module: Mathlib.Algebra.Order.Floor.Ring
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

Tactic:
⟨fun hx ↦ ⟨⌊x⌋, hx⟩, ?_⟩

Premises used: Int.floor, Iff.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
refine : (∃ (n : ℤ), k * x = k * (↑n : R) + 1) → k * x = k * (↑⌊x⌋ : R) + 1
⊢ k * x = k * (↑⌊x⌋ : R) + 1 ↔ ∃ (n : ℤ), k * x = k * (↑n : R) + 1

Tactic:
refine ⟨fun hx ↦ ⟨⌊x⌋, hx⟩, ?_⟩
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 * (↑n : R) + 1

Tactic:
hn
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
h : ⌊x⌋ = n
⊢ k * x = k * (↑⌊x⌋ : R) + 1

Tactic:
convert! hn
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
⊢ 0 < k

Tactic:
have hk0 : 0 < (k : R) := zero_le_one.trans_lt hk
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
h : k * (↑n : R) ≤ k * (↑n : R) + 1 ∧ k * (↑n : R) + 1 < k * HAdd.hAdd (α := R) (↑n : R) 1
⊢ ⌊x⌋ = n

Tactic:
rw [floor_eq_iff, ← mul_le_mul_iff_right₀ hk0, ← mul_lt_mul_iff_right₀ hk0, hn]

Premises used: Int.floor_eq_iff, mul_lt_mul_iff_right₀, mul_le_mul_iff_right₀
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
⊢ k * (↑n : R) ≤ k * (↑n : R) + 1 ∧ k * (↑n : R) + 1 < k * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simp [mul_add, hk]

Premises used: mul_add
-- Module: Mathlib.Algebra.Order.Floor.Ring
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⌋
rw₁ rw₂ : ⌊a⌋ = ⌊a⌋
⊢ ⌊(↑n : R) * a⌋ / n = ⌊a⌋

Tactic:
rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]

Premises used: Int.mul_cast_floor_div_cancel_of_pos, Commute.intCast_left
-- Module: Mathlib.Algebra.Order.Floor.Ring
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⌋
rw₁ rw₂ : ⌊a⌋ = ⌊a⌋
⊢ ⌊(↑n : R) * a⌋ / (↑n : ℤ) = ⌊a⌋

Tactic:
rw [Nat.cast_comm, mul_natCast_floor_div_cancel hn]

Premises used: Nat.cast_comm, Int.mul_natCast_floor_div_cancel
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
inr : ∀ (hn : 0 < n), ⌊a / (↑n : k)⌋ = ⌊a⌋ / n
⊢ ⌊a / (↑n : k)⌋ = ⌊a⌋ / n

Tactic:
obtain rfl | hn := hn.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
a : k
hn : LE.le (α := ℤ) 0 0
⊢ ⌊a / (↑0 : k)⌋ = ⌊a⌋ / 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
inr : ⌊a / (↑n : k)⌋ = ⌊a / (↑n : k) * (↑n : k)⌋ / n
⊢ ⌊a / (↑n : k)⌋ = ⌊a⌋ / n

Tactic:
nth_rw 2 [← div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))]

Premises used: Iff.mpr, div_mul_cancel₀, ne_of_gt, Int.cast_pos
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
inr inr₁ : ⌊a / (↑n : k)⌋ = ⌊a / (↑n : k)⌋
⊢ ⌊a / (↑n : k)⌋ = ⌊a / (↑n : k) * (↑n : k)⌋ / n

Tactic:
rw [mul_cast_floor_div_cancel_of_pos hn]

Premises used: Int.mul_cast_floor_div_cancel_of_pos
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
a : k
n : ℕ
⊢ ⌊a / (↑n : k)⌋ = ⌊a⌋ / (↑n : ℤ)

Tactic:
simpa using floor_div_cast_of_nonneg n.cast_nonneg a

Premises used: Nat.cast_nonneg, Int.floor_div_cast_of_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ a - (↑⌊a⌋ : R) = fract a

Tactic:
rfl

Premises used: Int.fract, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ (↑⌊a⌋ : R) + fract a = a

Tactic:
add_sub_cancel _ _

Premises used: Int.fract, add_sub_cancel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ fract a + (↑⌊a⌋ : R) = a

Tactic:
sub_add_cancel _ _

Premises used: Int.fract, sub_add_cancel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ a - fract a = (↑⌊a⌋ : R)

Tactic:
sub_sub_cancel _ _

Premises used: Int.fract, sub_sub_cancel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ fract a - a = -(↑⌊a⌋ : R)

Tactic:
sub_sub_cancel_left _ _

Premises used: Int.fract, sub_sub_cancel_left
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a b : R
unfold : a + b - (↑⌊a + b⌋ : R) - (a - (↑⌊a⌋ : R)) - (b - (↑⌊b⌋ : R)) = (↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋) : R)
⊢ fract (a + b) - fract a - fract b = (↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋) : R)

Tactic:
unfold fract

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a b : R
⊢ a + b - (↑⌊a + b⌋ : R) - (a - (↑⌊a⌋ : R)) - (b - (↑⌊b⌋ : R)) = (↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋) : R)

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℤ
rw : a + (↑m : R) - (↑⌊a + (↑m : R)⌋ : R) = fract a
⊢ fract (a + (↑m : R)) = fract a

Tactic:
rw [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℤ
⊢ a + (↑m : R) - (↑⌊a + (↑m : R)⌋ : R) = fract a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℕ
rw : a + (↑m : R) - (↑⌊a + (↑m : R)⌋ : R) = fract a
⊢ fract (a + (↑m : R)) = fract a

Tactic:
rw [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℕ
⊢ a + (↑m : R) - (↑⌊a + (↑m : R)⌋ : R) = fract a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ fract (a + 1) = fract a

Tactic:
mod_cast fract_add_natCast a 1

Premises used: congrArg, Int.fract, cast, Int.fract_add_natCast, HAdd.hAdd, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ fract (a + OfNat.ofNat n) = fract a

Tactic:
fract_add_natCast a n

Premises used: Int.fract_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
rw₁ rw₂ : fract a = fract a
⊢ fract ((↑m : R) + a) = fract a

Tactic:
rw [add_comm, fract_add_intCast]

Premises used: add_comm, Int.fract_add_intCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
rw₁ rw₂ : fract a = fract a
⊢ fract ((↑n : R) + a) = fract a

Tactic:
rw [add_comm, fract_add_natCast]

Premises used: Int.fract_add_natCast, add_comm
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ fract (1 + a) = fract a

Tactic:
mod_cast fract_natCast_add 1 a

Premises used: congrArg, Int.fract, cast, Int.fract_natCast_add, HAdd.hAdd, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
inst_4 : n.AtLeastTwo
a : R
⊢ fract (OfNat.ofNat n + a) = fract a

Tactic:
fract_natCast_add n a

Premises used: Int.fract_natCast_add
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℤ
rw : a - (↑m : R) - (↑⌊a - (↑m : R)⌋ : R) = fract a
⊢ fract (a - (↑m : R)) = fract a

Tactic:
rw [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
m : ℤ
⊢ a - (↑m : R) - (↑⌊a - (↑m : R)⌋ : R) = fract a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 : R)⌋ : R) = fract a
⊢ fract (a - (↑n : R)) = fract a

Tactic:
rw [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 : R)⌋ : R) = fract a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ fract (a - 1) = fract a

Tactic:
mod_cast fract_sub_natCast a 1

Premises used: congrArg, Int.fract, HSub.hSub, cast, Int.fract_sub_natCast, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ fract (a - OfNat.ofNat n) = fract a

Tactic:
fract_sub_natCast a n

Premises used: Int.fract_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
rw : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
⊢ fract (a + b) ≤ fract a + fract b

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]

Premises used: Int.cast_le, Int.fract, Int.cast_add, sub_le_sub_iff_left, sub_add_sub_comm
-- Module: Mathlib.Algebra.Order.Floor.Ring
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⌋

Tactic:
le_floor_add _ _

Premises used: Int.le_floor_add
-- Module: Mathlib.Algebra.Order.Floor.Ring
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⌋

Tactic:
exact le_floor_add _ _

Premises used: Int.le_floor_add
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
rw : HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
⊢ fract a + fract b ≤ fract (a + b) + 1

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]

Premises used: sub_add, Int.fract, sub_le_sub_iff_left, sub_add_sub_comm
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)

Tactic:
mod_cast le_floor_add_floor a b

Premises used: Int.cast, Int.floor, congrArg, HSub.hSub, cast, LE.le, Int.cast_le._simp_1, Nat.cast, HAdd.hAdd, congr, Int.le_floor_add_floor, Int.cast_add._simp_1, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Int.cast_one, Eq.trans, Int.cast_sub._simp_1
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)

Tactic:
exact mod_cast le_floor_add_floor a b

Premises used: Int.le_floor_add_floor
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ 0 ≤ fract a

Tactic:
sub_nonneg.2 <| floor_le _

Premises used: Iff.mpr, Int.fract, Int.floor_le, sub_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
⊢ 0 < fract a ↔ a ≠ (↑⌊a⌋ : R)

Tactic:
(fract_nonneg a).lt_iff_ne.trans <| ne_comm.trans sub_ne_zero

Premises used: sub_ne_zero, LE.le.lt_iff_ne, Iff.trans, ne_comm, Int.fract_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ fract a < 1

Tactic:
sub_lt_comm.1 <| sub_one_lt_floor _

Premises used: sub_lt_comm, Int.fract, Int.sub_one_lt_floor, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Ring
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) (fract 0) 0

Tactic:
rw [fract, floor_zero, cast_zero, sub_self]

Premises used: sub_self, Int.cast_zero, Int.fract, Int.floor_zero
-- Module: Mathlib.Algebra.Order.Floor.Ring
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 1) 0

Tactic:
simp [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
⊢ |fract a| = fract a

Tactic:
abs_eq_self.mpr <| fract_nonneg a

Premises used: Iff.mpr, Int.fract_nonneg, abs_eq_self
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
⊢ |1 - fract a| = 1 - fract a

Tactic:
abs_eq_self.mpr <| sub_nonneg.mpr (fract_lt_one a).le

Premises used: Iff.mpr, LT.lt.le, Int.fract_lt_one, sub_nonneg, abs_eq_self
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
unfold : HSub.hSub (α := R) (↑z : R) (↑(floor.{u_2} (α := R) (↑z : R)) : R) = 0
⊢ Eq.{u_2 + 1} (α := R) (fract (↑z : R)) 0

Tactic:
unfold fract

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
rw : HSub.hSub (α := R) (↑z : R) (↑z : R) = 0
⊢ HSub.hSub (α := R) (↑z : R) (↑(floor.{u_2} (α := R) (↑z : R)) : R) = 0

Tactic:
rw [floor_intCast]

Premises used: Int.floor_intCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
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) (↑z : R) = 0

Tactic:
sub_self _

Premises used: sub_self
-- Module: Mathlib.Algebra.Order.Floor.Ring
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) (↑z : R) = 0

Tactic:
exact sub_self _

Premises used: sub_self
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (fract (↑n : R)) 0

Tactic:
simp [fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ Eq.{u_2 + 1} (α := R) (fract (OfNat.ofNat n)) 0

Tactic:
fract_natCast n

Premises used: Int.fract_natCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ Eq.{u_2 + 1} (α := R) (fract (↑⌊a⌋ : R)) 0

Tactic:
fract_intCast _

Premises used: Int.fract_intCast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
rw : 0 ≤ fract a ∧ fract a < 1
⊢ ⌊fract a⌋ = 0

Tactic:
rw [floor_eq_iff, Int.cast_zero, zero_add]

Premises used: Int.cast_zero, zero_add, Int.floor_eq_iff