awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
rcases :
  ∀ (hd : Invertible (α := R) (↑d : R)),
    IsNat
      ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊
      0
⊢ IsNat ⌊r⌋₊ 0

Tactic:
rcases h with ⟨hd, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
n d : ℕ
hd : Invertible (α := R) (↑d : R)
out :
  ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊ =
    (↑0 : ℕ)
⊢ IsNat
    ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊
    0

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
n d : ℕ
hd : Invertible (α := R) (↑d : R)
out :
  HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _) < 1
⊢ ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊ =
    (↑0 : ℕ)

Tactic:
rw [Nat.cast_zero, Nat.floor_eq_zero]

Premises used: Nat.floor_eq_zero, Nat.cast_zero
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
n d : ℕ
hd : Invertible (α := R) (↑d : R)
⊢ HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _) ≤ 0

Tactic:
simp [mul_nonneg]

Premises used: mul_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
n d : ℕ
hd : Invertible (α := R) (↑d : R)
⊢ HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _) < 1

Tactic:
exact lt_of_le_of_lt (by simp [mul_nonneg]) one_pos

Premises used: lt_of_le_of_lt, one_pos
-- 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 : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ < n ↔ a < (↑n : R)

Tactic:
lt_iff_lt_of_le_iff_le <| le_floor_iff ha

Premises used: Nat.le_floor_iff, lt_iff_lt_of_le_iff_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
rw rw₁ : a < 1 ↔ a < 1
⊢ a < (↑1 : R) ↔ a < 1

Tactic:
rw [Nat.cast_one]

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

Tactic:
(le_floor_iff ha).1 le_rfl

Premises used: le_rfl, Nat.le_floor_iff, Iff.mp
-- 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 : ℕ
ha : 0 ≤ a
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
rw₃ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1
rw₄ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
rw₅ : ⌊a⌋₊ ≤ n ∧ n ≤ ⌊a⌋₊ ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
rw₆ rw₇ : n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
rw [← le_floor_iff ha, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt ha, Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]

Premises used: Nat.lt_add_one_iff, Nat.le_floor_iff, Nat.floor_lt, and_comm, Nat.cast_add, le_antisymm_iff, 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
n : ℕ
inst_3 : IsStrictOrderedRing R
h : ⌊a⌋₊ < n
⊢ a < (↑n : R)

Tactic:
lt_of_not_ge fun h' => (le_floor h').not_gt h

Premises used: lt_of_not_ge, LE.le.not_gt, Nat.le_floor
-- 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
h : ⌊a⌋₊ < 1
⊢ a < 1

Tactic:
mod_cast lt_of_floor_lt h

Premises used: congrArg, cast, Nat.lt_of_floor_lt, LT.lt, Eq.symm, 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
a : R
⊢ a < (↑⌊a⌋₊.succ : R)

Tactic:
lt_of_floor_lt <| Nat.lt_succ_self _

Premises used: Nat.lt_succ_self, Nat.lt_of_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 : R
⊢ a < HAdd.hAdd (α := R) (↑⌊a⌋₊ : R) 1

Tactic:
simpa using lt_succ_floor a

Premises used: Nat.lt_succ_floor
-- 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) 0 (↑n : R)
⊢ a ≤ floor.{u_1} (α := R) (↑n : R) ↔ a ≤ n

Tactic:
rw [le_floor_iff, Nat.cast_le]

Premises used: Nat.le_floor_iff, Nat.cast_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
n a : ℕ
⊢ LE.le.{u_1} (α := R) 0 (↑n : R)

Tactic:
n.cast_nonneg

Premises used: Nat.cast_nonneg
-- 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 : ℕ
⊢ LE.le.{u_1} (α := R) 0 (↑n : R)

Tactic:
exact n.cast_nonneg

Premises used: Nat.cast_nonneg
-- 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 : floor.{u_1} (α := R) (↑0 : R) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ floor.{u_1} (α := R) 0 = 0

Tactic:
rw [← Nat.cast_zero, floor_natCast]

Premises used: Nat.floor_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 : floor.{u_1} (α := R) (↑1 : R) = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ floor.{u_1} (α := R) 1 = 1

Tactic:
rw [← Nat.cast_one, floor_natCast]

Premises used: Nat.floor_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
⊢ floor.{u_1} (α := R) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
Nat.floor_natCast _

Premises used: Nat.floor_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
ha : LE.le.{u_1} (α := R) 0 0
⊢ floor.{u_1} (α := R) 0 = 0

Tactic:
floor_zero

Premises used: Nat.floor_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
ha : LE.le.{u_1} (α := R) 0 0
⊢ floor.{u_1} (α := R) 0 = 0

Tactic:
exact floor_zero

Premises used: Nat.floor_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
a b : R
h : a ≤ b
inl : ∀ (ha : a ≤ 0), ⌊a⌋₊ ≤ ⌊b⌋₊
inr : ∀ (ha : 0 ≤ a), ⌊a⌋₊ ≤ ⌊b⌋₊
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

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 b : R
h : a ≤ b
ha : a ≤ 0
inl : 0 ≤ ⌊b⌋₊
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

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 b : R
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊

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 b : R
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊

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 b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
le_floor ((floor_le ha).trans h)

Premises used: Nat.floor_le, Nat.le_floor, 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
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
exact le_floor ((floor_le ha).trans h)

Premises used: Nat.floor_le, Nat.le_floor, 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 b : R
inst_3 : IsStrictOrderedRing R
hab : a ≤ b
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
floor_mono hab

Premises used: Nat.floor_mono
-- 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
hn : n ≠ 0
inl : ∀ (ha : a ≤ 0), n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
inr : ∀ (ha : 0 ≤ a), n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ 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
a : R
n : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
inl : n ≤ 0 ↔ (↑n : R) ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ 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
a : R
n : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ 0 ↔ (↑n : R) ≤ a

Tactic:
iff_of_false (Nat.pos_of_ne_zero hn).not_ge
        (not_le_of_gt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)

Premises used: Iff.mpr, Nat.cast_pos, iff_of_false, Nat.pos_of_ne_zero, not_le_of_gt, LT.lt.not_ge, 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
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ 0 ↔ (↑n : R) ≤ a

Tactic:
exact
      iff_of_false (Nat.pos_of_ne_zero hn).not_ge
        (not_le_of_gt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)

Premises used: Iff.mpr, Nat.cast_pos, iff_of_false, Nat.pos_of_ne_zero, not_le_of_gt, LT.lt.not_ge, 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
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a

Tactic:
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
n : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a

Tactic:
exact 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
n : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ < n ↔ a < (↑n : R)

Tactic:
lt_iff_lt_of_le_iff_le <| le_floor_iff' hn

Premises used: Nat.le_floor_iff', lt_iff_lt_of_le_iff_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
inst_3 : IsStrictOrderedRing 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 [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, cast_one]

Premises used: Nat.le_floor_iff', Nat.one_ne_zero, zero_add, Nat.lt_iff_add_one_le, 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
h : 0 < ⌊a⌋₊
ha : a ≤ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : LT.lt (α := ℕ) 0 0) (ha : a ≤ 0), LT.lt (α := ℕ) 0 0
⊢ LT.lt (α := ℕ) 0 0

Tactic:
rwa [floor_of_nonpos ha] at h

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
a : R
n : ℕ
inst_3 : IsStrictOrderedRing R
h : n < ⌊a⌋₊
⊢ (↑n : R) < a

Tactic:
(Nat.cast_lt.2 h).trans_le <| floor_le (pos_of_floor_pos <| (Nat.zero_le n).trans_lt h).le

Premises used: Nat.pos_of_floor_pos, Iff.mpr, Nat.zero_le, LT.lt.le, LT.lt.trans_le, Nat.floor_le, 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 : R)
⊢ ⌊a⌋₊ ≤ n

Tactic:
le_imp_le_iff_lt_imp_lt.2 lt_of_lt_floor h

Premises used: Iff.mpr, le_imp_le_iff_lt_imp_lt, Nat.lt_of_lt_floor
-- 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
h : a ≤ 1
⊢ ⌊a⌋₊ ≤ 1

Tactic:
floor_le_of_le <| h.trans_eq <| Nat.cast_one.symm

Premises used: LE.le.trans_eq, Nat.floor_le_of_le, 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
rw : ⌊a⌋₊ < 1 ↔ a < (↑1 : R)
⊢ ⌊a⌋₊ = 0 ↔ a < 1

Tactic:
rw [← lt_one_iff, ← @cast_one R]

Premises used: Nat.lt_one_iff, 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
⊢ ⌊a⌋₊ < 1 ↔ a < (↑1 : R)

Tactic:
floor_lt' Nat.one_ne_zero

Premises used: Nat.floor_lt', Nat.one_ne_zero
-- 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
⊢ ⌊a⌋₊ < 1 ↔ a < (↑1 : R)

Tactic:
exact floor_lt' Nat.one_ne_zero

Premises used: Nat.floor_lt', Nat.one_ne_zero
-- 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
hn : n ≠ 0
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
rw₃ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1
rw₄ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
rw₅ : ⌊a⌋₊ ≤ n ∧ n ≤ ⌊a⌋₊ ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
rw₆ rw₇ : n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]

Premises used: Nat.le_floor_iff', Nat.add_one_ne_zero, Nat.lt_add_one_iff, Nat.floor_lt', and_comm, Nat.cast_add, le_antisymm_iff, 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 : ℕ
⊢ ∀ (a : R), a ∈ Ico (↑n : R) (HAdd.hAdd (α := R) (↑n : R) 1) → ⌊a⌋₊ = n

Tactic:
fun _ ⟨h₀, h₁⟩ =>
  (floor_eq_iff <| n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩

Premises used: Iff.mpr, Nat.floor_eq_iff, Nat.cast_nonneg, And.intro, _private.0.Nat.floor_eq_on_Ico.match_1, Nat.floor, LE.le.trans, Eq
-- 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 : R), a ∈ Ico (↑n : R) (HAdd.hAdd (α := R) (↑n : R) 1) → Eq.{u_1 + 1} (α := R) (↑⌊a⌋₊ : R) (↑n : R)

Tactic:
fun x hx => mod_cast floor_eq_on_Ico n x hx

Premises used: cast, Nat.cast_inj._simp_1, Eq.symm, Nat.floor_eq_on_Ico
-- 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
⊢ Eq.{u_1 + 1} (α := Set R) (floor ⁻¹' {0}) (Iio 1)

Tactic:
ext fun _ => floor_eq_zero

Premises used: Set.ext, Nat.floor_eq_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
n : ℕ
hn : n ≠ 0
⊢ floor ⁻¹' {n} = Ico (↑n : R) (HAdd.hAdd (α := R) (↑n : R) 1)

Tactic:
ext fun _ => floor_eq_iff' hn

Premises used: Set.ext, Nat.floor_eq_iff'
-- 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 : ℕ
hn : n ≠ 0
a : R
inl : ∀ (ha : a ≤ 0), ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
inr : ∀ (ha : 0 ≤ a), ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊

Tactic:
rcases le_total a 0 with ha | ha

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
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
inl : 0 / n = 0
inl₁ : a * (↑n : R) ≤ 0
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊

Tactic:
rw [floor_of_nonpos, 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
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ 0 / n = 0

Tactic:
simp
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ a * (↑n : R) ≤ 0

Tactic:
apply mul_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg

Premises used: mul_nonpos_of_nonpos_of_nonneg, Nat.cast_nonneg
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊

Tactic:
eq_of_forall_le_iff fun m ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
inr : ∀ (m : ℕ), m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊

Tactic:
refine eq_of_forall_le_iff fun m ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
inr : m * n ≤ ⌊a * (↑n : R)⌋₊ ↔ m ≤ ⌊a⌋₊
inr₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋₊
inr₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
inr₃ : HMul.hMul (α := R) (↑m : R) (↑n : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
inr₄ inr₅ : (↑m : R) ≤ a ↔ (↑m : R) ≤ a
⊢ m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊

Tactic:
rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]

Premises used: Iff.mpr, mul_nonneg, mul_le_mul_iff_of_pos_right, Nat.cast_nonneg', Nat.le_floor_iff, Nat.zero_lt_of_ne_zero, Nat.cast_mul, Nat.le_div_iff_mul_le, Nat.cast_pos'
-- 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 : ℕ
hn : n ≠ 0
a : R
rw : ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
rw₁ rw₂ : ⌊a⌋₊ = ⌊a⌋₊
⊢ ⌊(↑n : R) * a⌋₊ / n = ⌊a⌋₊

Tactic:
rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]

Premises used: Nat.cast_comm, Nat.mul_cast_floor_div_cancel
-- 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 : ℕ
rw : n + 1 ≤ ⌈a⌉₊ ↔ n < ⌈a⌉₊
rw₁ rw₂ : n < ⌈a⌉₊ ↔ n < ⌈a⌉₊
⊢ n + 1 ≤ ⌈a⌉₊ ↔ (↑n : R) < a

Tactic:
rw [← Nat.lt_ceil, Nat.add_one_le_iff]

Premises used: Nat.add_one_le_iff, 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
rw : HAdd.hAdd (α := ℕ) 0 1 ≤ ⌈a⌉₊ ↔ 0 < a
rw₁ : (↑0 : R) < a ↔ 0 < a
rw₂ rw₃ : 0 < a ↔ 0 < a
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a

Tactic:
rw [← zero_add 1, Nat.add_one_le_ceil_iff, Nat.cast_zero]

Premises used: zero_add, Nat.cast_zero, OfNat.ofNat, Nat.add_one_le_ceil_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
⊢ a ≤ (↑⌈a⌉₊ : R)

Tactic:
ceil_le.1 le_rfl

Premises used: le_rfl, Iff.mp, 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
⊢ Monotone.{u_1, 0} (α := R) ceil

Tactic:
gc_ceil_coe.monotone_l

Premises used: Nat.gc_ceil_coe, GaloisConnection.monotone_l
-- 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
hab : a ≤ b
⊢ ⌈a⌉₊ ≤ ⌈b⌉₊

Tactic:
ceil_mono hab

Premises used: Nat.ceil_mono
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
rw : ⌈a⌉₊ ≤ 0 ↔ a ≤ 0
rw₁ : a ≤ (↑0 : R) ↔ a ≤ 0
rw₂ rw₃ : a ≤ 0 ↔ a ≤ 0
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0

Tactic:
rw [← Nat.le_zero, ceil_le, Nat.cast_zero]

Premises used: Nat.le_zero, Nat.cast_zero, 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
n : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
rw₃ : ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₄ : ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + HAdd.hAdd (α := ℕ) 0 1 ∧ ⌈a⌉₊ ≤ n
rw₅ : ⌈a⌉₊ = n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₆ : ⌈a⌉₊ ≤ n ∧ n ≤ ⌈a⌉₊ ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₇ rw₈ : n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)

Tactic:
rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]

Premises used: not_le, Iff.mpr, Nat.lt_add_one_iff, and_comm, tsub_lt_iff_right, Nat.add_one_le_iff, le_antisymm_iff, pos_iff_ne_zero, 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
⊢ Eq.{u_1 + 1} (α := Set R) (ceil ⁻¹' {0}) (Iic 0)

Tactic:
ext fun _ => ceil_eq_zero

Premises used: Set.ext, Nat.ceil_eq_zero
-- Module: Mathlib.Algebra.Order.Floor.Semiring
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
n : ℕ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Set R) (ceil ⁻¹' {n}) (Ioc (↑(n - 1) : R) (↑n : R))

Tactic:
ext fun _ => ceil_eq_iff hn

Premises used: Set.ext, Nat.ceil_eq_iff
-- 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
rw : a ≤ HAdd.hAdd (α := R) (↑⌊a⌋₊ : R) 1
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

Tactic:
rw [ceil_le, Nat.cast_add, Nat.cast_one]

Premises used: Nat.cast_add, Nat.cast_one, 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
a : R
⊢ a ≤ HAdd.hAdd (α := R) (↑⌊a⌋₊ : R) 1

Tactic:
(lt_floor_add_one a).le

Premises used: LT.lt.le, Nat.lt_floor_add_one