awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ∞
⊢ ⌈(↑n : ℝ≥0∞) + r⌉ₑ = n + ⌈r⌉ₑ

Tactic:
simp [add_comm, ceil_add_toENNReal]

Premises used: add_comm, ENat.ceil_add_toENNReal
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
⊢ ⌊r + (↑n : ℝ≥0∞)⌋ₑ = ⌊r⌋ₑ + (↑n : ℕ∞)

Tactic:
floor_add_toENNReal r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.floor_add_toENNReal
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
⊢ ⌈r + (↑n : ℝ≥0∞)⌉ₑ = ⌈r⌉ₑ + (↑n : ℕ∞)

Tactic:
ceil_add_toENNReal r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.ceil_add_toENNReal, ENat.map
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
⊢ ⌊(↑n : ℝ≥0∞) + r⌋ₑ = (↑n : ℕ∞) + ⌊r⌋ₑ

Tactic:
floor_toENNReal_add r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.floor_toENNReal_add
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
⊢ ⌈(↑n : ℝ≥0∞) + r⌉ₑ = (↑n : ℕ∞) + ⌈r⌉ₑ

Tactic:
ceil_toENNReal_add r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.ceil_toENNReal_add
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ ⌊r + 1⌋ₑ = ⌊r⌋ₑ + 1

Tactic:
mod_cast floor_add_natCast r 1

Premises used: congrArg, ENat.floor_add_natCast, cast, ENat.floor, HAdd.hAdd, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ ⌈r + 1⌉ₑ = ⌈r⌉ₑ + 1

Tactic:
mod_cast ceil_add_natCast r 1

Premises used: ENat.ceil_add_natCast, congrArg, cast, ENat.ceil, HAdd.hAdd, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
inst : n.AtLeastTwo
⊢ ⌊r + OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ + OfNat.ofNat n

Tactic:
floor_add_natCast r n

Premises used: ENat.floor_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
inst : n.AtLeastTwo
⊢ ⌈r + OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ + OfNat.ofNat n

Tactic:
ceil_add_natCast r n

Premises used: ENat.ceil_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌊∞ - (↑⊤ : ℝ≥0∞)⌋ₑ = ⌊∞⌋ₑ - ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
⊢ ⌊∞ - (↑(↑n : ℕ∞) : ℝ≥0∞)⌋ₑ = ⌊∞⌋ₑ - (↑n : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
⊢ ⌊(↑r : ℝ≥0∞) - (↑⊤ : ℝ≥0∞)⌋ₑ = ⌊(↑r : ℝ≥0∞)⌋ₑ - ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
norm_cast : ⌊r - (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ - n
⊢ ⌊(↑(r - (↑n : ℝ≥0)) : ℝ≥0∞)⌋ₑ = (↑(⌊r⌋₊ - n) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌊r - (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ - n

Tactic:
Nat.floor_sub_natCast ..

Premises used: Nat.floor_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌊r - (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ - n

Tactic:
exact Nat.floor_sub_natCast ..

Premises used: Nat.floor_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
⊢ ⌈∞ - (↑⊤ : ℝ≥0∞)⌉ₑ = ⌈∞⌉ₑ - ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
n : ℕ
⊢ ⌈∞ - (↑(↑n : ℕ∞) : ℝ≥0∞)⌉ₑ = ⌈∞⌉ₑ - (↑n : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
⊢ ⌈(↑r : ℝ≥0∞) - (↑⊤ : ℝ≥0∞)⌉ₑ = ⌈(↑r : ℝ≥0∞)⌉ₑ - ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
norm_cast : ⌈r - (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ - n
⊢ ⌈(↑(r - (↑n : ℝ≥0)) : ℝ≥0∞)⌉ₑ = (↑(⌈r⌉₊ - n) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌈r - (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ - n

Tactic:
Nat.ceil_sub_natCast ..

Premises used: Nat.ceil_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌈r - (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ - n

Tactic:
exact Nat.ceil_sub_natCast ..

Premises used: Nat.ceil_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
⊢ ⌊r - (↑n : ℝ≥0∞)⌋ₑ = ⌊r⌋ₑ - (↑n : ℕ∞)

Tactic:
floor_sub_toENNReal r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.floor_sub_toENNReal
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
⊢ ⌈r - (↑n : ℝ≥0∞)⌉ₑ = ⌈r⌉ₑ - (↑n : ℕ∞)

Tactic:
ceil_sub_toENNReal r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.ceil_sub_toENNReal
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ ⌊r - 1⌋ₑ = ⌊r⌋ₑ - 1

Tactic:
mod_cast floor_sub_toENNReal r 1

Premises used: congrArg, HSub.hSub, cast, ENat.toENNReal, ENat.floor_sub_toENNReal, ENat.toENNReal_one, ENat.floor, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
⊢ ⌈r - 1⌉ₑ = ⌈r⌉ₑ - 1

Tactic:
mod_cast ceil_sub_toENNReal r 1

Premises used: congrArg, HSub.hSub, cast, ENat.ceil, ENat.toENNReal, ENat.ceil_sub_toENNReal, ENat.toENNReal_one, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
inst : n.AtLeastTwo
⊢ ⌊r - OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ - OfNat.ofNat n

Tactic:
floor_sub_toENNReal r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.floor_sub_toENNReal
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
n : ℕ
inst : n.AtLeastTwo
⊢ ⌈r - OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ - OfNat.ofNat n

Tactic:
ceil_sub_toENNReal r n

Premises used: WithTop.map, ENat.toENNReal, Nat.cast, WithTop.some, ENat.map, ENat.ceil_sub_toENNReal
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
hr : r ≠ ∞
⊢ r ≠ ∞

Tactic:
hr
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
hr : r ≠ ∞
lift : ∀ (r : ℝ≥0), (↑⌈(↑r : ℝ≥0∞)⌉ₑ : ℝ≥0∞) < (↑r : ℝ≥0∞) + 1
⊢ (↑⌈r⌉ₑ : ℝ≥0∞) < r + 1

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0
⊢ (↑⌈(↑r : ℝ≥0∞)⌉ₑ : ℝ≥0∞) < (↑r : ℝ≥0∞) + 1

Tactic:
simpa using mod_cast Nat.ceil_lt_add_one zero_le

Premises used: zero_le, Nat.ceil_lt_add_one
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0∞
⊢ ⌈∞ + x⌉ₑ ≤ ⌈∞⌉ₑ + ⌈x⌉ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
x : ℝ≥0∞
⊢ ⌈x + ∞⌉ₑ ≤ ⌈x⌉ₑ + ⌈∞⌉ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
ι : Sort u_1
f : ι → ℕ∞
x : ℝ≥0∞
⊢ (↑(⨆ (i : ι), f i) : ℝ≥0∞) ≤ x ↔ ⨆ (i : ι), (↑(f i) : ℝ≥0∞) ≤ x

Tactic:
simp [← le_floor]

Premises used: ENat.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
ι : Sort u_1
f : ι → ℕ∞
x : ℝ≥0∞
⊢ x ≤ (↑(⨅ (i : ι), f i) : ℝ≥0∞) ↔ x ≤ ⨅ (i : ι), (↑(f i) : ℝ≥0∞)

Tactic:
simp [← ceil_le]

Premises used: ENat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋ₑ
⊢ toENNReal ⁻¹' Ioi a = Ioi ⌊a⌋ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉ₑ
⊢ toENNReal ⁻¹' Iio a = Iio ⌈a⌉ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋ₑ
⊢ toENNReal ⁻¹' Iic a = Iic ⌊a⌋ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉ₑ
⊢ toENNReal ⁻¹' Ici a = Ici ⌈a⌉ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉ₑ ⌊b⌋ₑ
⊢ toENNReal ⁻¹' Icc a b = Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉ₑ ⌈b⌉ₑ
⊢ toENNReal ⁻¹' Ico a b = Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋ₑ ⌊b⌋ₑ
⊢ toENNReal ⁻¹' Ioc a b = Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ
⊢ toENNReal ⁻¹' Ioo a b = Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
a b : ℝ≥0∞
x : ℕ∞
⊢ x ∈ toENNReal ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Extended
Goal:
r : ℝ≥0∞
hr : 0 < r
⊢ 0 < ⌈r⌉ₑ

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ⌊a⌋

Tactic:
Int.floor_nonneg.2 ha

Premises used: Iff.mpr, Int.floor_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
ha : 0 < a
⊢ 0 ≤ ⌊a⌋

Tactic:
int_floor_nonneg ha.le

Premises used: LT.lt.le, Mathlib.Meta.Positivity.int_floor_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : FloorSemiring α
a : α
⊢ 0 < a → 0 < ⌈a⌉₊

Tactic:
Nat.ceil_pos.2

Premises used: Iff.mpr, Nat.ceil_pos
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
a : α
⊢ 0 < a → 0 < ⌈a⌉

Tactic:
Int.ceil_pos.2

Premises used: Iff.mpr, Int.ceil_pos
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : a < (↑(z + 1) : R) ↔ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ ≤ z ↔ a < HAdd.hAdd (α := R) (↑z : R) 1

Tactic:
rw [← lt_add_one_iff, floor_lt]

Premises used: Int.floor_lt, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a < (↑(z + 1) : R) ↔ a < (↑(z + 1) : R)
⊢ a < (↑(z + 1) : R) ↔ a < HAdd.hAdd (α := R) (↑z : R) 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : (↑(z + 1) : R) ≤ a ↔ HAdd.hAdd (α := R) (↑z : R) 1 ≤ a
⊢ z < ⌊a⌋ ↔ HAdd.hAdd (α := R) (↑z : R) 1 ≤ a

Tactic:
rw [← add_one_le_iff, le_floor]

Premises used: Int.add_one_le_iff, Int.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑(z + 1) : R) ≤ a ↔ (↑(z + 1) : R) ≤ a
⊢ (↑(z + 1) : R) ≤ a ↔ HAdd.hAdd (α := R) (↑z : R) 1 ≤ a

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z - 1 ↔ ⌊a⌋ < z
rw₁ rw₂ : ⌊a⌋ < z ↔ ⌊a⌋ < z
⊢ ⌊a⌋ ≤ z - 1 ↔ a < (↑z : R)

Tactic:
rw [← floor_lt, le_sub_one_iff]

Premises used: Int.le_sub_one_iff, Int.floor_lt
-- 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⌋ ≤ -1 ↔ a < 0

Tactic:
simpa using floor_le_iff (z := -1)

Premises used: Int.floor_le_iff
-- 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⌋.succ : R)

Tactic:
floor_lt.1 <| Int.lt_succ_self _

Premises used: Int.lt_succ_self, Int.floor_lt, Iff.mp
-- 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 < HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1

Tactic:
simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a

Premises used: Int.lt_succ_floor, Int.cast_add, Int.succ, 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
⊢ Monotone.{u_2, 0} (α := R) floor

Tactic:
gc_coe_floor.monotone_u

Premises used: GaloisConnection.monotone_u, Int.gc_coe_floor
-- 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
hab : a ≤ b
⊢ ⌊a⌋ ≤ ⌊b⌋

Tactic:
floor_mono hab

Premises used: Int.floor_mono
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
rw : HAdd.hAdd (α := ℤ) 0 1 ≤ ⌊a⌋ ↔ 1 ≤ a
rw₁ : 1 ≤ ⌊a⌋ ↔ 1 ≤ a
rw₂ : (↑1 : R) ≤ a ↔ 1 ≤ a
rw₃ rw₄ : 1 ≤ a ↔ 1 ≤ a
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a

Tactic:
rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]

Premises used: Int.lt_iff_add_one_le, zero_add, Int.le_floor, 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
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₂ : ⌊a⌋ < z + 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₃ : a < (↑(z + 1) : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₄ : a < HAdd.hAdd (α := R) (↑z : R) (↑1 : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₅ : a < HAdd.hAdd (α := R) (↑z : R) 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₆ rw₇ : (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1 ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1

Tactic:
rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]

Premises used: Int.floor_lt, Int.cast_add, and_comm, le_antisymm_iff, Int.le_floor, Int.lt_add_one_iff, 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
a : R
⊢ ⌊a⌋ = 0 ↔ Membership.mem (γ := Set R) (Ico 0 1) a

Tactic:
simp [floor_eq_iff]

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
n : ℤ
⊢ ∀ a ∈ Ico (↑n : R) (HAdd.hAdd (α := R) (↑n : R) 1), ⌊a⌋ = n

Tactic:
fun _ ⟨h₀, h₁⟩ =>
  floor_eq_iff.mpr ⟨h₀, h₁⟩

Premises used: Iff.mpr, Int.floor, Int.floor_eq_iff, _private.0.Int.floor_eq_on_Ico.match_1, And.intro, Eq
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
n : ℤ
⊢ ∀ a ∈ Ico (↑n : R) (HAdd.hAdd (α := R) (↑n : R) 1), Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑n : R)

Tactic:
fun a ha =>
  congr_arg _ <| floor_eq_on_Ico n a ha

Premises used: Int.cast, congr_arg, Int.floor_eq_on_Ico
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
m : ℤ
⊢ floor ⁻¹' {m} = Ico (↑m : R) (HAdd.hAdd (α := R) (↑m : R) 1)

Tactic:
ext fun _ => floor_eq_iff

Premises used: Set.ext, 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 : R
⊢ a - 1 < (↑⌊a⌋ : R)

Tactic:
sub_lt_iff_lt_add.2 (lt_floor_add_one a)

Premises used: Iff.mpr, Int.lt_floor_add_one, sub_lt_iff_lt_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
z a : ℤ
rw : LE.le.{u_2} (α := R) (↑a : R) (↑z : R) ↔ a ≤ z
rw₁ rw₂ : a ≤ z ↔ a ≤ z
⊢ a ≤ floor.{u_2} (α := R) (↑z : R) ↔ a ≤ z

Tactic:
rw [le_floor, Int.cast_le]

Premises used: Int.cast_le, Int.le_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
n : ℕ
a : ℤ
rw : LE.le.{u_2} (α := R) (↑a : R) (↑n : R) ↔ a ≤ (↑n : ℤ)
rw₁ : LE.le.{u_2} (α := R) (↑a : R) (↑(↑n : ℤ) : R) ↔ a ≤ (↑n : ℤ)
rw₂ rw₃ : a ≤ (↑n : ℤ) ↔ a ≤ (↑n : ℤ)
⊢ a ≤ floor.{u_2} (α := R) (↑n : R) ↔ a ≤ (↑n : ℤ)

Tactic:
rw [le_floor, ← cast_natCast, cast_le]

Premises used: Int.cast_natCast, Int.cast_le, Int.le_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
rw : floor.{u_2} (α := R) (↑0 : R) = 0
rw₁ rw₂ : Eq (α := ℤ) 0 0
⊢ floor.{u_2} (α := R) 0 = 0

Tactic:
rw [← cast_zero, floor_intCast]

Premises used: Int.floor_intCast, Int.cast_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
rw : floor.{u_2} (α := R) (↑1 : R) = 1
rw₁ rw₂ : Eq (α := ℤ) 1 1
⊢ floor.{u_2} (α := R) 1 = 1

Tactic:
rw [← cast_one, floor_intCast]

Premises used: Int.floor_intCast, 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
n : ℕ
inst_4 : n.AtLeastTwo
⊢ floor.{u_2} (α := R) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
floor_natCast n

Premises used: Int.floor_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_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
rw₄ rw₅ : HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1 ↔ HSub.hSub (α := R) (↑a : R) (↑z : R) ≤ a_1
⊢ a ≤ ⌊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]

Premises used: Int.cast_sub, sub_le_iff_le_add, Int.le_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
rw : ⌊a + (↑1 : R)⌋ = ⌊a⌋ + 1
rw₁ rw₂ : ⌊a⌋ + 1 = ⌊a⌋ + 1
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1

Tactic:
rw [← cast_one, floor_add_intCast]

Premises used: Int.floor_add_intCast, 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
a b : R
rw : HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) ≤ a + b
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
rw [le_floor, Int.cast_add]

Premises used: Int.cast_add, Int.le_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₁ : (↑⌊a⌋ : R) ≤ a
h₂ : (↑⌊b⌋ : R) ≤ b
⊢ HAdd.hAdd (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) ≤ a + b

Tactic:
gcongr
-- 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⌋ : R) ≤ a

Tactic:
apply floor_le

Premises used: 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
⊢ (↑⌊b⌋ : R) ≤ b

Tactic:
apply floor_le

Premises used: 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
rw : HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ (↑⌊b⌋ : R)
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]

Premises used: Int.cast_sub, sub_le_iff_le_add, sub_le_comm, Int.le_floor, 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
a b : R
⊢ HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ (↑⌊b⌋ : R)

Tactic:
le_trans ?_ (sub_one_lt_floor _).le

Premises used: Int.sub_one_lt_floor, LT.lt.le, le_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 b : R
refine : HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ b - 1
⊢ HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ (↑⌊b⌋ : R)

Tactic:
refine le_trans ?_ (sub_one_lt_floor _).le

Premises used: Int.sub_one_lt_floor, LT.lt.le, le_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 b : R
rw : (↑⌊a + b⌋ : R) ≤ a + b
⊢ HSub.hSub (α := R) (↑⌊a + b⌋ : R) 1 - a ≤ b - 1

Tactic:
rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]

Premises used: add_sub_assoc, sub_le_sub_iff_right, sub_le_iff_le_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⌋ : R) ≤ a + b

Tactic:
floor_le _

Premises used: 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
⊢ (↑⌊a + b⌋ : R) ≤ a + b

Tactic:
exact floor_le _

Premises used: 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
z : ℤ
a : R
⊢ ⌊(↑z : R) + a⌋ = z + ⌊a⌋

Tactic:
simpa only [add_comm] using floor_add_intCast a z

Premises used: add_comm, Int.floor_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
a : R
n : ℕ
rw : ⌊a + (↑(↑n : ℤ) : R)⌋ = ⌊a⌋ + (↑n : ℤ)
rw₁ rw₂ : ⌊a⌋ + (↑n : ℤ) = ⌊a⌋ + (↑n : ℤ)
⊢ ⌊a + (↑n : R)⌋ = ⌊a⌋ + (↑n : ℤ)

Tactic:
rw [← Int.cast_natCast, floor_add_intCast]

Premises used: Int.cast_natCast, Int.floor_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
a : R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌊a + OfNat.ofNat n⌋ = ⌊a⌋ + OfNat.ofNat n

Tactic:
floor_add_natCast a n

Premises used: Int.floor_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
n : ℕ
a : R
rw : ⌊(↑(↑n : ℤ) : R) + a⌋ = (↑n : ℤ) + ⌊a⌋
rw₁ rw₂ : (↑n : ℤ) + ⌊a⌋ = (↑n : ℤ) + ⌊a⌋
⊢ ⌊(↑n : R) + a⌋ = (↑n : ℤ) + ⌊a⌋

Tactic:
rw [← Int.cast_natCast, floor_intCast_add]

Premises used: Int.cast_natCast, Int.floor_intCast_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
n : ℕ
inst_4 : n.AtLeastTwo
a : R
⊢ ⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋

Tactic:
floor_natCast_add n a

Premises used: Int.floor_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
z : ℤ
rw : ⌊a - (↑z : R)⌋ = ⌊a + -(↑z : R)⌋
rw₁ rw₂ : ⌊a + -(↑z : R)⌋ = ⌊a + -(↑z : R)⌋
⊢ ⌊a - (↑z : R)⌋ = ⌊a + (↑(-z) : R)⌋

Tactic:
rw [Int.cast_neg, sub_eq_add_neg]

Premises used: Int.cast_neg, 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 : R
n : ℕ
rw : ⌊a - (↑(↑n : ℤ) : R)⌋ = ⌊a⌋ - (↑n : ℤ)
rw₁ rw₂ : ⌊a⌋ - (↑n : ℤ) = ⌊a⌋ - (↑n : ℤ)
⊢ ⌊a - (↑n : R)⌋ = ⌊a⌋ - (↑n : ℤ)

Tactic:
rw [← Int.cast_natCast, floor_sub_intCast]

Premises used: Int.cast_natCast, Int.floor_sub_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
⊢ ⌊a - 1⌋ = ⌊a⌋ - 1

Tactic:
mod_cast floor_sub_natCast a 1

Premises used: Int.floor, congrArg, HSub.hSub, cast, congr, Int.floor_sub_natCast, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans