awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rwa : b * (↑⌊a⌋ : k) + b ≤ (↑⌊a⌋ : k)
rwa₁ : b ≤ (↑⌊a⌋ : k) - b * (↑⌊a⌋ : k)
rwa₂ : b ≤ (1 - b) * (↑⌊a⌋ : k)
rwa₃ : b / (1 - b) ≤ (↑⌊a⌋ : k)
rwa₄ : ⌈b / (1 - b)⌉ ≤ ⌊a⌋
rwa₅ rwa₆ rwa₇ rwa₈ : (↑⌈b / (1 - b)⌉ : k) ≤ a
⊢ b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)

Tactic:
rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]

Premises used: one_sub_mul, le_sub_iff_add_le', Int.ceil_le, Int.le_floor, mul_add_one, div_le_iff₀'
-- 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
b₁ : b * a < b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1
b₂ : b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)
⊢ b * a < (↑⌊a⌋ : k)

Tactic:
calc
    b * a < b * (⌊a⌋ + 1) := by gcongr; apply lt_floor_add_one
    _ ≤ ⌊a⌋ := by
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]

Premises used: Int.floor, HAdd.hAdd, OfNat.ofNat
-- 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 : k
ha : 1 ≤ a
inl :
  ∀ (ha : LE.le.{u_4} (α := k) 1 1),
    ⌈HDiv.hDiv (α := k) (↑⌈(HSub.hSub (α := k) 1 1)⁻¹⌉ : k) 1⌉ = ⌈(HSub.hSub (α := k) 1 1)⁻¹⌉
inr : ∀ (ha : 1 < a), ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉
⊢ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
obtain rfl | ha := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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
ha : LE.le.{u_4} (α := k) 1 1
⊢ ⌈HDiv.hDiv (α := k) (↑⌈(HSub.hSub (α := k) 1 1)⁻¹⌉ : k) 1⌉ = ⌈(HSub.hSub (α := k) 1 1)⁻¹⌉

Tactic:
simp
-- 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 : k
ha_1 : 1 ≤ a
ha : 1 < a
linarith : a - 1 ≤ 0 → 1 - a + (a - 1 - 0) = 0
⊢ 0 < a - 1

Tactic:
linarith
-- 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 : k
ha_1 : 1 ≤ a
ha : 1 < a
⊢ 0 < a - 1

Tactic:
have : 0 < a - 1 := by linarith
-- 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 : k
ha_1 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ LE.le.{u_4} (α := k) 0 (↑⌈(a - 1)⁻¹⌉ : k)

Tactic:
positivity
-- 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 : k
ha_1 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
inr : ⌈(a - 1)⁻¹⌉ ≤ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉
⊢ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_

Premises used: Iff.mpr, LT.lt.le, div_le_self, le_antisymm, Int.ceil_le
-- 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 : k
ha_1 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
inr : (↑⌈(a - 1)⁻¹⌉ : k) < 1 / (1 - a⁻¹)
⊢ ⌈(a - 1)⁻¹⌉ ≤ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉

Tactic:
rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
    ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)]

Premises used: Iff.mpr, sub_pos, sub_lt_comm, lt_div_iff₀, mul_one_sub, Int.le_ceil_iff, div_eq_mul_inv, inv_lt_one_of_one_lt₀
-- 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 : k
ha_1 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ (↑⌈(a - 1)⁻¹⌉ : k) < (a - 1)⁻¹ + 1

Tactic:
ceil_lt_add_one (R := k) _

Premises used: Int.ceil_lt_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 : k
ha_1 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
h : 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1
⊢ (↑⌈(a - 1)⁻¹⌉ : k) < 1 / (1 - a⁻¹)

Tactic:
convert! ceil_lt_add_one (R := k) _ using 1

Premises used: Int.ceil_lt_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 : k
ha_1 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1

Tactic:
field
-- 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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
inl : ∀ (hab : a ≤ (b - 1)⁻¹), (↑⌈a⌉ : k) < b * a
inr : ∀ (hba : (b - 1)⁻¹ ≤ a), (↑⌈a⌉ : k) < b * a
⊢ (↑⌈a⌉ : k) < b * a

Tactic:
obtain hab | hba := le_total a (b - 1)⁻¹

Premises used: HSub.hSub, le_total, Inv.inv, OfNat.ofNat
-- 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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hab : a ≤ (b - 1)⁻¹
⊢ LE.le.{u_4} (α := k) (↑⌈a⌉ : k) (↑⌈(b - 1)⁻¹⌉ : k)

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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hab : a ≤ (b - 1)⁻¹
rwa : 0 < b
⊢ (↑⌈(b - 1)⁻¹⌉ : k) < b * a

Tactic:
rwa [← div_lt_iff₀']

Premises used: div_lt_iff₀'
-- 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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b

Tactic:
positivity
-- 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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hab : a ≤ (b - 1)⁻¹
by : LE.le.{u_4} (α := k) (↑⌈a⌉ : k) (↑⌈(b - 1)⁻¹⌉ : k)
by₁ : (↑⌈(b - 1)⁻¹⌉ : k) < b * a
⊢ (↑⌈a⌉ : k) < b * a

Tactic:
calc
      ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity

Premises used: Int.cast, HSub.hSub, Inv.inv, Int.ceil, OfNat.ofNat
-- 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 : 1 < b
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ 0 < b - 1

Tactic:
rw [← sub_pos] at hb

Premises used: sub_pos
-- 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 : 1 < b
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
hb₁ : 0 < b - 1
⊢ (↑⌈(b - 1)⁻¹⌉ : k) / b < a

Tactic:
rw [← sub_pos] at hb

Premises used: sub_pos
-- 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 : 1 < b
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
hb₁ : 0 < b - 1
hba₁ : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
⊢ (b - 1)⁻¹ ≤ a

Tactic:
rw [← sub_pos] at hb

Premises used: sub_pos
-- 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 - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ (↑⌈a⌉ : k) < a + 1

Tactic:
ceil_lt_add_one _

Premises used: Int.ceil_lt_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 - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
rw : b - 1 ≠ 0
⊢ a + 1 = a + (b - 1) * (b - 1)⁻¹

Tactic:
rw [mul_inv_cancel₀]

Premises used: mul_inv_cancel₀
-- 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 - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0

Tactic:
positivity
-- 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 - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
bc : 0 ≤ b - 1
⊢ a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a

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 - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
rw : a + (b * a - a) = b * a
rw₁ rw₂ : b * a = b * a
⊢ a + (b - 1) * a = b * a

Tactic:
rw [sub_one_mul, add_sub_cancel]

Premises used: add_sub_cancel, sub_one_mul
-- 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 - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hba : (b - 1)⁻¹ ≤ a
a₁ : a + 1 = a + (b - 1) * (b - 1)⁻¹
a₂ : a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a
a₃ : a + (b - 1) * a = b * a
⊢ (↑⌈a⌉ : k) < b * a

Tactic:
calc
      ⌈a⌉ < a + 1 := ceil_lt_add_one _
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

Premises used: HSub.hSub, Int.ceil_lt_add_one, OfNat.ofNat
-- 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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b ≤ a
inl :
  ∀ (hba : (↑⌈(b - 1)⁻¹⌉ : k) / b ≤ (↑⌈(b - 1)⁻¹⌉ : k) / b),
    (↑⌈(↑⌈(b - 1)⁻¹⌉ : k) / b⌉ : k) ≤ b * ((↑⌈(b - 1)⁻¹⌉ : k) / b)
inr : ∀ (hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a), (↑⌈a⌉ : k) ≤ b * a
⊢ (↑⌈a⌉ : k) ≤ b * a

Tactic:
obtain rfl | hba := hba.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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
b : k
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b ≤ (↑⌈(b - 1)⁻¹⌉ : k) / b
inl : b ≠ 0
⊢ (↑⌈(↑⌈(b - 1)⁻¹⌉ : k) / b⌉ : k) ≤ b * ((↑⌈(b - 1)⁻¹⌉ : k) / b)

Tactic:
rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]

Premises used: Int.ceil_div_ceil_inv_sub_one, LT.lt.le, mul_div_cancel₀
-- 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
b : k
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b ≤ (↑⌈(b - 1)⁻¹⌉ : k) / b
⊢ b ≠ 0

Tactic:
positivity
-- 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 : 1 < b
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b ≤ a
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
⊢ (↑⌈a⌉ : k) ≤ b * a

Tactic:
(ceil_lt_mul hb hba).le

Premises used: LT.lt.le, Int.ceil_lt_mul
-- 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 : 1 < b
hba_1 : (↑⌈(b - 1)⁻¹⌉ : k) / b ≤ a
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
⊢ (↑⌈a⌉ : k) ≤ b * a

Tactic:
exact (ceil_lt_mul hb hba).le

Premises used: LT.lt.le, Int.ceil_lt_mul
-- 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 : k
ha : 1 ≤ a
rw : 2⁻¹ * a < (↑⌊a⌋ : k)
⊢ a / 2 < (↑⌊a⌋ : k)

Tactic:
rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- 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 : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < (↑⌊a⌋ : k)

Tactic:
mul_lt_floor ?_ ?_ ?_

Premises used: Int.mul_lt_floor
-- 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 : k
ha : 1 ≤ a
refine_1 : LT.lt.{u_4} (α := k) 0 2⁻¹
refine_2 : LT.lt.{u_4} (α := k) 2⁻¹ 1
refine_3 : (↑⌈2⁻¹ / HSub.hSub (α := k) 1 2⁻¹⌉ : k) ≤ a
⊢ 2⁻¹ * a < (↑⌊a⌋ : k)

Tactic:
refine mul_lt_floor ?_ ?_ ?_

Premises used: Int.mul_lt_floor
-- 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 : k
ha : 1 ≤ a
⊢ LT.lt.{u_4} (α := k) 0 2⁻¹

Tactic:
norm_num
-- 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 : k
ha : 1 ≤ a
⊢ LT.lt.{u_4} (α := k) 2⁻¹ 1

Tactic:
norm_num
-- 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 : k
ha refine_3 : 1 ≤ a
⊢ (↑⌈2⁻¹ / HSub.hSub (α := k) 1 2⁻¹⌉ : k) ≤ a

Tactic:
norm_num
-- 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 : k
ha : 1 ≤ a
⊢ 1 ≤ a

Tactic:
assumption
-- 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 : k
ha : 2⁻¹ < a
norm_num : ∀ (ha : 1 / 2 < a), 1 / 2 < a
⊢ HDiv.hDiv (α := k) (↑⌈(HSub.hSub (α := k) 2 1)⁻¹⌉ : k) 2 < a

Tactic:
norm_num at ha ⊢
-- 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 : k
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
ha
-- 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 : k
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
exact ha
-- 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 : k
ha : 2⁻¹ ≤ a
norm_num : ∀ (ha : 1 / 2 ≤ a), 1 / 2 ≤ a
⊢ HDiv.hDiv (α := k) (↑⌈(HSub.hSub (α := k) 2 1)⁻¹⌉ : k) 2 ≤ a

Tactic:
norm_num at ha ⊢
-- 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 : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
ha
-- 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 : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
exact ha
-- 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
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋ ⌈b⌉
⊢ Int.cast ⁻¹' Ioo a b = Ioo ⌊a⌋ ⌈b⌉

Tactic:
ext
-- 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
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋ ⌈b⌉

Tactic:
simp [floor_lt, lt_ceil]

Premises used: Int.lt_ceil, 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 b : R
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉ ⌈b⌉
⊢ Int.cast ⁻¹' Ico a b = Ico ⌈a⌉ ⌈b⌉

Tactic:
ext
-- 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
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉ ⌈b⌉

Tactic:
simp [ceil_le, lt_ceil]

Premises used: Int.lt_ceil, 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
a b : R
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋ ⌊b⌋
⊢ Int.cast ⁻¹' Ioc a b = Ioc ⌊a⌋ ⌊b⌋

Tactic:
ext
-- 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
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋ ⌊b⌋

Tactic:
simp [floor_lt, le_floor]

Premises used: Int.floor_lt, 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 b : R
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉ ⌊b⌋
⊢ Int.cast ⁻¹' Icc a b = Icc ⌈a⌉ ⌊b⌋

Tactic:
ext
-- 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
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉ ⌊b⌋

Tactic:
simp [ceil_le, le_floor]

Premises used: 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
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋
⊢ Int.cast ⁻¹' Ioi a = Ioi ⌊a⌋

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋

Tactic:
simp [floor_lt]

Premises used: 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
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉
⊢ Int.cast ⁻¹' Ici a = Ici ⌈a⌉

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉

Tactic:
simp [ceil_le]

Premises used: 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
a : R
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉
⊢ Int.cast ⁻¹' Iio a = Iio ⌈a⌉

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉

Tactic:
simp [lt_ceil]

Premises used: Int.lt_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
h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋
⊢ Int.cast ⁻¹' Iic a = Iic ⌊a⌋

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
x : ℤ
⊢ x ∈ Int.cast ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋

Tactic:
simp [le_floor]

Premises used: Int.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
a : R
b : S
h : ∀ (n : ℤ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
⊢ ⌊a⌋ = ⌊b⌋

Tactic:
(le_floor.2 <| (h _).1 <| floor_le _).antisymm <| le_floor.2 <| (h _).2 <| floor_le _

Premises used: Iff.mpr, LE.le.antisymm, Int.le_floor, Iff.mp, Int.floor_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
a : R
b : S
h : ∀ (n : ℤ), a ≤ (↑n : R) ↔ b ≤ (↑n : S)
⊢ ⌈a⌉ = ⌈b⌉

Tactic:
(ceil_le.2 <| (h _).2 <| le_ceil _).antisymm <| ceil_le.2 <| (h _).1 <| le_ceil _

Premises used: Iff.mpr, Int.le_ceil, LE.le.antisymm, Int.ceil_le, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℤ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
rw₁ rw₂ : (↑n : R) ≤ a ↔ (↑n : R) ≤ a
⊢ LE.le.{u_3} (α := S) ((↑n : S) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a

Tactic:
rw [← map_intCast f, hf.le_iff_le]

Premises used: map_intCast, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℤ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑n : R) : S) ↔ a ≤ (↑n : R)
rw₁ rw₂ : a ≤ (↑n : R) ↔ a ≤ (↑n : R)
⊢ LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((↑n : S) : S) ↔ a ≤ (↑n : R)

Tactic:
rw [← map_intCast f, hf.le_iff_le]

Premises used: map_intCast, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
simp_rw :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
    (f : (a : R) → S) (a - (↑⌊a⌋ : R))
simp_rw₁ :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
    HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑⌊a⌋ : R) : S)
simp_rw₂ :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
    HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑⌊a⌋ : S) : S)
⊢ Eq.{u_3 + 1} (α := S) (fract ((f : (a : R) → S) a) : S) ((f : (a : R) → S) (fract a) : S)

Tactic:
simp_rw [fract, map_sub, map_intCast, map_floor _ hf]

Premises used: map_sub, Int.fract, map_intCast, Int.map_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 : IsStrictOrderedRing R
a : R
ha : -1 < a
pos : ∀ (h : 0 ≤ a), (↑⌈a⌉₊ : R) < a + 1
neg : ∀ (h : a < 0), (↑⌈a⌉₊ : R) < a + 1
⊢ (↑⌈a⌉₊ : R) < a + 1

Tactic:
by_cases! h : 0 ≤ a
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsStrictOrderedRing R
a : R
ha : -1 < a
h : 0 ≤ a
⊢ (↑⌈a⌉₊ : R) < a + 1

Tactic:
ceil_lt_add_one h

Premises used: Nat.ceil_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 : IsStrictOrderedRing R
a : R
ha : -1 < a
h : 0 ≤ a
⊢ (↑⌈a⌉₊ : R) < a + 1

Tactic:
exact ceil_lt_add_one h

Premises used: Nat.ceil_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 : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
neg : 0 < a + 1
⊢ (↑⌈a⌉₊ : R) < a + 1

Tactic:
rw [ceil_eq_zero.mpr h.le, cast_zero]

Premises used: Iff.mpr, Nat.ceil_eq_zero, LT.lt.le, Nat.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 : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ 0 < a + 1

Tactic:
neg_lt_iff_pos_add.mp ha

Premises used: neg_lt_iff_pos_add, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ 0 < a + 1

Tactic:
exact neg_lt_iff_pos_add.mp ha

Premises used: neg_lt_iff_pos_add, Iff.mp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
rw : (↑⌊a⌋.toNat : ℤ) = ⌊a⌋
rw₁ rw₂ : ⌊a⌋ = ⌊a⌋
⊢ (↑⌊a⌋₊ : ℤ) = ⌊a⌋

Tactic:
rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]

Premises used: Iff.mpr, Int.toNat_of_nonneg, Int.floor_nonneg, Int.floor_toNat
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
rw : (↑⌈a⌉.toNat : ℤ) = ⌈a⌉
rw₁ rw₂ : ⌈a⌉ = ⌈a⌉
⊢ (↑⌈a⌉₊ : ℤ) = ⌈a⌉

Tactic:
rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]

Premises used: Int.toNat_of_nonneg, Int.ceil_nonneg, Int.ceil_toNat