awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
⊢ a ≤ HAdd.hAdd (α := R) (↑⌊a⌋₊ : R) 1

Tactic:
exact (lt_floor_add_one a).le

Premises used: LT.lt.le, Nat.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : FloorSemiring R
z : ℤ
a : ℕ
simp : LE.le.{u_3} (α := R) (↑z : R) (↑a : R) ↔ z ≤ (↑a : ℤ)
⊢ ceil.{u_3} (α := R) (↑z : R) ≤ a ↔ z.toNat ≤ a

Tactic:
simp only [ceil_le, Int.toNat_le]

Premises used: Int.toNat_le, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : FloorSemiring R
z : ℤ
a : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : z ≤ (↑a : ℤ) ↔ z ≤ (↑a : ℤ)
⊢ LE.le.{u_3} (α := R) (↑z : R) (↑a : R) ↔ z ≤ (↑a : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
n a : ℕ
rw : LE.le.{u_1} (α := R) (↑n : R) (↑a : R) ↔ n ≤ a
rw₁ rw₂ : n ≤ a ↔ n ≤ a
⊢ ceil.{u_1} (α := R) (↑n : R) ≤ a ↔ n ≤ a

Tactic:
rw [ceil_le, cast_le]

Premises used: Nat.cast_le, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
rw : ceil.{u_1} (α := R) (↑0 : R) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ ceil.{u_1} (α := R) 0 = 0

Tactic:
rw [← Nat.cast_zero, ceil_natCast]

Premises used: Nat.ceil_natCast, Nat.cast_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
rw : ceil.{u_1} (α := R) (↑1 : R) = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ ceil.{u_1} (α := R) 1 = 1

Tactic:
rw [← Nat.cast_one, ceil_natCast]

Premises used: Nat.ceil_natCast, Nat.cast_one
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ceil.{u_1} (α := R) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
ceil_natCast n

Premises used: Nat.ceil_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
n : ℕ
inst_3 : IsStrictOrderedRing R
h : ⌈a⌉₊ < n
⊢ a < (↑n : R)

Tactic:
(le_ceil a).trans_lt (Nat.cast_lt.2 h)

Premises used: Iff.mpr, Nat.le_ceil, Nat.cast_lt, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
n : ℕ
inst_3 : IsStrictOrderedRing R
h : ⌈a⌉₊ ≤ n
⊢ a ≤ (↑n : R)

Tactic:
(le_ceil a).trans (Nat.cast_le.2 h)

Premises used: Iff.mpr, Nat.le_ceil, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
inl : ∀ (ha : a ≤ 0), ⌊a⌋₊ ≤ ⌈a⌉₊
inr : ∀ (ha : 0 ≤ a), ⌊a⌋₊ ≤ ⌈a⌉₊
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
obtain ha | ha := le_total a 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
ha : a ≤ 0
inl : 0 ≤ ⌈a⌉₊
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
rw [floor_of_nonpos ha]

Premises used: Nat.floor_of_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
cast_le.1 ((floor_le ha).trans <| le_ceil _)

Premises used: Iff.mp, Nat.floor_le, Nat.le_ceil, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
exact cast_le.1 ((floor_le ha).trans <| le_ceil _)

Premises used: Iff.mp, Nat.floor_le, Nat.le_ceil, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
inl : ∀ (ha : 0 ≤ a), ⌊a⌋₊ < ⌈b⌉₊
inr : ∀ (ha : a < 0), ⌊a⌋₊ < ⌈b⌉₊
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rcases le_or_gt 0 a with (ha | ha)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
inl : a < (↑⌈b⌉₊ : R)
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rw [floor_lt ha]

Premises used: Nat.floor_lt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ a < (↑⌈b⌉₊ : R)

Tactic:
h.trans_le (le_ceil _)

Premises used: LT.lt.trans_le, Nat.le_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ a < (↑⌈b⌉₊ : R)

Tactic:
exact h.trans_le (le_ceil _)

Premises used: LT.lt.trans_le, Nat.le_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
inr : 0 < ⌈b⌉₊
inr₁ : (↑0 : R) < b
inr₂ inr₃ inr₄ inr₅ : 0 < b
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]

Premises used: LT.lt.le, Nat.floor_of_nonpos, Nat.lt_ceil, Nat.cast_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
ha : 0 ≤ a
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋₊ ⌈b⌉₊
⊢ Nat.cast ⁻¹' Ioo a b = Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
ha : 0 ≤ a
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
simp [floor_lt, lt_ceil, ha]

Premises used: Nat.floor_lt, Nat.lt_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉₊ ⌈b⌉₊
⊢ Nat.cast ⁻¹' Ico a b = Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
simp [ceil_le, lt_ceil]

Premises used: Nat.lt_ceil, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋₊ ⌊b⌋₊
⊢ Nat.cast ⁻¹' Ioc a b = Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
simp [floor_lt, le_floor_iff, hb, ha]

Premises used: Nat.le_floor_iff, Nat.floor_lt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
hb : 0 ≤ b
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉₊ ⌊b⌋₊
⊢ Nat.cast ⁻¹' Icc a b = Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
hb : 0 ≤ b
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
simp [ceil_le, hb, le_floor_iff]

Premises used: Nat.le_floor_iff, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋₊
⊢ Nat.cast ⁻¹' Ioi a = Ioi ⌊a⌋₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋₊

Tactic:
simp [floor_lt, ha]

Premises used: Nat.floor_lt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉₊
⊢ Nat.cast ⁻¹' Ici a = Ici ⌈a⌉₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉₊

Tactic:
simp [ceil_le]

Premises used: Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉₊
⊢ Nat.cast ⁻¹' Iio a = Iio ⌈a⌉₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉₊

Tactic:
simp [lt_ceil]

Premises used: Nat.lt_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋₊
⊢ Nat.cast ⁻¹' Iic a = Iic ⌊a⌋₊

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
x : ℕ
⊢ x ∈ Nat.cast ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋₊

Tactic:
simp [le_floor_iff, ha]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
rw : (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
⊢ b ≤ ⌊a + (↑n : R)⌋₊ ↔ b ≤ ⌊a⌋₊ + n

Tactic:
rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]

Premises used: Nat.cast_nonneg, Nat.le_floor_iff, add_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
inl : ∀ (hb : n ≤ b), (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
inr : ∀ (hb : b ≤ n), (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n

Tactic:
obtain hb | hb := le_total n b

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
inl : ∀ (d : ℕ) (hb : n ≤ n + d), (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₃ : (↑d : R) ≤ a ↔ d + n ≤ ⌊a⌋₊ + n
inl₄ : (↑d : R) ≤ a ↔ d ≤ ⌊a⌋₊
inl₅ inl₆ : (↑d : R) ≤ a ↔ (↑d : R) ≤ a
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n

Tactic:
rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]

Premises used: Nat.le_floor_iff, Nat.cast, add_comm, Nat.cast_add, add_le_add_iff_right
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
inr : ∀ (d : ℕ) (hb : b ≤ b + d), (↑b : R) ≤ a + (↑(b + d) : R) ↔ b ≤ ⌊a⌋₊ + (b + d)
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
inr : (↑b : R) ≤ (↑b : R) + (a + (↑d : R)) ↔ b ≤ b + (⌊a⌋₊ + d)
⊢ (↑b : R) ≤ a + (↑(b + d) : R) ↔ b ≤ ⌊a⌋₊ + (b + d)

Tactic:
rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]

Premises used: add_left_comm, Nat.cast, Nat.cast_add
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ (↑b : R) ≤ (↑b : R) + (a + (↑d : R)) ↔ b ≤ b + (⌊a⌋₊ + d)

Tactic:
iff_of_true ?_ le_self_add

Premises used: iff_of_true, le_self_add
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
inr : (↑b : R) ≤ (↑b : R) + (a + (↑d : R))
⊢ (↑b : R) ≤ (↑b : R) + (a + (↑d : R)) ↔ b ≤ b + (⌊a⌋₊ + d)

Tactic:
refine iff_of_true ?_ le_self_add

Premises used: iff_of_true, le_self_add
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ (↑b : R) ≤ (↑b : R) + (a + (↑d : R))

Tactic:
le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

Premises used: Nat.cast_nonneg, le_add_of_nonneg_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ (↑b : R) ≤ (↑b : R) + (a + (↑d : R))

Tactic:
exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

Premises used: le_add_of_nonneg_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
rw : ⌊a + (↑1 : R)⌋₊ = ⌊a⌋₊ + 1
rw₁ rw₂ : ⌊a⌋₊ + 1 = ⌊a⌋₊ + 1
⊢ ⌊a + 1⌋₊ = ⌊a⌋₊ + 1

Tactic:
rw [← cast_one, floor_add_natCast ha 1]

Premises used: Nat.floor_add_natCast, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌊a + OfNat.ofNat n⌋₊ = ⌊a⌋₊ + OfNat.ofNat n

Tactic:
floor_add_natCast ha n

Premises used: Nat.floor_add_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
inl : ∀ (ha : a ≤ 0), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
inr : ∀ (ha : 0 ≤ a), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n

Tactic:
obtain ha | ha := le_total a 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
inl : ⌊a - (↑n : R)⌋₊ = 0 - n
inl₁ : 0 = 0 - n
inl₂ inl₃ : Eq (α := ℕ) 0 0
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]

Premises used: Nat.cast_nonneg, tsub_nonpos_of_le, Nat.floor_of_nonpos, LE.le.trans, zero_tsub
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
inr : ∀ (h : a ≤ (↑n : R)), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
inr₁ : ∀ (h : (↑n : R) ≤ a), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n

Tactic:
rcases le_total a n with h | h

Premises used: le_total, Nat.cast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ (↑n : R)
inr : ⌊a⌋₊ ≤ n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]

Premises used: tsub_nonpos_of_le, tsub_eq_zero_iff_le, eq_comm, Nat.floor_of_nonpos
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ (↑n : R)
⊢ ⌊a⌋₊ ≤ n

Tactic:
Nat.cast_le.1 ((Nat.floor_le ha).trans h)

Premises used: Iff.mp, Nat.floor_le, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ (↑n : R)
⊢ ⌊a⌋₊ ≤ n

Tactic:
exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)

Premises used: Iff.mp, Nat.floor_le, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : (↑n : R) ≤ a
rw : 0 ≤ a - (↑n : R)
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]

Premises used: Nat.floor_add_natCast, tsub_add_cancel_of_le, Nat.le_floor, eq_tsub_iff_add_eq_of_le
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : (↑n : R) ≤ a
⊢ 0 ≤ a - (↑n : R)

Tactic:
le_tsub_of_add_le_left ((add_zero _).trans_le h)

Premises used: le_tsub_of_add_le_left, Eq.trans_le, add_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : (↑n : R) ≤ a
⊢ 0 ≤ a - (↑n : R)

Tactic:
exact le_tsub_of_add_le_left ((add_zero _).trans_le h)

Premises used: le_tsub_of_add_le_left, Eq.trans_le, add_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
⊢ ⌊a - 1⌋₊ = ⌊a⌋₊ - 1

Tactic:
mod_cast floor_sub_natCast a 1

Premises used: congrArg, HSub.hSub, cast, Nat.floor_sub_natCast, Nat.floor, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
inst_7 : n.AtLeastTwo
⊢ ⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n

Tactic:
floor_sub_natCast a n

Premises used: Nat.floor_sub_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
contrapose! : b < ⌈a + (↑n : R)⌉₊ ↔ b < ⌈a⌉₊ + n
⊢ ⌈a + (↑n : R)⌉₊ ≤ b ↔ ⌈a⌉₊ + n ≤ b

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
rw : (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
⊢ b < ⌈a + (↑n : R)⌉₊ ↔ b < ⌈a⌉₊ + n

Tactic:
rw [lt_ceil]

Premises used: Nat.lt_ceil
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
inl : ∀ (hb : n ≤ b), (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
inr : ∀ (hb : b < n), (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n

Tactic:
obtain hb | hb := le_or_gt n b

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
inl : ∀ (d : ℕ) (hb : n ≤ n + d), (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₃ : (↑d : R) < a ↔ d + n < ⌈a⌉₊ + n
inl₄ : (↑d : R) < a ↔ d < ⌈a⌉₊
inl₅ inl₆ : (↑d : R) < a ↔ (↑d : R) < a
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n

Tactic:
rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]

Premises used: Nat.cast, add_comm, Nat.cast_add, Nat.lt_ceil, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n

Tactic:
iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

Premises used: Iff.mpr, iff_of_true, Nat.lt_add_left, Nat.cast_lt, lt_add_of_nonneg_of_lt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n

Tactic:
exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

Premises used: Iff.mpr, iff_of_true, Nat.lt_add_left, Nat.cast_lt, lt_add_of_nonneg_of_lt
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
rw : ⌈a + (↑1 : R)⌉₊ = ⌈a⌉₊ + 1
rw₁ rw₂ : ⌈a⌉₊ + 1 = ⌈a⌉₊ + 1
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

Tactic:
rw [cast_one.symm, ceil_add_natCast ha 1]

Premises used: Nat.ceil_add_natCast, OfNat.ofNat, Eq.symm, Nat.cast_one
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌈a + OfNat.ofNat n⌉₊ = ⌈a⌉₊ + OfNat.ofNat n

Tactic:
ceil_add_natCast ha n

Premises used: Nat.ceil_add_natCast