awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
⊢ Monotone.{u_2, 0} (α := R) ceil

Tactic:
gc_ceil_coe.monotone_l

Premises used: Int.gc_ceil_coe, GaloisConnection.monotone_l
-- 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:
ceil_mono hab

Premises used: Int.ceil_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
ha : -1 < a
rwa : HSub.hSub (α := R) (↑0 : R) 1 < a
rwa₁ : HSub.hSub (α := R) 0 1 < a
rwa₂ rwa₃ rwa₄ rwa₅ : -1 < a
⊢ 0 ≤ ⌈a⌉

Tactic:
rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]

Premises used: Int.cast_zero, Int.le_ceil_iff, zero_sub
-- 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 ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
rw₂ : ⌈a⌉ = z ↔ (↑(z - 1) : R) < a ∧ ⌈a⌉ ≤ z
rw₃ : ⌈a⌉ = z ↔ z - 1 < ⌈a⌉ ∧ ⌈a⌉ ≤ z
rw₄ : ⌈a⌉ = z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
rw₅ : ⌈a⌉ ≤ z ∧ z ≤ ⌈a⌉ ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
rw₆ rw₇ : z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)

Tactic:
rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]

Premises used: Int.lt_ceil, Int.cast_sub, and_comm, Int.ceil_le, le_antisymm_iff, Int.cast_one, Int.sub_one_lt_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⌉ = 0 ↔ Membership.mem (γ := Set R) (Ioc (-1) 0) a

Tactic:
simp [ceil_eq_iff]

Premises used: Int.ceil_eq_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 ∈ Ioc (HSub.hSub (α := R) (↑z : R) 1) (↑z : R), ⌈a⌉ = z

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

Premises used: Iff.mpr, Int.ceil_eq_iff, _private.0.Int.ceil_eq_on_Ioc.match_1, And.intro, Int.ceil, Eq
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
m : ℤ
⊢ ceil ⁻¹' {m} = Ioc (HSub.hSub (α := R) (↑m : R) 1) (↑m : R)

Tactic:
ext fun _ => ceil_eq_iff

Premises used: Set.ext, Int.ceil_eq_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
inst_3 : IsOrderedRing R
z : ℤ
rw : z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
rw₁ : z ≤ ⌊-a⌋ ↔ a ≤ (↑(-z) : R)
rw₂ : (↑z : R) ≤ -a ↔ a ≤ (↑(-z) : R)
rw₃ : (↑z : R) ≤ -a ↔ a ≤ -(↑z : R)
rw₄ rw₅ : a ≤ -(↑z : R) ↔ a ≤ -(↑z : R)
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉

Tactic:
rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]

Premises used: Int.cast_neg, le_neg, Int.ceil_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
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
rw₁ : -a ≤ (↑z : R) ↔ -z ≤ ⌊a⌋
rw₂ : -a ≤ (↑z : R) ↔ (↑(-z) : R) ≤ a
rw₃ : -a ≤ (↑z : R) ↔ -(↑z : R) ≤ a
rw₄ rw₅ : -(↑z : R) ≤ a ↔ -(↑z : R) ≤ a
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z

Tactic:
rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]

Premises used: Int.cast_neg, neg_le, Int.ceil_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
z a : ℤ
rw : LE.le.{u_2} (α := R) (↑z : R) (↑a : R) ↔ z ≤ a
rw₁ rw₂ : z ≤ a ↔ z ≤ a
⊢ ceil.{u_2} (α := R) (↑z : R) ≤ a ↔ z ≤ a

Tactic:
rw [ceil_le, Int.cast_le]

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

Tactic:
rw [ceil_le, ← cast_natCast, cast_le]

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

Tactic:
ceil_natCast n

Premises used: Int.ceil_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 : R
z : ℤ
rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
rw₁ : -⌈a + (↑z : R)⌉ = -⌈a⌉ - z
rw₂ : ⌊-(a + (↑z : R))⌋ = -⌈a⌉ - z
rw₃ : ⌊-(a + (↑z : R))⌋ = ⌊-a⌋ - z
rw₄ : ⌊-a - (↑z : R)⌋ = ⌊-a⌋ - z
rw₅ rw₆ : ⌊-a⌋ - z = ⌊-a⌋ - z
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z

Tactic:
rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]

Premises used: Int.floor_neg, neg_add', neg_inj, 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
z : ℤ
a : R
rw : ⌈a + (↑z : R)⌉ = z + ⌈a⌉
rw₁ : ⌈a⌉ + z = z + ⌈a⌉
rw₂ rw₃ : z + ⌈a⌉ = z + ⌈a⌉
⊢ ⌈(↑z : R) + a⌉ = z + ⌈a⌉

Tactic:
rw [add_comm, ceil_add_intCast, add_comm]

Premises used: add_comm, Int.ceil_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, ceil_add_intCast]

Premises used: Int.cast_natCast, Int.ceil_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
n : ℕ
a : R
⊢ ⌈(↑n : R) + a⌉ = (↑n : ℤ) + ⌈a⌉

Tactic:
mod_cast ceil_intCast_add n a

Premises used: Int.cast_natCast, congrArg, cast, Nat.cast, HAdd.hAdd, congrFun', Int.ceil, Eq, Int.ceil_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
a : R
rw : ⌈a + 1⌉ = ⌈a + (↑1 : R)⌉
rw₁ rw₂ : ⌈a + 1⌉ = ⌈a + 1⌉
⊢ ⌈a + 1⌉ = ⌈a⌉ + 1

Tactic:
rw [← ceil_add_intCast a (1 : ℤ), cast_one]

Premises used: Int.ceil_add_intCast, OfNat.ofNat, 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 : R
⊢ ⌈1 + a⌉ = 1 + ⌈a⌉

Tactic:
mod_cast ceil_natCast_add 1 a

Premises used: congrArg, cast, HAdd.hAdd, congr, congrFun', Int.ceil, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans, Int.ceil_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
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n

Tactic:
ceil_add_natCast a n

Premises used: Int.ceil_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 : ℕ
inst_4 : n.AtLeastTwo
a : R
⊢ ⌈OfNat.ofNat n + a⌉ = OfNat.ofNat n + ⌈a⌉

Tactic:
ceil_natCast_add n a

Premises used: Int.ceil_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 : ℕ
⊢ ⌈a - (↑(↑n : ℤ) : R)⌉ = ⌈a⌉ - (↑n : ℤ)

Tactic:
ceil_sub_intCast a n

Premises used: Int.ceil_sub_intCast, Nat.cast
-- 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 : ℕ
h : ⌈a - (↑n : R)⌉ = ⌈a - (↑(↑n : ℤ) : R)⌉
⊢ ⌈a - (↑n : R)⌉ = ⌈a⌉ - (↑n : ℤ)

Tactic:
convert! ceil_sub_intCast a n using 1

Premises used: Int.ceil_sub_intCast, Nat.cast
-- 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 : ℕ
⊢ ⌈a - (↑n : R)⌉ = ⌈a - (↑(↑n : ℤ) : R)⌉

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
rw : ⌈a - 1⌉ + 1 = ⌈a⌉
rw₁ : ⌈a - 1 + 1⌉ = ⌈a⌉
rw₂ rw₃ : ⌈a⌉ = ⌈a⌉
⊢ ⌈a - 1⌉ = ⌈a⌉ - 1

Tactic:
rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]

Premises used: eq_sub_iff_add_eq, Int.ceil_add_one, sub_add_cancel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n

Tactic:
ceil_sub_natCast a n

Premises used: Int.ceil_sub_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 : R
rw : ⌈a⌉ < ⌈a⌉ + 1
⊢ (↑⌈a⌉ : R) < a + 1

Tactic:
rw [← lt_ceil, ← Int.cast_one, ceil_add_intCast]

Premises used: Int.lt_ceil, Int.ceil_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 : R
⊢ ⌈a⌉ < ⌈a⌉ + 1

Tactic:
apply lt_add_one

Premises used: lt_add_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 : a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉ : R) (↑⌈b⌉ : R)
⊢ ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

Tactic:
rw [ceil_le, Int.cast_add]

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

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 ≤ (↑⌈a⌉ : R)

Tactic:
apply le_ceil

Premises used: Int.le_ceil
-- 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 ≤ (↑⌈b⌉ : R)

Tactic:
apply le_ceil

Premises used: Int.le_ceil
-- 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 : (↑⌈b⌉ : R) ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Tactic:
rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]

Premises used: Int.cast_sub, Int.cast_add, Int.ceil_le, le_sub_iff_add_le, Int.cast_one, le_sub_comm
-- 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) ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a

Tactic:
(ceil_lt_add_one _).le.trans ?_

Premises used: LT.lt.le, Int.ceil_lt_add_one, 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 : b + 1 ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a
⊢ (↑⌈b⌉ : R) ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a

Tactic:
refine (ceil_lt_add_one _).le.trans ?_

Premises used: LT.lt.le, Int.ceil_lt_add_one, 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 ≤ (↑⌈a + b⌉ : R)
⊢ b + 1 ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a

Tactic:
rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]

Premises used: add_assoc, le_sub_iff_add_le', add_le_add_iff_right
-- 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 ≤ (↑⌈a + b⌉ : R)

Tactic:
le_ceil _

Premises used: Int.le_ceil
-- 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 ≤ (↑⌈a + b⌉ : R)

Tactic:
exact le_ceil _

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

Tactic:
rw [← cast_zero, ceil_intCast]

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

Tactic:
rw [← cast_one, ceil_intCast]

Premises used: Int.ceil_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
z : ℤ
⊢ ∀ a ∈ Ioc (HSub.hSub (α := R) (↑z : R) 1) (↑z : R), Eq.{u_2 + 1} (α := R) (↑⌈a⌉ : R) (↑z : R)

Tactic:
fun a ha => congrArg Int.cast (ceil_eq_on_Ioc z a ha)

Premises used: Int.cast, congrArg, Int.ceil_eq_on_Ioc
-- 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⌉ : R) = a ↔ Membership.mem (γ := Set R) (range Int.cast) a

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌊a⌋ ≤ ⌈a⌉

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

Premises used: Int.cast_le, Int.le_ceil, Iff.mp, Int.floor_le, 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
h : a < b
⊢ ⌊a⌋ < ⌈b⌉

Tactic:
cast_lt.1 <| (floor_le a).trans_lt <| h.trans_le <| le_ceil b

Premises used: Int.le_ceil, Int.cast_lt, LT.lt.trans_le, Iff.mp, Int.floor_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ range Int.cast

Tactic:
⟨fun h ht => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (h : ⌈a⌉ = ⌊a⌋ + 1) (ht : Membership.mem (γ := Set R) (range Int.cast) a), False
refine_2 : ∀ (h : a ∉ range Int.cast), ⌈a⌉ = ⌊a⌋ + 1
⊢ ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ range Int.cast

Tactic:
refine ⟨fun h ht => ?_, fun h => ?_⟩
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : Membership.mem (γ := Set R) (range Int.cast) a
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑⌈a⌉ : R)

Tactic:
have h0 := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : Membership.mem (γ := Set R) (range Int.cast) a
h0 : Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑⌈a⌉ : R)
⊢ Eq.{u_2 + 1} (α := R) 1 0

Tactic:
rw [h, cast_add, cast_one, left_eq_add] at h0

Premises used: left_eq_add, Int.cast_add, 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 : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : Membership.mem (γ := Set R) (range Int.cast) a
h0 : Eq.{u_2 + 1} (α := R) 1 0
⊢ False

Tactic:
one_ne_zero h0

Premises used: one_ne_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
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : Membership.mem (γ := Set R) (range Int.cast) a
h0 : Eq.{u_2 + 1} (α := R) 1 0
⊢ False

Tactic:
exact one_ne_zero h0

Premises used: one_ne_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
a : R
h : a ∉ range Int.cast
refine_2 : ⌊a⌋ + 1 ≤ ⌈a⌉
⊢ ⌈a⌉ = ⌊a⌋ + 1

Tactic:
apply le_antisymm (Int.ceil_le_floor_add_one _)

Premises used: le_antisymm, Int.ceil_le_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : a ∉ range Int.cast
refine_2 : (↑⌊a⌋ : R) < a
⊢ ⌊a⌋ + 1 ≤ ⌈a⌉

Tactic:
rw [add_one_le_iff, lt_ceil]

Premises used: Int.lt_ceil, Int.add_one_le_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
h : a ∉ range Int.cast
⊢ (↑⌊a⌋ : R) < a

Tactic:
lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

Premises used: Int.floor_eq_self_iff_mem, Iff.mp, Int.floor_le, iff_false_right, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ (↑⌊a⌋ : R) < a

Tactic:
exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

Premises used: Int.floor_eq_self_iff_mem, Iff.mp, Int.floor_le, iff_false_right, lt_of_le_of_ne
-- 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
inl : ∀ (ha : fract a = 0), fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
inr : ∀ (ha : fract a ≠ 0), fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)

Tactic:
rcases eq_or_ne (fract a) 0 with ha | ha

Premises used: Int.fract, eq_or_ne, OfNat.ofNat
-- 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
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)

Tactic:
Or.inl ha

Premises used: Or.inl
-- 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
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- 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
ha : fract a ≠ 0
inr : fract a = a + 1 - (↑⌈a⌉ : R)
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)

Tactic:
right
-- 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
ha : fract a ≠ 0
this : (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
rw : fract a = a + 1 - (a - fract a + 1)
⊢ fract a = a + 1 - (↑⌈a⌉ : R)

Tactic:
rw [this, ← self_sub_fract]

Premises used: Int.self_sub_fract
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
this : (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
⊢ fract a = a + 1 - (a - fract a + 1)

Tactic:
abel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
inr : (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
⊢ fract a = a + 1 - (↑⌈a⌉ : R)

Tactic:
suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
inr : Eq.{u_2 + 1} (α := R) (↑⌈a⌉ : R) (↑(⌊a⌋ + 1) : R)
⊢ (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1

Tactic:
rw [← Int.cast_one, ← Int.cast_add]

Premises used: Int.cast_add, 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 : R
ha : fract a ≠ 0
⊢ a < (↑(⌊a⌋ + 1) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
inr : HSub.hSub (α := R) (↑(⌊a⌋ + 1) : R) 1 < a
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉ : R) (↑(⌊a⌋ + 1) : R)

Tactic:
refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)

Premises used: Iff.mpr, Int.cast, congrArg, Int.ceil_eq_iff, le_of_lt, And.intro
-- 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
ha : fract a ≠ 0
inr : 0 < fract a
⊢ HSub.hSub (α := R) (↑(⌊a⌋ + 1) : R) 1 < a

Tactic:
rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]

Premises used: Int.cast_add, Int.self_sub_fract, sub_lt_self_iff, add_tsub_cancel_right, 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 : R
ha : fract a ≠ 0
⊢ 0 < fract a

Tactic:
ha.symm.lt_of_le (fract_nonneg a)

Premises used: Ne.symm, Int.fract_nonneg, Ne.lt_of_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 : R
ha : fract a ≠ 0
⊢ 0 < fract a

Tactic:
exact ha.symm.lt_of_le (fract_nonneg a)

Premises used: Ne.symm, Int.fract_nonneg, Ne.lt_of_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
ha : fract a ≠ 0
rw : (↑⌈a⌉ : R) = a + 1 - (a + 1 - (↑⌈a⌉ : R))
⊢ (↑⌈a⌉ : R) = a + 1 - fract a

Tactic:
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]

Premises used: Iff.mp, or_iff_right, Int.fract_eq_zero_or_add_one_sub_ceil
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
ha : fract a ≠ 0
⊢ (↑⌈a⌉ : R) = a + 1 - (a + 1 - (↑⌈a⌉ : R))

Tactic:
abel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
ha : fract a ≠ 0
rw : (↑⌈a⌉ : R) - a = 1 - (a + 1 - (↑⌈a⌉ : R))
⊢ (↑⌈a⌉ : R) - a = 1 - fract a

Tactic:
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]

Premises used: Iff.mp, or_iff_right, Int.fract_eq_zero_or_add_one_sub_ceil
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
ha : fract a ≠ 0
⊢ (↑⌈a⌉ : R) - a = 1 - (a + 1 - (↑⌈a⌉ : R))

Tactic:
abel
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : (↑⌈b / (1 - b)⌉ : k) ≤ a
hbc : a < HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1
⊢ b * a < b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : (↑⌈b / (1 - b)⌉ : k) ≤ a
⊢ a < HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1

Tactic:
apply lt_floor_add_one

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : (↑⌈b / (1 - b)⌉ : k) ≤ a
linarith : 1 - b ≤ 0 → b - 1 + (1 - b - 0) = 0
⊢ 0 < 1 - b

Tactic:
linarith