mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ ≤ a + b

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ ≤ a + b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a⌋ + ↑n = ⌊a⌋ + ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : R
⊢ ↑n + ⌊a⌋ = ↑n + ⌊a⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊a + -↑z⌋ = ⌊a + -↑z⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a⌋ - ↑n = ⌊a⌋ - ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R}, ⌊a⌋ = ⌊b⌋ → b ≤ a → |a - b| < 1
h0 : ¬b ≤ a
⊢ |b - a| < 1

Tactic:
]

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R}, ⌊a⌋ = ⌊b⌋ → b ≤ a → |a - b| < 1
h0 : ¬b ≤ a
⊢ |b - a| < 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
⊢ ↑m ≤ a ↔ ↑m ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * x = k * ↑⌊x⌋ + 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
]

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * x = k * ↑⌊x⌋ + 1 ↔ ∃ n, k * x = k * ↑n + 1
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ k * ↑n ≤ k * ↑n + 1 ∧ k * ↑n + 1 < k * (↑n + 1)

Tactic:
]

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ k * ↑n ≤ k * ↑n + 1 ∧ k * ↑n + 1 < k * (↑n + 1)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊a⌋ = ⌊a⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a⌋ = ⌊a⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a / ↑n * ↑n⌋ / n

Tactic:
]

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a / ↑n * ↑n⌋ / n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a / ↑n⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
m : ℤ
a : R
⊢ fract a = fract a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : R
⊢ fract a = fract a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ↑z - ↑z = 0

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ↑z - ↑z = 0
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ 0 ≤ fract a ∧ fract a < 1

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ 0 ≤ fract a ∧ fract a < 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ = ↑z

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ ↑⌊a⌋ - ↑⌊b⌋ = ↑⌊a⌋ - ↑⌊b⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a : R
Hsq : 0 ≤ a ^ 2
Hsq' : 0 ≤ (1 + a) ^ 2
H : 0 ≤ 2 + a
n : ℕ
⊢ 0 ≤ 2 * 1 + a

Tactic:
simpa using H

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 ≤ a

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 ≤ a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ fract x ≤ 1

Tactic:
]

Goal state after:
case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ fract x ≤ 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z

Tactic:
]

Goal state after:
case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)

Tactic:
]

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1

Tactic:
]

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)

Tactic:
]

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑m

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ ↑(l₀ % n) / ↑n = ↑(l₀ % n) / ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Tactic:
]

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)

Tactic:
]

Goal state after:
case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_2.e_a
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ -↑m₀ % ↑n = -↑m₀ % ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
⊢ -(-q.num / ↑q.den) = -(-q.num / ↑q.den)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Tactic:
]

Goal state after:
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a ≤ ↑⌊a⌋ + 1

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a ≤ ↑⌊a⌋ + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ -1 < a

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ -1 < a
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den

Tactic:
]

Goal state after:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑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)

Tactic:
]

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑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)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < d

Tactic:
]

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < d
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
⊢ -(-n / ↑d) = -(-n / ↑d)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)

Tactic:
]

Goal state after:
n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ⌊-x⌋ = ⌊-x⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ a ≤ -↑z ↔ a ≤ -↑z

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ ⌊x + 1 / 2⌋ = ⌊x + 1 / 2⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ -↑z ≤ a ↔ -↑z ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z a : ℤ
⊢ z ≤ a ↔ z ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: a : ℤ
ha : 0 < a
⊢ 0 < 1

Tactic:
]

Goal state after:
a : ℤ
ha : 0 < a
⊢ 0 < 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : ℤ
⊢ ↑n ≤ a ↔ ↑n ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ⌊↑n / ↑d⌋

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊-a⌋ - z = ⌊-a⌋ - z

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
a : R
⊢ z + ⌈a⌉ = z + ⌈a⌉

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑n / ↑d⌉.toNat

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑n / ↑d⌉.toNat
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a⌉ + ↑n = ⌈a⌉ + ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌈a + 1⌉ = ⌈a + 1⌉

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌈a + -↑z⌉ = ⌈a + -↑z⌉

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌈a⌉ = ⌈a⌉

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌈a⌉ < ⌈a⌉ + 1

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌈a⌉ < ⌈a⌉ + 1