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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : -1 < a
rw : (↑⌈a⌉.toNat : ℤ) = ⌈a⌉
rw₁ rw₂ : ⌈a⌉ = ⌈a⌉
⊢ (↑⌈a⌉₊ : ℤ) = ⌈a⌉

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

Premises used: Int.toNat_of_nonneg, Int.ceil_nonneg_of_neg_one_lt, Int.ceil_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 : Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑(↑⌊a⌋₊ : ℤ) : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑⌊a⌋₊ : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑⌊a⌋ : R)

Tactic:
rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.natCast_floor_eq_floor
-- 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 : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑(↑⌈a⌉₊ : ℤ) : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉₊ : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉ : R)

Tactic:
rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.natCast_ceil_eq_ceil
-- 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 : -1 < a
rw : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑(↑⌈a⌉₊ : ℤ) : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉₊ : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉ : R)

Tactic:
rw [← Int.natCast_ceil_eq_ceil_of_neg_one_lt ha, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.natCast_ceil_eq_ceil_of_neg_one_lt
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
⊢ Subsingleton.{u_4 + 1} (FloorRing R)

Tactic:
⟨fun H₁ H₂ => ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
refine : ∀ (H₁ H₂ : FloorRing R), H₁ = H₂
⊢ Subsingleton.{u_4 + 1} (FloorRing R)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₁ H₂ : FloorRing R
⊢ Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)

Tactic:
have : H₁.floor = H₂.floor :=
    funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₁ H₂ : FloorRing R
this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
⊢ Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)

Tactic:
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₁ H₂ : FloorRing R
this_1 : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)
mk :
  ∀ (floor ceil : R → ℤ) (gc_coe_floor : GaloisConnection Int.cast floor) (gc_ceil_coe : GaloisConnection ceil Int.cast)
    (this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _))
    (this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)),
    { floor := floor, ceil := ceil, gc_coe_floor := gc_coe_floor, gc_ceil_coe := gc_ceil_coe : FloorRing R } = H₂
⊢ H₁ = H₂

Tactic:
cases H₁
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₂ : FloorRing R
floor ceil : R → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
gc_ceil_coe : GaloisConnection ceil Int.cast
this_1 : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)
mk :
  ∀ (floor_1 ceil_1 : R → ℤ) (gc_coe_floor_1 : GaloisConnection Int.cast floor_1)
    (gc_ceil_coe_1 : GaloisConnection ceil_1 Int.cast)
    (this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _))
    (this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)),
    { floor := floor, ceil := ceil, gc_coe_floor := gc_coe_floor, gc_ceil_coe := gc_ceil_coe : FloorRing R } =
      { floor := floor_1, ceil := ceil_1, gc_coe_floor := gc_coe_floor_1, gc_ceil_coe := gc_ceil_coe_1 }
⊢ { floor := floor, ceil := ceil, gc_coe_floor := gc_coe_floor, gc_ceil_coe := gc_ceil_coe : FloorRing R } = H₂

Tactic:
cases H₂
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
floor ceil : R → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
gc_ceil_coe : GaloisConnection ceil Int.cast
floor_1 ceil_1 : R → ℤ
gc_coe_floor_1 : GaloisConnection Int.cast floor_1
gc_ceil_coe_1 : GaloisConnection ceil_1 Int.cast
this_1 : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)
⊢ { floor := floor, ceil := ceil, gc_coe_floor := gc_coe_floor, gc_ceil_coe := gc_ceil_coe : FloorRing R } =
    { floor := floor_1, ceil := ceil_1, gc_coe_floor := gc_coe_floor_1, gc_ceil_coe := gc_ceil_coe_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
n : ℕ
inl : ⌊a / (↑0 : K)⌋₊ = ⌊a⌋₊ / 0
inr : ∀ (hn : n > 0), ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
⊢ ⌊a / (↑0 : K)⌋₊ = ⌊a⌋₊ / 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
n : ℕ
hn : n > 0
⊢ Ne.{u_2 + 1} (α := K) (↑n : K) 0

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
n : ℕ
hn : n > 0
inr : ⌊a / (↑n : K)⌋₊ = ⌊a / (↑n : K) * (↑n : K)⌋₊ / n
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n

Tactic:
nth_rw 2 [← div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)]

Premises used: div_mul_cancel₀
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
n : ℕ
hn : n > 0
inr inr₁ : ⌊a / (↑n : K)⌋₊ = ⌊a / (↑n : K)⌋₊
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a / (↑n : K) * (↑n : K)⌋₊ / n

Tactic:
rw [mul_cast_floor_div_cancel (Nat.ne_zero_of_lt hn)]

Premises used: Nat.ne_zero_of_lt, Nat.mul_cast_floor_div_cancel
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
n : ℕ
inst_4 : n.AtLeastTwo
⊢ ⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n

Tactic:
floor_div_natCast a n

Premises used: Nat.floor_div_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
m n : ℕ
⊢ ⌊HDiv.hDiv (α := K) (↑m : K) (↑n : K)⌋₊ = floor.{u_2} (α := K) (↑m : K) / n

Tactic:
floor_div_natCast (m : K) n

Premises used: Nat.floor_div_natCast, Nat.cast
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
m n : ℕ
h : m = floor.{u_2} (α := K) (↑m : K)
⊢ ⌊HDiv.hDiv (α := K) (↑m : K) (↑n : K)⌋₊ = m / n

Tactic:
convert! floor_div_natCast (m : K) n

Premises used: Nat.floor_div_natCast, Nat.cast
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
m n : ℕ
h h₁ : m = m
⊢ m = floor.{u_2} (α := K) (↑m : K)

Tactic:
rw [m.floor_natCast]

Premises used: Nat.floor_natCast
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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: Nat.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : (↑⌈b / (1 - b)⌉₊ : K) ≤ a
rw : ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊
⊢ b * HAdd.hAdd (α := K) (↑⌊a⌋₊ : K) 1 ≤ (↑⌊a⌋₊ : K)

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

Premises used: one_sub_mul, le_sub_iff_add_le', mul_add_one, div_le_iff₀', Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : (↑⌈b / (1 - b)⌉₊ : K) ≤ a
⊢ ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊

Tactic:
le_floor hba

Premises used: Nat.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : (↑⌈b / (1 - b)⌉₊ : K) ≤ a
⊢ ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊

Tactic:
exact le_floor hba

Premises used: Nat.le_floor
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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
      rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le]
      exact le_floor hba

Premises used: HAdd.hAdd, Nat.floor, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a b : K
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b < a
hab : a ≤ (b - 1)⁻¹
⊢ LE.le.{u_2} (α := K) (↑⌈a⌉₊ : K) (↑⌈(b - 1)⁻¹⌉₊ : K)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a b : K
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b < a
hab : a ≤ (b - 1)⁻¹
by : LE.le.{u_2} (α := 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: HSub.hSub, Nat.cast, Inv.inv, Nat.ceil, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a b : K
hb : 0 < b - 1
hba_1 : (↑⌈(b - 1)⁻¹⌉₊ : K) / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ 0 ≤ (b - 1)⁻¹

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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 <| hba.trans' <| by positivity
      _ = 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, Nat.ceil_lt_add_one, OfNat.ofNat, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
b : K
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K) / b
inl : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K)
inl₁ : b ≠ 0
⊢ (↑⌈(↑⌈(b - 1)⁻¹⌉₊ : K) / b⌉₊ : K) ≤ b * ((↑⌈(b - 1)⁻¹⌉₊ : K) / b)

Tactic:
rw [mul_div_cancel₀, cast_le, ceil_le]

Premises used: mul_div_cancel₀, Nat.cast_le, Nat.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
b : K
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K) / b
⊢ LE.le.{u_2} (α := K) 0 (↑⌈(b - 1)⁻¹⌉₊ : K)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
b : K
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K) / b
⊢ (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K)

Tactic:
exact _root_.div_le_self (by positivity) hb.le

Premises used: LT.lt.le, div_le_self
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
b : K
hb : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K) / b
⊢ b ≠ 0

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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, Nat.ceil_lt_mul
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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, Nat.ceil_lt_mul
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ * a < (↑⌊a⌋₊ : K)

Tactic:
mul_lt_floor ?_ ?_ ?_

Premises used: Nat.mul_lt_floor
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 ≤ a
refine_1 : LT.lt.{u_2} (α := K) 0 2⁻¹
refine_2 : LT.lt.{u_2} (α := K) 2⁻¹ 1
refine_3 : (↑⌈2⁻¹ / HSub.hSub (α := K) 1 2⁻¹⌉₊ : K) ≤ a
⊢ 2⁻¹ * a < (↑⌊a⌋₊ : K)

Tactic:
refine mul_lt_floor ?_ ?_ ?_

Premises used: Nat.mul_lt_floor
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ LT.lt.{u_2} (α := K) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ LT.lt.{u_2} (α := K) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha refine_3 : 1 ≤ a
⊢ (↑⌈2⁻¹ / HSub.hSub (α := K) 1 2⁻¹⌉₊ : K) ≤ a

Tactic:
norm_num
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 1 ≤ a

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
ha
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
exact ha
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring 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.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
ha
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : FloorSemiring K
a : K
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
exact ha
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ Nat.floor.{u_3} (α := R) (↑m : R) = (↑m : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ IsNat (Nat.floor.{u_3} (α := R) (↑m : R)) m

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ LE.le.{u_3} (α := R) (↑(Int.negOfNat m) : R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ IsNat (Nat.floor.{u_3} (α := R) (↑(Int.negOfNat m) : R)) 0

Tactic:
exact ⟨Nat.floor_of_nonpos <| by simp⟩
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : n / d = res
out : ⌊r⌋₊ = (↑res : ℕ)
⊢ IsNat ⌊r⌋₊ res

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Floor.Semifield
Goal:
R : Type u_3
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : n / d = res
out : ⌊r⌋₊ = (↑(n / d) : ℕ)
out₁ : ⌊HDiv.hDiv (α := R) (↑n : R) (↑d : R)⌋₊ = (↑(n / d) : ℕ)
out₂ : n / d = (↑(n / d) : ℕ)
out₃ out₄ : n / d = n / d
⊢ ⌊r⌋₊ = (↑res : ℕ)

Tactic:
rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]

Premises used: Nat.cast_id, Nat.floor_div_eq_div, Mathlib.Meta.NormNum.IsNNRat.to_eq, rfl