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
⊢ 0 ≤ fract a ∧ fract a < 1

Tactic:
⟨fract_nonneg _, fract_lt_one _⟩

Premises used: And.intro, Int.fract_lt_one, 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
⊢ 0 ≤ fract a ∧ fract a < 1

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _⟩
-- 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 : fract a = b
rw : 0 ≤ fract a ∧ fract a < 1 ∧ ∃ (z : ℤ), a - fract a = (↑z : R)
⊢ 0 ≤ b ∧ b < 1 ∧ ∃ (z : ℤ), a - b = (↑z : R)

Tactic:
rw [← h]
-- 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 : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ (z : ℤ), a - fract a = (↑z : R)

Tactic:
⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩

Premises used: Int.floor, sub_sub_cancel, And.intro, Int.fract_lt_one, Exists.intro, 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 b : R
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ (z : ℤ), a - fract a = (↑z : R)

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, 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
inst_3 : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
rw : Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑z : R)
⊢ fract a = b

Tactic:
rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz]

Premises used: eq_sub_iff_add_eq, eq_comm, add_comm, Int.self_sub_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 b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑z : R)

Tactic:
congrArg Int.cast ?_

Premises used: Int.cast, congrArg
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
refine : ⌊a⌋ = z
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑z : R)

Tactic:
refine congrArg Int.cast ?_

Premises used: Int.cast, congrArg
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
rw : a - b ≤ a ∧ a < a - b + 1
⊢ ⌊a⌋ = z

Tactic:
rw [floor_eq_iff, ← hz]

Premises used: Int.floor_eq_iff
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
left : a - b ≤ a
right : a < a - b + 1
⊢ a - b ≤ a ∧ a < a - b + 1

Tactic:
constructor
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ a - b ≤ a

Tactic:
simpa [sub_eq_add_neg, add_assoc]

Premises used: add_assoc, sub_eq_add_neg
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ a < a - b + 1

Tactic:
simpa [sub_eq_add_neg, add_assoc]

Premises used: add_assoc, sub_eq_add_neg
-- 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 - (↑⌊a⌋ : R) = b - (↑⌊b⌋ : R)
rw : a - b = HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
rw₁ rw₂ : HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) = HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
⊢ a - b = (↑(⌊a⌋ - ⌊b⌋) : R)

Tactic:
rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]

Premises used: sub_eq_sub_iff_sub_eq_sub, Int.cast_sub, 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
a b : R
z : ℤ
hz : a - b = (↑z : R)
⊢ fract a = fract b

Tactic:
fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩

Premises used: Iff.mpr, Int.floor, HAdd.hAdd, And.intro, Int.fract_lt_one, Exists.intro, Int.fract_nonneg, Int.fract_eq_iff
-- 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
z : ℤ
hz : a - b = (↑z : R)
refine : a - fract b = (↑(z + ⌊b⌋) : R)
⊢ fract a = fract b

Tactic:
refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩

Premises used: Iff.mpr, Int.floor, HAdd.hAdd, And.intro, Int.fract_lt_one, Exists.intro, Int.fract_nonneg, Int.fract_eq_iff
-- 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
z : ℤ
hz : a - b = (↑z : R)
rw : b + (↑z : R) - fract b = HAdd.hAdd (α := R) (↑z : R) (↑⌊b⌋ : R)
⊢ a - fract b = (↑(z + ⌊b⌋) : R)

Tactic:
rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]

Premises used: Int.cast_add, add_comm, eq_add_of_sub_eq
-- 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
z : ℤ
hz : a - b = (↑z : R)
⊢ b + (↑z : R) - fract b = HAdd.hAdd (α := R) (↑z : R) (↑⌊b⌋ : R)

Tactic:
add_sub_sub_cancel _ _ _

Premises used: Int.fract, add_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
inst_3 : IsOrderedRing R
a b : R
z : ℤ
hz : a - b = (↑z : R)
⊢ b + (↑z : R) - fract b = HAdd.hAdd (α := R) (↑z : R) (↑⌊b⌋ : R)

Tactic:
exact add_sub_sub_cancel _ _ _

Premises used: add_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
inst_3 : IsOrderedRing R
a : R
⊢ a - a = (↑0 : R)

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 (fract a) = fract a

Tactic:
fract_eq_self.2 ⟨fract_nonneg _, fract_lt_one _⟩

Premises used: Iff.mpr, And.intro, Int.fract_eq_self, Int.fract_lt_one, 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 = 0 ↔ Membership.mem (γ := Set R) (range Int.cast) a

Tactic:
simp [fract_eq_iff, eq_comm]

Premises used: eq_comm, Int.fract_eq_iff
-- 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 ≠ 0 ↔ a ∉ range Int.cast

Tactic:
fract_eq_zero_iff.not

Premises used: Iff.not, Int.fract_eq_zero_iff
-- 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
x : R
hx : fract x ≠ 0
rw : 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
⊢ fract (-x) = 1 - fract x

Tactic:
rw [fract_eq_iff]

Premises used: Int.fract_eq_iff
-- 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
x : R
hx : fract x ≠ 0
left : 0 ≤ 1 - fract x
right : 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)

Tactic:
constructor
-- 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
x : R
hx : fract x ≠ 0
left : fract x ≤ 1
⊢ 0 ≤ 1 - fract x

Tactic:
rw [le_sub_iff_add_le, zero_add]

Premises used: zero_add, le_sub_iff_add_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
x : R
hx : fract x ≠ 0
⊢ fract x ≤ 1

Tactic:
(fract_lt_one x).le

Premises used: LT.lt.le, Int.fract_lt_one
-- 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
x : R
hx : fract x ≠ 0
⊢ fract x ≤ 1

Tactic:
exact (fract_lt_one x).le

Premises used: LT.lt.le, Int.fract_lt_one
-- 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
x : R
hx : fract x ≠ 0
⊢ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)

Tactic:
⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 1, ?_⟩

Premises used: Int.floor, sub_lt_self, HSub.hSub, lt_of_le_of_ne', And.intro, Exists.intro, Int.fract_nonneg, OfNat.ofNat, Neg.neg
-- 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
x : R
hx : fract x ≠ 0
right : -x - (1 - fract x) = (↑(-⌊x⌋ - 1) : R)
⊢ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)

Tactic:
refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 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
x : R
hx : fract x ≠ 0
right : -x + fract x = -(↑⌊x⌋ : R)
⊢ -x - (1 - fract x) = (↑(-⌊x⌋ - 1) : R)

Tactic:
simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]

Premises used: Int.cast_neg, Int.cast_sub, sub_sub_eq_add_sub, sub_left_inj, Int.cast_one
-- 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
x : R
hx : fract x ≠ 0
rw : -((↑⌊x⌋ : R) + fract x)
| -x

Tactic:
rw [← floor_add_fract x]

Premises used: Int.floor_add_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
x : R
hx : fract x ≠ 0
right : -((↑⌊x⌋ : R) + fract x) + fract x = -(↑⌊x⌋ : R)
⊢ -x + fract x = -(↑⌊x⌋ : R)

Tactic:
conv in -x => rw [← floor_add_fract x]

Premises used: Int.floor_add_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
x : R
hx : fract x ≠ 0
⊢ -((↑⌊x⌋ : R) + fract x) + fract x = -(↑⌊x⌋ : R)

Tactic:
simp [-floor_add_fract]

Premises used: Int.floor_add_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
x : R
simp : (∃ (z : ℤ), -x = (↑z : R)) ↔ ∃ (z : ℤ), x = (↑z : R)
⊢ fract (-x) = 0 ↔ fract x = 0

Tactic:
simp only [fract_eq_iff, le_refl, zero_lt_one, tsub_zero, true_and]

Premises used: le_refl, tsub_zero, zero_lt_one, true_and, Int.fract_eq_iff
-- 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
x : R
mp : (∃ (z : ℤ), -x = (↑z : R)) → ∃ (z : ℤ), x = (↑z : R)
mpr : (∃ (z : ℤ), x = (↑z : R)) → ∃ (z : ℤ), -x = (↑z : R)
⊢ (∃ (z : ℤ), -x = (↑z : R)) ↔ ∃ (z : ℤ), x = (↑z : R)

Tactic:
constructor
-- 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
x : R
z : ℤ
hz : -x = (↑z : R)
h : x = (↑(-z) : R)
⊢ ∃ (z : ℤ), x = (↑z : R)

Tactic:
use -z
-- 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
x : R
z : ℤ
hz : x = (↑z : R)
h : -x = (↑(-z) : R)
⊢ ∃ (z : ℤ), -x = (↑z : R)

Tactic:
use -z
-- 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
x : R
z : ℤ
hz : -x = (↑z : R)
⊢ x = (↑(-z) : R)

Tactic:
simp [← hz]
-- 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
x : R
z : ℤ
hz : x = (↑z : R)
⊢ -x = (↑(-z) : R)

Tactic:
simp [← hz]
-- 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
h : fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑0 : R)
⊢ ∃ (z : ℤ), fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑z : R)

Tactic:
use 0
-- 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 * (↑0 : R) - fract (a * (↑0 : R)) = (↑0 : R)

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
c : ℕ
hc : ∃ (z : ℤ), fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
succ :
  ∀ (z : ℤ) (hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)),
    ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)

Tactic:
rcases hc with ⟨z, hz⟩
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
succ : ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)

Tactic:
rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]

Premises used: Nat.cast_add, mul_add, mul_one, Nat.cast_one
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
succ :
  ∀ (y : ℤ) (hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)),
    ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)

Tactic:
rcases fract_add (a * c) a with ⟨y, hy⟩

Premises used: HMul.hMul, Nat.cast, Int.fract_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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
y : ℤ
hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)
h : fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑(z - y) : R)
⊢ ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)

Tactic:
use z - y
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
y : ℤ
hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)
h :
  fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) =
    fract a * (↑c : R) - fract (a * (↑c : R)) - (fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a)
⊢ fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑(z - y) : R)

Tactic:
rw [Int.cast_sub, ← hz, ← hy]

Premises used: Int.cast_sub
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
y : ℤ
hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)
⊢ fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) =
    fract a * (↑c : R) - fract (a * (↑c : R)) - (fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a)

Tactic:
abel
-- 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
b : ℕ
zero : ∃ (z : ℤ), fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑z : R)
succ :
  ∀ (c : ℕ) (hc : ∃ (z : ℤ), fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)),
    ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑b : R) - fract (a * (↑b : R)) = (↑z : R)

Tactic:
induction b with
  | zero => use 0; simp
  | succ c hc =>
    rcases hc with ⟨z, hz⟩
    rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    rcases fract_add (a * c) a with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel

Premises used: Int.cast_sub, Nat.cast_add, Int.succ, mul_add, mul_one, Nat.cast_one
-- 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
s : Set R
h :
  ∀ (x : R), x ∈ fract ⁻¹' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1)) x
⊢ fract ⁻¹' s = ⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1)

Tactic:
ext x
-- 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
s : Set R
x : R
h : fract x ∈ s ↔ ∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))
⊢ x ∈ fract ⁻¹' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1)) x

Tactic:
simp only [mem_preimage, mem_iUnion, mem_inter_iff]

Premises used: Set.mem_inter_iff, Set.mem_iUnion, Set.mem_preimage
-- 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
s : Set R
x : R
⊢ fract x ∈ s ↔ ∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))

Tactic:
⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩

Premises used: Int.floor, And.intro, Iff.intro, Int.fract_lt_one, Exists.intro, 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
s : Set R
x : R
h : (∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))) → fract x ∈ s
⊢ fract x ∈ s ↔ ∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))

Tactic:
refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩
-- 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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
⊢ ⌊x⌋ = m

Tactic:
floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩

Premises used: Iff.mpr, sub_lt_iff_lt_add', Int.floor_eq_iff, And.intro, Iff.mp, sub_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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
⊢ x - (↑⌊x⌋ : R) ∈ s

Tactic:
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩

Premises used: Iff.mpr, sub_lt_iff_lt_add', Int.floor_eq_iff, And.intro, Iff.mp, sub_nonneg, rfl
-- 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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
hms₁ : x - (↑⌊x⌋ : R) ∈ s
⊢ 0 ≤ x - (↑⌊x⌋ : R)

Tactic:
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩

Premises used: Iff.mpr, sub_lt_iff_lt_add', Int.floor_eq_iff, And.intro, Iff.mp, sub_nonneg, rfl
-- 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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
hms₁ : x - (↑⌊x⌋ : R) ∈ s
hm0₁ : 0 ≤ x - (↑⌊x⌋ : R)
⊢ x - (↑⌊x⌋ : R) < 1

Tactic:
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩

Premises used: Iff.mpr, sub_lt_iff_lt_add', Int.floor_eq_iff, And.intro, Iff.mp, sub_nonneg, rfl
-- 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
s : Set R
x : R
hms : x - (↑⌊x⌋ : R) ∈ s
hm0 : 0 ≤ x - (↑⌊x⌋ : R)
hm1 : x - (↑⌊x⌋ : R) < 1
⊢ fract x ∈ s

Tactic:
hms

Premises used: Set.Mem, 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
s : Set R
x : R
hms : x - (↑⌊x⌋ : R) ∈ s
hm0 : 0 ≤ x - (↑⌊x⌋ : R)
hm1 : x - (↑⌊x⌋ : R) < 1
⊢ fract x ∈ s

Tactic:
exact hms
-- 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
s : Set R
h : ∀ (x : R), x ∈ fract '' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) '' s ∩ Ico 0 1) x
⊢ fract '' s = ⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) '' s ∩ Ico 0 1

Tactic:
ext x
-- 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
s : Set R
x : R
h : (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
⊢ x ∈ fract '' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) '' s ∩ Ico 0 1) x

Tactic:
simp only [mem_image, mem_inter_iff, mem_iUnion]

Premises used: Set.mem_inter_iff, Set.mem_iUnion, Set.mem_image
-- 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
s : Set R
x : R
h : (∃ x_1 ∈ s, fract x_1 = x) → ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
h₁ : (∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x) → ∃ x_1 ∈ s, fract x_1 = x
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x

Tactic:
constructor
-- 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
s : Set R
y : R
hy : y ∈ s
⊢ ∃ (i : ℤ), (∃ x ∈ s, x - (↑i : R) = fract y) ∧ Membership.mem (γ := Set R) (Ico 0 1) (fract y)

Tactic:
⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩

Premises used: Int.floor, And.intro, Int.fract_lt_one, Exists.intro, Int.fract_nonneg, rfl
-- 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
s : Set R
y : R
hy : y ∈ s
⊢ ∃ (i : ℤ), (∃ x ∈ s, x - (↑i : R) = fract y) ∧ Membership.mem (γ := Set R) (Ico 0 1) (fract y)

Tactic:
exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩
-- 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
s : Set R
m : ℤ
y : R
hys : y ∈ s
h0 : 0 ≤ y - (↑m : R)
h1 : y - (↑m : R) < 1
⊢ ⌊y⌋ = m

Tactic:
floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩

Premises used: Iff.mpr, sub_lt_iff_lt_add', Int.floor_eq_iff, And.intro, Iff.mp, sub_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
s : Set R
m : ℤ
y : R
hys : y ∈ s
h0 : 0 ≤ y - (↑m : R)
h1 : y - (↑m : R) < 1
h : ∀ (h0 : 0 ≤ y - (↑⌊y⌋ : R)) (h1 : y - (↑⌊y⌋ : R) < 1), ∃ x ∈ s, fract x = y - (↑⌊y⌋ : R)
⊢ ∃ x ∈ s, fract x = y - (↑m : R)

Tactic:
obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩

Premises used: Iff.mpr, sub_lt_iff_lt_add', Int.floor_eq_iff, And.intro, Iff.mp, sub_nonneg, rfl