awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (↑1 : R) = 1
⊢ floor.{u_1} (α := R) 1 = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← Nat.cast_one, 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
a b : R
h : a ≤ b
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
have inl : ∀ (ha : a ≤ 0), ⌊a⌋₊ ≤ ⌊b⌋₊
Tactic: obtain ha | ha := le_total a 0
-- 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
a b : R
h : a ≤ b
inl : ∀ (ha : a ≤ 0), ⌊a⌋₊ ≤ ⌊b⌋₊
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
have inr : ∀ (ha : 0 ≤ a), ⌊a⌋₊ ≤ ⌊b⌋₊
Tactic: obtain ha | ha := le_total a 0
-- 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
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
have inl : 0 ≤ ⌊b⌋₊
Tactic: rw [floor_of_nonpos ha]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
have inl : ∀ (ha : a ≤ 0), n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
Tactic: obtain ha | ha := le_total a 0
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
inl : ∀ (ha : a ≤ 0), n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
have inr : ∀ (ha : 0 ≤ a), n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
Tactic: obtain ha | ha := le_total a 0
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ (↑n : R) ≤ a
have inl : n ≤ 0 ↔ (↑n : R) ≤ a
Tactic: rw [floor_of_nonpos ha]
-- 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
inst_3 : IsStrictOrderedRing R
⊢ 0 < ⌊a⌋₊ ↔ 1 ≤ a
have rw : HAdd.hAdd (α := ℕ) 0 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a
Tactic: rw [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, 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
inst_3 : IsStrictOrderedRing R
rw : HAdd.hAdd (α := ℕ) 0 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a
rw₁ : 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a
⊢ 0 < ⌊a⌋₊ ↔ 1 ≤ a
have rw₂ : (↑1 : R) ≤ a ↔ 1 ≤ a
Tactic: rw [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, 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
inst_3 : IsStrictOrderedRing R
rw : HAdd.hAdd (α := ℕ) 0 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a
rw₁ : 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a
rw₂ : (↑1 : R) ≤ a ↔ 1 ≤ a
⊢ 0 < ⌊a⌋₊ ↔ 1 ≤ a
have rw₃ : 1 ≤ a ↔ 1 ≤ a
Tactic: rw [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, 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
inst_3 : IsStrictOrderedRing R
h : 0 < ⌊a⌋₊
ha : a ≤ 0
⊢ LT.lt (α := ℕ) 0 0
have rwa : ∀ (h : LT.lt (α := ℕ) 0 0) (ha : a ≤ 0), LT.lt (α := ℕ) 0 0
Tactic: rwa [floor_of_nonpos ha] at h
Cleared hypotheses: h, ha
-- 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
inst_3 : IsStrictOrderedRing R
⊢ ⌊a⌋₊ = 0 ↔ a < 1
have rw : ⌊a⌋₊ < 1 ↔ a < (↑1 : R)
Tactic: rw [← lt_one_iff, ← @cast_one R]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
⊢ ⌊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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
⊢ ⌊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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
rw₃ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1
⊢ ⌊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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
rw₃ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1
rw₄ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
⊢ ⌊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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
inst_3 : IsStrictOrderedRing R
hn : n ≠ 0
rw : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) 1
rw₁ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < HAdd.hAdd (α := R) (↑n : R) (↑1 : R)
rw₂ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < (↑(n + 1) : R)
rw₃ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1
rw₄ : ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
rw₅ : ⌊a⌋₊ ≤ n ∧ n ≤ ⌊a⌋₊ ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
⊢ ⌊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' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
have inl : ∀ (ha : a ≤ 0), ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
Tactic: rcases le_total a 0 with ha | ha
-- 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 : ℕ
hn : n ≠ 0
a : R
inl : ∀ (ha : a ≤ 0), ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
have inr : ∀ (ha : 0 ≤ a), ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
Tactic: rcases le_total a 0 with ha | ha
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
have inl : 0 / n = 0
Tactic: rw [floor_of_nonpos, floor_of_nonpos ha]
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
inl : 0 / n = 0
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
have inl₁ : a * (↑n : R) ≤ 0
Tactic: rw [floor_of_nonpos, floor_of_nonpos ha]
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
⊢ ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
have inr : ∀ (m : ℕ), m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
Tactic: refine eq_of_forall_le_iff fun m ↦ ?_
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
⊢ m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
have inr : m * n ≤ ⌊a * (↑n : R)⌋₊ ↔ m ≤ ⌊a⌋₊
Tactic: rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
inr : m * n ≤ ⌊a * (↑n : R)⌋₊ ↔ m ≤ ⌊a⌋₊
⊢ m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
have inr₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋₊
Tactic: rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
inr : m * n ≤ ⌊a * (↑n : R)⌋₊ ↔ m ≤ ⌊a⌋₊
inr₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋₊
⊢ m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
have inr₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
Tactic: rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
inr : m * n ≤ ⌊a * (↑n : R)⌋₊ ↔ m ≤ ⌊a⌋₊
inr₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋₊
inr₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
⊢ m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
have inr₃ : HMul.hMul (α := R) (↑m : R) (↑n : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
Tactic: rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]
-- 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 : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
inr : m * n ≤ ⌊a * (↑n : R)⌋₊ ↔ m ≤ ⌊a⌋₊
inr₁ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ m ≤ ⌊a⌋₊
inr₂ : (↑(m * n) : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
inr₃ : HMul.hMul (α := R) (↑m : R) (↑n : R) ≤ a * (↑n : R) ↔ (↑m : R) ≤ a
⊢ m ≤ ⌊a * (↑n : R)⌋₊ / n ↔ m ≤ ⌊a⌋₊
have inr₄ : (↑m : R) ≤ a ↔ (↑m : R) ≤ a
Tactic: rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]
-- 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 : ℕ
hn : n ≠ 0
a : R
⊢ ⌊(↑n : R) * a⌋₊ / n = ⌊a⌋₊
have rw : ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
Tactic: rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]
-- 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 : ℕ
hn : n ≠ 0
a : R
rw : ⌊a * (↑n : R)⌋₊ / n = ⌊a⌋₊
⊢ ⌊(↑n : R) * a⌋₊ / n = ⌊a⌋₊
have rw₁ : ⌊a⌋₊ = ⌊a⌋₊
Tactic: rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]
-- 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 : ℕ
⊢ n + 1 ≤ ⌈a⌉₊ ↔ (↑n : R) < a
have rw : n + 1 ≤ ⌈a⌉₊ ↔ n < ⌈a⌉₊
Tactic: rw [← Nat.lt_ceil, Nat.add_one_le_iff]
-- 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 : ℕ
rw : n + 1 ≤ ⌈a⌉₊ ↔ n < ⌈a⌉₊
⊢ n + 1 ≤ ⌈a⌉₊ ↔ (↑n : R) < a
have rw₁ : n < ⌈a⌉₊ ↔ n < ⌈a⌉₊
Tactic: rw [← Nat.lt_ceil, Nat.add_one_le_iff]
-- 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
rw : HAdd.hAdd (α := ℕ) 0 1 ≤ ⌈a⌉₊ ↔ 0 < a
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a
have rw₁ : (↑0 : R) < a ↔ 0 < a
Tactic: rw [← zero_add 1, Nat.add_one_le_ceil_iff, Nat.cast_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
rw : HAdd.hAdd (α := ℕ) 0 1 ≤ ⌈a⌉₊ ↔ 0 < a
rw₁ : (↑0 : R) < a ↔ 0 < a
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a
have rw₂ : 0 < a ↔ 0 < a
Tactic: rw [← zero_add 1, Nat.add_one_le_ceil_iff, Nat.cast_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
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0
have rw : ⌈a⌉₊ ≤ 0 ↔ a ≤ 0
Tactic: rw [← Nat.le_zero, ceil_le, Nat.cast_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
rw : ⌈a⌉₊ ≤ 0 ↔ a ≤ 0
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0
have rw₁ : a ≤ (↑0 : R) ↔ a ≤ 0
Tactic: rw [← Nat.le_zero, ceil_le, Nat.cast_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
rw : ⌈a⌉₊ ≤ 0 ↔ a ≤ 0
rw₁ : a ≤ (↑0 : R) ↔ a ≤ 0
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0
have rw₂ : a ≤ 0 ↔ a ≤ 0
Tactic: rw [← Nat.le_zero, ceil_le, Nat.cast_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
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₃ : ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
rw₃ : ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₄ : ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + HAdd.hAdd (α := ℕ) 0 1 ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
rw₃ : ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₄ : ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + HAdd.hAdd (α := ℕ) 0 1 ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₅ : ⌈a⌉₊ = n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
rw₃ : ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₄ : ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + HAdd.hAdd (α := ℕ) 0 1 ∧ ⌈a⌉₊ ≤ n
rw₅ : ⌈a⌉₊ = n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₆ : ⌈a⌉₊ ≤ n ∧ n ≤ ⌈a⌉₊ ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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 : ℕ
hn : n ≠ 0
rw : ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ ⌈a⌉₊ ≤ n
rw₁ : ⌈a⌉₊ = n ↔ ¬a ≤ (↑(n - 1) : R) ∧ ⌈a⌉₊ ≤ n
rw₂ : ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
rw₃ : ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₄ : ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + HAdd.hAdd (α := ℕ) 0 1 ∧ ⌈a⌉₊ ≤ n
rw₅ : ⌈a⌉₊ = n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
rw₆ : ⌈a⌉₊ ≤ n ∧ n ≤ ⌈a⌉₊ ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
⊢ ⌈a⌉₊ = n ↔ (↑(n - 1) : R) < a ∧ a ≤ (↑n : R)
have rw₇ : n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
Tactic: rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
-- 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
a : R
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1
have rw : a ≤ HAdd.hAdd (α := R) (↑⌊a⌋₊ : R) 1
Tactic: rw [ceil_le, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : FloorSemiring R
z : ℤ
a : ℕ
⊢ ceil.{u_3} (α := R) (↑z : R) ≤ a ↔ z.toNat ≤ a
have simp : LE.le.{u_3} (α := R) (↑z : R) (↑a : R) ↔ z ≤ (↑a : ℤ)
Tactic: simp only [ceil_le, Int.toNat_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : FloorSemiring R
z : ℤ
a : ℕ
⊢ LE.le.{u_3} (α := R) (↑z : R) (↑a : R) ↔ z ≤ (↑a : ℤ)
have norm_cast : z ≤ (↑a : ℤ) ↔ z ≤ (↑a : ℤ)
Tactic: norm_cast
-- 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 : ℕ
⊢ ceil.{u_1} (α := R) (↑n : R) ≤ a ↔ n ≤ a
have rw : LE.le.{u_1} (α := R) (↑n : R) (↑a : R) ↔ n ≤ a
Tactic: rw [ceil_le, 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
n a : ℕ
rw : LE.le.{u_1} (α := R) (↑n : R) (↑a : R) ↔ n ≤ a
⊢ ceil.{u_1} (α := R) (↑n : R) ≤ a ↔ n ≤ a
have rw₁ : n ≤ a ↔ n ≤ a
Tactic: rw [ceil_le, 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
⊢ ceil.{u_1} (α := R) 0 = 0
have rw : ceil.{u_1} (α := R) (↑0 : R) = 0
Tactic: rw [← Nat.cast_zero, ceil_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 : ceil.{u_1} (α := R) (↑0 : R) = 0
⊢ ceil.{u_1} (α := R) 0 = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← Nat.cast_zero, ceil_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
⊢ ceil.{u_1} (α := R) 1 = 1
have rw : ceil.{u_1} (α := R) (↑1 : R) = 1
Tactic: rw [← Nat.cast_one, ceil_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 : ceil.{u_1} (α := R) (↑1 : R) = 1
⊢ ceil.{u_1} (α := R) 1 = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← Nat.cast_one, ceil_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
a : R
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
have inl : ∀ (ha : a ≤ 0), ⌊a⌋₊ ≤ ⌈a⌉₊
Tactic: obtain ha | ha := le_total a 0