awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
rw₁ : -a ≤ (↑z : R) ↔ -z ≤ ⌊a⌋
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
have rw₂ : -a ≤ (↑z : R) ↔ (↑(-z) : R) ≤ a
Tactic: rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
rw₁ : -a ≤ (↑z : R) ↔ -z ≤ ⌊a⌋
rw₂ : -a ≤ (↑z : R) ↔ (↑(-z) : R) ≤ a
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
have rw₃ : -a ≤ (↑z : R) ↔ -(↑z : R) ≤ a
Tactic: rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
rw₁ : -a ≤ (↑z : R) ↔ -z ≤ ⌊a⌋
rw₂ : -a ≤ (↑z : R) ↔ (↑(-z) : R) ≤ a
rw₃ : -a ≤ (↑z : R) ↔ -(↑z : R) ≤ a
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
have rw₄ : -(↑z : R) ≤ a ↔ -(↑z : R) ≤ a
Tactic: rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z a : ℤ
⊢ ceil.{u_2} (α := R) (↑z : R) ≤ a ↔ z ≤ a
have rw : LE.le.{u_2} (α := R) (↑z : R) (↑a : R) ↔ z ≤ a
Tactic: rw [ceil_le, Int.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z a : ℤ
rw : LE.le.{u_2} (α := R) (↑z : R) (↑a : R) ↔ z ≤ a
⊢ ceil.{u_2} (α := R) (↑z : R) ≤ a ↔ z ≤ a
have rw₁ : z ≤ a ↔ z ≤ a
Tactic: rw [ceil_le, Int.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : ℤ
⊢ ceil.{u_2} (α := R) (↑n : R) ≤ a ↔ (↑n : ℤ) ≤ a
have rw : LE.le.{u_2} (α := R) (↑n : R) (↑a : R) ↔ (↑n : ℤ) ≤ a
Tactic: rw [ceil_le, ← cast_natCast, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : ℤ
rw : LE.le.{u_2} (α := R) (↑n : R) (↑a : R) ↔ (↑n : ℤ) ≤ a
⊢ ceil.{u_2} (α := R) (↑n : R) ≤ a ↔ (↑n : ℤ) ≤ a
have rw₁ : LE.le.{u_2} (α := R) (↑(↑n : ℤ) : R) (↑a : R) ↔ (↑n : ℤ) ≤ a
Tactic: rw [ceil_le, ← cast_natCast, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : ℤ
rw : LE.le.{u_2} (α := R) (↑n : R) (↑a : R) ↔ (↑n : ℤ) ≤ a
rw₁ : LE.le.{u_2} (α := R) (↑(↑n : ℤ) : R) (↑a : R) ↔ (↑n : ℤ) ≤ a
⊢ ceil.{u_2} (α := R) (↑n : R) ≤ a ↔ (↑n : ℤ) ≤ a
have rw₂ : (↑n : ℤ) ≤ a ↔ (↑n : ℤ) ≤ a
Tactic: rw [ceil_le, ← cast_natCast, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z
have rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
Tactic: rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z
have rw₁ : -⌈a + (↑z : R)⌉ = -⌈a⌉ - z
Tactic: rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
rw₁ : -⌈a + (↑z : R)⌉ = -⌈a⌉ - z
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z
have rw₂ : ⌊-(a + (↑z : R))⌋ = -⌈a⌉ - z
Tactic: rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
rw₁ : -⌈a + (↑z : R)⌉ = -⌈a⌉ - z
rw₂ : ⌊-(a + (↑z : R))⌋ = -⌈a⌉ - z
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z
have rw₃ : ⌊-(a + (↑z : R))⌋ = ⌊-a⌋ - z
Tactic: rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
rw₁ : -⌈a + (↑z : R)⌉ = -⌈a⌉ - z
rw₂ : ⌊-(a + (↑z : R))⌋ = -⌈a⌉ - z
rw₃ : ⌊-(a + (↑z : R))⌋ = ⌊-a⌋ - z
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z
have rw₄ : ⌊-a - (↑z : R)⌋ = ⌊-a⌋ - z
Tactic: rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : -⌈a + (↑z : R)⌉ = -(⌈a⌉ + z)
rw₁ : -⌈a + (↑z : R)⌉ = -⌈a⌉ - z
rw₂ : ⌊-(a + (↑z : R))⌋ = -⌈a⌉ - z
rw₃ : ⌊-(a + (↑z : R))⌋ = ⌊-a⌋ - z
rw₄ : ⌊-a - (↑z : R)⌋ = ⌊-a⌋ - z
⊢ ⌈a + (↑z : R)⌉ = ⌈a⌉ + z
have rw₅ : ⌊-a⌋ - z = ⌊-a⌋ - z
Tactic: rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
a : R
⊢ ⌈(↑z : R) + a⌉ = z + ⌈a⌉
have rw : ⌈a + (↑z : R)⌉ = z + ⌈a⌉
Tactic: rw [add_comm, ceil_add_intCast, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
a : R
rw : ⌈a + (↑z : R)⌉ = z + ⌈a⌉
⊢ ⌈(↑z : R) + a⌉ = z + ⌈a⌉
have rw₁ : ⌈a⌉ + z = z + ⌈a⌉
Tactic: rw [add_comm, ceil_add_intCast, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z : ℤ
a : R
rw : ⌈a + (↑z : R)⌉ = z + ⌈a⌉
rw₁ : ⌈a⌉ + z = z + ⌈a⌉
⊢ ⌈(↑z : R) + a⌉ = z + ⌈a⌉
have rw₂ : z + ⌈a⌉ = z + ⌈a⌉
Tactic: rw [add_comm, ceil_add_intCast, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a + (↑n : R)⌉ = ⌈a⌉ + (↑n : ℤ)
have rw : ⌈a + (↑(↑n : ℤ) : R)⌉ = ⌈a⌉ + (↑n : ℤ)
Tactic: rw [← Int.cast_natCast, ceil_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
rw : ⌈a + (↑(↑n : ℤ) : R)⌉ = ⌈a⌉ + (↑n : ℤ)
⊢ ⌈a + (↑n : R)⌉ = ⌈a⌉ + (↑n : ℤ)
have rw₁ : ⌈a⌉ + (↑n : ℤ) = ⌈a⌉ + (↑n : ℤ)
Tactic: rw [← Int.cast_natCast, ceil_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌈a + 1⌉ = ⌈a⌉ + 1
have rw : ⌈a + 1⌉ = ⌈a + (↑1 : R)⌉
Tactic: rw [← ceil_add_intCast a (1 : ℤ), cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
rw : ⌈a + 1⌉ = ⌈a + (↑1 : R)⌉
⊢ ⌈a + 1⌉ = ⌈a⌉ + 1
have rw₁ : ⌈a + 1⌉ = ⌈a + 1⌉
Tactic: rw [← ceil_add_intCast a (1 : ℤ), cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
⊢ ⌈a - (↑z : R)⌉ = ⌈a + (↑(-z) : R)⌉
have rw : ⌈a - (↑z : R)⌉ = ⌈a + -(↑z : R)⌉
Tactic: rw [Int.cast_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
z : ℤ
rw : ⌈a - (↑z : R)⌉ = ⌈a + -(↑z : R)⌉
⊢ ⌈a - (↑z : R)⌉ = ⌈a + (↑(-z) : R)⌉
have rw₁ : ⌈a + -(↑z : R)⌉ = ⌈a + -(↑z : R)⌉
Tactic: rw [Int.cast_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a - (↑n : R)⌉ = ⌈a⌉ - (↑n : ℤ)
have h : ⌈a - (↑n : R)⌉ = ⌈a - (↑(↑n : ℤ) : R)⌉
Tactic: convert! ceil_sub_intCast a n using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌈a - 1⌉ = ⌈a⌉ - 1
have rw : ⌈a - 1⌉ + 1 = ⌈a⌉
Tactic: rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
rw : ⌈a - 1⌉ + 1 = ⌈a⌉
⊢ ⌈a - 1⌉ = ⌈a⌉ - 1
have rw₁ : ⌈a - 1 + 1⌉ = ⌈a⌉
Tactic: rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
rw : ⌈a - 1⌉ + 1 = ⌈a⌉
rw₁ : ⌈a - 1 + 1⌉ = ⌈a⌉
⊢ ⌈a - 1⌉ = ⌈a⌉ - 1
have rw₂ : ⌈a⌉ = ⌈a⌉
Tactic: rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ (↑⌈a⌉ : R) < a + 1
have rw : ⌈a⌉ < ⌈a⌉ + 1
Tactic: rw [← lt_ceil, ← Int.cast_one, ceil_add_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
have rw : a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉ : R) (↑⌈b⌉ : R)
Tactic: rw [ceil_le, Int.cast_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉ : R) (↑⌈b⌉ : R)
have h₁ : a ≤ (↑⌈a⌉ : R)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
h₁ : a ≤ (↑⌈a⌉ : R)
⊢ a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉ : R) (↑⌈b⌉ : R)
have h₂ : b ≤ (↑⌈b⌉ : R)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
have rw : (↑⌈b⌉ : R) ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a
Tactic: rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ (↑⌈b⌉ : R) ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a
have refine : b + 1 ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a
Tactic: refine (ceil_lt_add_one _).le.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a b : R
⊢ b + 1 ≤ HAdd.hAdd (α := R) (↑⌈a + b⌉ : R) 1 - a
have rw : a + b ≤ (↑⌈a + b⌉ : R)
Tactic: rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
⊢ ceil.{u_2} (α := R) 0 = 0
have rw : ceil.{u_2} (α := R) (↑0 : R) = 0
Tactic: rw [← cast_zero, ceil_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : ceil.{u_2} (α := R) (↑0 : R) = 0
⊢ ceil.{u_2} (α := R) 0 = 0
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [← cast_zero, ceil_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
⊢ ceil.{u_2} (α := R) 1 = 1
have rw : ceil.{u_2} (α := R) (↑1 : R) = 1
Tactic: rw [← cast_one, ceil_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
rw : ceil.{u_2} (α := R) (↑1 : R) = 1
⊢ ceil.{u_2} (α := R) 1 = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [← cast_one, ceil_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ range Int.cast
have refine_1 : ∀ (h : ⌈a⌉ = ⌊a⌋ + 1) (ht : Membership.mem (γ := Set R) (range Int.cast) a), False
Tactic: refine ⟨fun h ht => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
refine_1 : ∀ (h : ⌈a⌉ = ⌊a⌋ + 1) (ht : Membership.mem (γ := Set R) (range Int.cast) a), False
⊢ ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ range Int.cast
have refine_2 : ∀ (h : a ∉ range Int.cast), ⌈a⌉ = ⌊a⌋ + 1
Tactic: refine ⟨fun h ht => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : Membership.mem (γ := Set R) (range Int.cast) a
⊢ False
have h0 : Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑⌈a⌉ : R)
Tactic: have h0 := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : Membership.mem (γ := Set R) (range Int.cast) a
h0 : Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑⌈a⌉ : R)
⊢ False
have h0₁ : Eq.{u_2 + 1} (α := R) 1 0
Tactic: rw [h, cast_add, cast_one, left_eq_add] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌈a⌉ = ⌊a⌋ + 1
have refine_2 : ⌊a⌋ + 1 ≤ ⌈a⌉
Tactic: apply le_antisymm (Int.ceil_le_floor_add_one _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌊a⌋ + 1 ≤ ⌈a⌉
have refine_2 : (↑⌊a⌋ : R) < a
Tactic: rw [add_one_le_iff, lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
have inl : ∀ (ha : fract a = 0), fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
Tactic: rcases eq_or_ne (fract a) 0 with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
inl : ∀ (ha : fract a = 0), fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
have inr : ∀ (ha : fract a ≠ 0), fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
Tactic: rcases eq_or_ne (fract a) 0 with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - (↑⌈a⌉ : R)
have inr : fract a = a + 1 - (↑⌈a⌉ : R)
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
this : (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
⊢ fract a = a + 1 - (↑⌈a⌉ : R)
have rw : fract a = a + 1 - (a - fract a + 1)
Tactic: rw [this, ← self_sub_fract]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ fract a = a + 1 - (↑⌈a⌉ : R)
have inr : (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
Tactic: suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ (↑⌈a⌉ : R) = HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
have inr : Eq.{u_2 + 1} (α := R) (↑⌈a⌉ : R) (↑(⌊a⌋ + 1) : R)
Tactic: rw [← Int.cast_one, ← Int.cast_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉ : R) (↑(⌊a⌋ + 1) : R)
have inr : HSub.hSub (α := R) (↑(⌊a⌋ + 1) : R) 1 < a
Tactic: refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ HSub.hSub (α := R) (↑(⌊a⌋ + 1) : R) 1 < a
have inr : 0 < fract a
Tactic: rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
ha : fract a ≠ 0
⊢ (↑⌈a⌉ : R) = a + 1 - fract a
have rw : (↑⌈a⌉ : R) = a + 1 - (a + 1 - (↑⌈a⌉ : R))
Tactic: rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
ha : fract a ≠ 0
⊢ (↑⌈a⌉ : R) - a = 1 - fract a
have rw : (↑⌈a⌉ : R) - a = 1 - (a + 1 - (↑⌈a⌉ : R))
Tactic: rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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 * 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.Ring (goal)
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
⊢ 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.Ring (goal)
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 * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)
have rwa : b * (↑⌊a⌋ : k) + b ≤ (↑⌊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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)
have rwa₁ : b ≤ (↑⌊a⌋ : k) - b * (↑⌊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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)
have rwa₂ : b ≤ (1 - b) * (↑⌊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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)
have rwa₃ : b / (1 - b) ≤ (↑⌊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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ b * HAdd.hAdd (α := k) (↑⌊a⌋ : k) 1 ≤ (↑⌊a⌋ : k)
have rwa₄ : ⌈b / (1 - b)⌉ ≤ ⌊a⌋
Tactic: rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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 * 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
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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 * 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
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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
⊢ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉
have inl : ∀ (ha : LE.le.{u_4} (α := k) 1 1),
  ⌈HDiv.hDiv (α := k) (↑⌈(HSub.hSub (α := k) 1 1)⁻¹⌉ : k) 1⌉ = ⌈(HSub.hSub (α := k) 1 1)⁻¹⌉
Tactic: obtain rfl | ha := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)⁻¹⌉
⊢ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉
have inr : ∀ (ha : 1 < a), ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉
Tactic: obtain rfl | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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
have linarith : a - 1 ≤ 0 → 1 - a + (a - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
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
⊢ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉
have this : 0 < a - 1
Tactic: have : 0 < a - 1 := by linarith