awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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 _)
⊢ { floor := floor, ceil := ceil, gc_coe_floor := gc_coe_floor, gc_ceil_coe := gc_ceil_coe : FloorRing R } = H₂
have 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 }
Tactic: cases H₂
Cleared hypotheses: H₂, this_1, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a : K
n : ℕ
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n
have inl : ⌊a / (↑0 : K)⌋₊ = ⌊a⌋₊ / 0
Tactic: obtain rfl | hn := n.eq_zero_or_pos
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n
have inr : ∀ (hn : n > 0), ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n
Tactic: obtain rfl | hn := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a⌋₊ / n
have inr : ⌊a / (↑n : K)⌋₊ = ⌊a / (↑n : K) * (↑n : K)⌋₊ / n
Tactic: nth_rw 2 [← div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ ⌊a / (↑n : K)⌋₊ = ⌊a / (↑n : K) * (↑n : K)⌋₊ / n
have inr : ⌊a / (↑n : K)⌋₊ = ⌊a / (↑n : K)⌋₊
Tactic: rw [mul_cast_floor_div_cancel (Nat.ne_zero_of_lt hn)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)⌋₊ = m / n
have h : m = floor.{u_2} (α := K) (↑m : K)
Tactic: convert! floor_div_natCast (m : K) n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
Goal:
K : Type u_2
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
m n : ℕ
⊢ m = floor.{u_2} (α := K) (↑m : K)
have h : m = m
Tactic: rw [m.floor_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 * a < b * HAdd.hAdd (α := K) (↑⌊a⌋₊ : K) 1
have hbc : a < HAdd.hAdd (α := K) (↑⌊a⌋₊ : K) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ 0 < 1 - b
have linarith : 1 - b ≤ 0 → b - 1 + (1 - b - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 * HAdd.hAdd (α := K) (↑⌊a⌋₊ : K) 1 ≤ (↑⌊a⌋₊ : K)
have rw : ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊
Tactic: rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 * a < (↑⌊a⌋₊ : K)
have b₁ : b * a < b * HAdd.hAdd (α := K) (↑⌊a⌋₊ : K) 1
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
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 * a < (↑⌊a⌋₊ : K)
have b₂ : b * HAdd.hAdd (α := K) (↑⌊a⌋₊ : K) 1 ≤ (↑⌊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
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ (↑⌈a⌉₊ : K) < b * a
have inl : ∀ (hab : a ≤ (b - 1)⁻¹), (↑⌈a⌉₊ : K) < b * a
Tactic: obtain hab | hba := le_total a (b - 1)⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ (↑⌈a⌉₊ : K) < b * a
have inr : ∀ (hba : (b - 1)⁻¹ ≤ a), (↑⌈a⌉₊ : K) < b * a
Tactic: obtain hab | hba := le_total a (b - 1)⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)⁻¹
⊢ (↑⌈(b - 1)⁻¹⌉₊ : K) < b * a
have rwa : 0 < b
Tactic: rwa [← div_lt_iff₀']
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)⁻¹
⊢ (↑⌈a⌉₊ : K) < b * a
have by : LE.le.{u_2} (α := K) (↑⌈a⌉₊ : K) (↑⌈(b - 1)⁻¹⌉₊ : K)
Tactic: calc
      ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : K) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)
⊢ (↑⌈a⌉₊ : K) < b * a
have by₁ : (↑⌈(b - 1)⁻¹⌉₊ : K) < b * a
Tactic: calc
      ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : K) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (hypothesis)
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
⊢ (↑⌈a⌉₊ : K) < b * a
have hb₁ : 0 < b - 1
Tactic: rw [← sub_pos] at hb
Cleared hypotheses: hb, hba_1, hba
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 + 1 = a + (b - 1) * (b - 1)⁻¹
have rw : b - 1 ≠ 0
Tactic: rw [mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a
have bc : 0 ≤ b - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 + (b - 1) * a = b * a
have rw : a + (b * a - a) = b * a
Tactic: rw [sub_one_mul, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ a + (b - 1) * a = b * a
have rw₁ : b * a = b * a
Tactic: rw [sub_one_mul, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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⌉₊ : K) < b * a
have a₁ : a + 1 = a + (b - 1) * (b - 1)⁻¹
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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⌉₊ : K) < b * a
have a₂ : a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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⌉₊ : K) < b * a
have a₃ : a + (b - 1) * a = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ (↑⌈a⌉₊ : K) ≤ b * a
have inl : ∀ (hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K) / b),
  (↑⌈(↑⌈(b - 1)⁻¹⌉₊ : K) / b⌉₊ : K) ≤ b * ((↑⌈(b - 1)⁻¹⌉₊ : K) / b)
Tactic: obtain rfl | hba := hba.eq_or_lt
Cleared hypotheses: a, hba
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)
⊢ (↑⌈a⌉₊ : K) ≤ b * a
have inr : ∀ (hba : (↑⌈(b - 1)⁻¹⌉₊ : K) / b < a), (↑⌈a⌉₊ : K) ≤ b * a
Tactic: obtain rfl | hba := hba.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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⌉₊ : K) ≤ b * ((↑⌈(b - 1)⁻¹⌉₊ : K) / b)
have inl : (↑⌈(b - 1)⁻¹⌉₊ : K) / b ≤ (↑⌈(b - 1)⁻¹⌉₊ : K)
Tactic: rw [mul_div_cancel₀, cast_le, ceil_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)
⊢ (↑⌈(↑⌈(b - 1)⁻¹⌉₊ : K) / b⌉₊ : K) ≤ b * ((↑⌈(b - 1)⁻¹⌉₊ : K) / b)
have inl₁ : b ≠ 0
Tactic: rw [mul_div_cancel₀, cast_le, ceil_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ a / 2 < (↑⌊a⌋₊ : K)
have rw : 2⁻¹ * a < (↑⌊a⌋₊ : K)
Tactic: rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)
have refine_1 : LT.lt.{u_2} (α := K) 0 2⁻¹
Tactic: refine mul_lt_floor ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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⁻¹
⊢ 2⁻¹ * a < (↑⌊a⌋₊ : K)
have refine_2 : LT.lt.{u_2} (α := K) 2⁻¹ 1
Tactic: refine mul_lt_floor ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ 2⁻¹ * a < (↑⌊a⌋₊ : K)
have refine_3 : (↑⌈2⁻¹ / HSub.hSub (α := K) 1 2⁻¹⌉₊ : K) ≤ a
Tactic: refine mul_lt_floor ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ HDiv.hDiv (α := K) (↑⌈(HSub.hSub (α := K) 2 1)⁻¹⌉₊ : K) 2 < a
have norm_num : ∀ (ha : 1 / 2 < a), 1 / 2 < a
Tactic: norm_num at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ HDiv.hDiv (α := K) (↑⌈(HSub.hSub (α := K) 2 1)⁻¹⌉₊ : K) 2 ≤ a
have norm_num : ∀ (ha : 1 / 2 ≤ a), 1 / 2 ≤ a
Tactic: norm_num at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ IsNat ⌊r⌋₊ res
have out : ⌊r⌋₊ = (↑res : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ ⌊r⌋₊ = (↑res : ℕ)
have out : ⌊r⌋₊ = (↑(n / d) : ℕ)
Tactic: rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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) : ℕ)
⊢ ⌊r⌋₊ = (↑res : ℕ)
have out₁ : ⌊HDiv.hDiv (α := R) (↑n : R) (↑d : R)⌋₊ = (↑(n / d) : ℕ)
Tactic: rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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) : ℕ)
⊢ ⌊r⌋₊ = (↑res : ℕ)
have out₂ : n / d = (↑(n / d) : ℕ)
Tactic: rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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) : ℕ)
⊢ ⌊r⌋₊ = (↑res : ℕ)
have out₃ : n / d = n / d
Tactic: rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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
⊢ IsNat ⌊r⌋₊ 0
have rcases : ∀ (hd : Invertible (α := R) (↑d : R)),
  IsNat
    ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊
    0
Tactic: rcases h with ⟨hd, rfl⟩
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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)
⊢ IsNat
    ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊
    0
have out : ⌊HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)⌋₊ =
  (↑0 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semifield (goal)
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 : ℕ)
have out : HMul.hMul (α := R) (↑(Int.negOfNat n) : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _) < 1
Tactic: rw [Nat.cast_zero, Nat.floor_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a < (↑1 : R) ↔ a < 1
have rw : a < 1 ↔ a < 1
Tactic: rw [Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw : ⌊a⌋₊ = n ↔ n ≤ ⌊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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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)
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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)
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw₃ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw₄ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw₅ : ⌊a⌋₊ ≤ n ∧ n ≤ ⌊a⌋₊ ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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
⊢ ⌊a⌋₊ = n ↔ (↑n : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
have rw₆ : n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
n a : ℕ
⊢ a ≤ floor.{u_1} (α := R) (↑n : R) ↔ a ≤ n
have rw : LE.le.{u_1} (α := R) 0 (↑n : R)
Tactic: rw [le_floor_iff, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
⊢ floor.{u_1} (α := R) 0 = 0
have rw : floor.{u_1} (α := R) (↑0 : R) = 0
Tactic: rw [← Nat.cast_zero, floor_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
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
⊢ floor.{u_1} (α := R) 0 = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← Nat.cast_zero, floor_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
⊢ floor.{u_1} (α := R) 1 = 1
have rw : floor.{u_1} (α := R) (↑1 : R) = 1
Tactic: rw [← Nat.cast_one, floor_natCast]