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
inst_3 : IsOrderedRing R
a b : R
h : fract a = b
⊢ 0 ≤ b ∧ b < 1 ∧ ∃ (z : ℤ), a - b = (↑z : R)
have rw : 0 ≤ fract a ∧ fract a < 1 ∧ ∃ (z : ℤ), a - fract a = (↑z : R)
Tactic: rw [← 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 b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ fract a = b
have rw : Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑z : R)
Tactic: rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz]
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋ : R) (↑z : R)
have refine : ⌊a⌋ = z
Tactic: refine congrArg Int.cast ?_
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ ⌊a⌋ = z
have rw : a - b ≤ a ∧ a < a - b + 1
Tactic: rw [floor_eq_iff, ← hz]
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
⊢ a - b ≤ a ∧ a < a - b + 1
have left : a - b ≤ a
Tactic: constructor
-- 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₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = (↑z : R)
left : a - b ≤ a
⊢ a - b ≤ a ∧ a < a - b + 1
have right : a < a - b + 1
Tactic: constructor
-- 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) = b - (↑⌊b⌋ : R)
⊢ a - b = (↑(⌊a⌋ - ⌊b⌋) : R)
have rw : a - b = HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
Tactic: rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 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 b : R
h : a - (↑⌊a⌋ : R) = b - (↑⌊b⌋ : R)
rw : a - b = HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
⊢ a - b = (↑(⌊a⌋ - ⌊b⌋) : R)
have rw₁ : HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R) = HSub.hSub (α := R) (↑⌊a⌋ : R) (↑⌊b⌋ : R)
Tactic: rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 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 b : R
z : ℤ
hz : a - b = (↑z : R)
⊢ fract a = fract b
have refine : a - fract b = (↑(z + ⌊b⌋) : R)
Tactic: refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩
-- 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
z : ℤ
hz : a - b = (↑z : R)
⊢ a - fract b = (↑(z + ⌊b⌋) : R)
have rw : b + (↑z : R) - fract b = HAdd.hAdd (α := R) (↑z : R) (↑⌊b⌋ : R)
Tactic: rw [eq_add_of_sub_eq hz, add_comm, 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
x : R
hx : fract x ≠ 0
⊢ fract (-x) = 1 - fract x
have rw : 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
Tactic: rw [fract_eq_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
inst_3 : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
have left : 0 ≤ 1 - fract x
Tactic: constructor
-- 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
x : R
hx : fract x ≠ 0
left : 0 ≤ 1 - fract x
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
have right : 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
Tactic: constructor
-- 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
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x
have left : fract x ≤ 1
Tactic: rw [le_sub_iff_add_le, zero_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
x : R
hx : fract x ≠ 0
⊢ 1 - fract x < 1 ∧ ∃ (z : ℤ), -x - (1 - fract x) = (↑z : R)
have right : -x - (1 - fract x) = (↑(-⌊x⌋ - 1) : R)
Tactic: refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 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
x : R
hx : fract x ≠ 0
⊢ -x - (1 - fract x) = (↑(-⌊x⌋ - 1) : R)
have right : -x + fract x = -(↑⌊x⌋ : R)
Tactic: simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]
-- 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
x : R
hx : fract x ≠ 0
| -x
have rw : -((↑⌊x⌋ : R) + fract x)
Tactic: rw [← floor_add_fract x]
-- 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
x : R
hx : fract x ≠ 0
⊢ -x + fract x = -(↑⌊x⌋ : R)
have right : -((↑⌊x⌋ : R) + fract x) + fract x = -(↑⌊x⌋ : R)
Tactic: conv in -x => rw [← floor_add_fract x]
-- 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
x : R
⊢ fract (-x) = 0 ↔ fract x = 0
have simp : (∃ (z : ℤ), -x = (↑z : R)) ↔ ∃ (z : ℤ), x = (↑z : R)
Tactic: simp only [fract_eq_iff, le_refl, zero_lt_one, tsub_zero, true_and]
-- 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
x : R
⊢ (∃ (z : ℤ), -x = (↑z : R)) ↔ ∃ (z : ℤ), x = (↑z : R)
have mp : (∃ (z : ℤ), -x = (↑z : R)) → ∃ (z : ℤ), x = (↑z : R)
Tactic: constructor
-- 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
x : R
mp : (∃ (z : ℤ), -x = (↑z : R)) → ∃ (z : ℤ), x = (↑z : R)
⊢ (∃ (z : ℤ), -x = (↑z : R)) ↔ ∃ (z : ℤ), x = (↑z : R)
have mpr : (∃ (z : ℤ), x = (↑z : R)) → ∃ (z : ℤ), -x = (↑z : R)
Tactic: constructor
-- 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
x : R
z : ℤ
hz : -x = (↑z : R)
⊢ ∃ (z : ℤ), x = (↑z : R)
have h : x = (↑(-z) : R)
Tactic: use -z
-- 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
x : R
z : ℤ
hz : x = (↑z : R)
⊢ ∃ (z : ℤ), -x = (↑z : R)
have h : -x = (↑(-z) : R)
Tactic: use -z
-- 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 : ℤ), fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑z : R)
have h : fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑0 : R)
Tactic: use 0
-- 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
c : ℕ
hc : ∃ (z : ℤ), fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)
have succ : ∀ (z : ℤ) (hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)),
  ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)
Tactic: rcases hc with ⟨z, hz⟩
Cleared hypotheses: hc
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)
have succ : ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)
Tactic: rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)
have succ : ∀ (y : ℤ) (hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)),
  ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)
Tactic: rcases fract_add (a * c) a with ⟨y, hy⟩
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
y : ℤ
hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)
⊢ ∃ (z : ℤ), fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑z : R)
have h : fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑(z - y) : R)
Tactic: use z - y
-- 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
c : ℕ
z : ℤ
hz : fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)
y : ℤ
hy : fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a = (↑y : R)
⊢ fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) = (↑(z - y) : R)
have h : fract a * (↑c : R) + fract a - fract (a * (↑c : R) + a) =
  fract a * (↑c : R) - fract (a * (↑c : R)) - (fract (a * (↑c : R) + a) - fract (a * (↑c : R)) - fract a)
Tactic: rw [Int.cast_sub, ← hz, ← hy]
-- 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
b : ℕ
⊢ ∃ (z : ℤ), fract a * (↑b : R) - fract (a * (↑b : R)) = (↑z : R)
have zero : ∃ (z : ℤ), fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑z : R)
Tactic: induction b with
  | zero => use 0; simp
  | succ c hc =>
    rcases hc with ⟨z, hz⟩
    rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    rcases fract_add (a * c) a with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel
Cleared hypotheses: b
-- 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
b : ℕ
zero : ∃ (z : ℤ), fract a * (↑0 : R) - fract (a * (↑0 : R)) = (↑z : R)
⊢ ∃ (z : ℤ), fract a * (↑b : R) - fract (a * (↑b : R)) = (↑z : R)
have succ : ∀ (c : ℕ) (hc : ∃ (z : ℤ), fract a * (↑c : R) - fract (a * (↑c : R)) = (↑z : R)),
  ∃ (z : ℤ), fract a * (↑(c + 1) : R) - fract (a * (↑(c + 1) : R)) = (↑z : R)
Tactic: induction b with
  | zero => use 0; simp
  | succ c hc =>
    rcases hc with ⟨z, hz⟩
    rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    rcases fract_add (a * c) a with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel
Cleared hypotheses: b
-- 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
s : Set R
⊢ fract ⁻¹' s = ⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1)
have h : ∀ (x : R), x ∈ fract ⁻¹' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1)) x
Tactic: ext x
-- 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
s : Set R
x : R
⊢ x ∈ fract ⁻¹' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1)) x
have h : fract x ∈ s ↔ ∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))
Tactic: simp only [mem_preimage, mem_iUnion, mem_inter_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
inst_3 : IsOrderedRing R
s : Set R
x : R
⊢ fract x ∈ s ↔ ∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))
have h : (∃ (i : ℤ), x - (↑i : R) ∈ s ∧ Membership.mem (γ := Set R) (Ico 0 1) (x - (↑i : R))) → fract x ∈ s
Tactic: refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩
-- 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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
⊢ fract x ∈ s
have hms₁ : x - (↑⌊x⌋ : R) ∈ s
Tactic: obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
Cleared hypotheses: m, hms, hm0, hm1
-- 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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
hms₁ : x - (↑⌊x⌋ : R) ∈ s
⊢ fract x ∈ s
have hm0₁ : 0 ≤ x - (↑⌊x⌋ : R)
Tactic: obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
Cleared hypotheses: m, hms, hm0, hm1
-- 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
s : Set R
x : R
m : ℤ
hms : x - (↑m : R) ∈ s
hm0 : 0 ≤ x - (↑m : R)
hm1 : x - (↑m : R) < 1
hms₁ : x - (↑⌊x⌋ : R) ∈ s
hm0₁ : 0 ≤ x - (↑⌊x⌋ : R)
⊢ fract x ∈ s
have hm1₁ : x - (↑⌊x⌋ : R) < 1
Tactic: obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
Cleared hypotheses: m, hms, hm0, hm1
-- 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
s : Set R
⊢ fract '' s = ⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) '' s ∩ Ico 0 1
have h : ∀ (x : R), x ∈ fract '' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) '' s ∩ Ico 0 1) x
Tactic: ext x
-- 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
s : Set R
x : R
⊢ x ∈ fract '' s ↔ Membership.mem (γ := Set R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) '' s ∩ Ico 0 1) x
have h : (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
Tactic: simp only [mem_image, mem_inter_iff, mem_iUnion]
-- 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
s : Set R
x : R
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
have h : (∃ x_1 ∈ s, fract x_1 = x) → ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
Tactic: constructor
-- 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
s : Set R
x : R
h : (∃ x_1 ∈ s, fract x_1 = x) → ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x
have h₁ : (∃ (i : ℤ), (∃ x_1 ∈ s, x_1 - (↑i : R) = x) ∧ Membership.mem (γ := Set R) (Ico 0 1) x) → ∃ x_1 ∈ s, fract x_1 = x
Tactic: constructor
-- 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
s : Set R
m : ℤ
y : R
hys : y ∈ s
h0 : 0 ≤ y - (↑m : R)
h1 : y - (↑m : R) < 1
⊢ ∃ x ∈ s, fract x = y - (↑m : R)
have h : ∀ (h0 : 0 ≤ y - (↑⌊y⌋ : R)) (h1 : y - (↑⌊y⌋ : R) < 1), ∃ x ∈ s, fract x = y - (↑⌊y⌋ : R)
Tactic: obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩
Cleared hypotheses: m, h0, h1
-- 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 : FloorRing k
a b : k
ha : a ≠ 0
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b
have rw : fract (b / a) * a + (↑⌊b / a⌋ : k) * a = b
Tactic: rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b 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 : FloorRing k
a b : k
ha : a ≠ 0
rw : fract (b / a) * a + (↑⌊b / a⌋ : k) * a = b
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b
have rw₁ : (fract (b / a) + (↑⌊b / a⌋ : k)) * a = b
Tactic: rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b 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 : FloorRing k
a b : k
ha : a ≠ 0
rw : fract (b / a) * a + (↑⌊b / a⌋ : k) * a = b
rw₁ : (fract (b / a) + (↑⌊b / a⌋ : k)) * a = b
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b
have rw₂ : b / a * a = b
Tactic: rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b 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 : FloorRing k
a b : k
ha : a ≠ 0
rw : fract (b / a) * a + (↑⌊b / a⌋ : k) * a = b
rw₁ : (fract (b / a) + (↑⌊b / a⌋ : k)) * a = b
rw₂ : b / a * a = b
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b
have rw₃ : b = b
Tactic: rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b 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
b a : k
hb : 0 < b
⊢ a < b + (↑⌊a / b⌋ : k) * b
have rw : a / b < HAdd.hAdd (α := k) (↑⌊a / b⌋ : k) 1
Tactic: rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]
-- 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
m n : ℕ
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
have inl : fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % 0) : k) (↑0 : k)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n
-- 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
m n : ℕ
inl : fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % 0) : k) (↑0 : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
have inr : ∀ (hn : n > 0), fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- 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
m n : ℕ
hn : n > 0
⊢ LT.lt.{u_4} (α := k) 0 (↑n : k)
have norm_cast : 0 < n
Tactic: norm_cast
-- 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
m n : ℕ
hn : n > 0
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
have hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
Tactic: have hn' : 0 < (n : k) := by
    norm_cast
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
have inr : 0 ≤ HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
Tactic: refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : 0 ≤ HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
have inr₁ : HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) < 1
Tactic: refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : 0 ≤ HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
inr₁ : HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) < 1
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
have inr₂ : HDiv.hDiv (α := k) (↑m : k) (↑n : k) - HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) =
  (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)
Tactic: refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ HDiv.hDiv (α := k) (↑m : k) (↑n : k) - HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) =
    (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)
have inr : (↑m : k) = (↑(m % n) : k) + HMul.hMul (α := k) (↑n : k) (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)
Tactic: rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add,
      mul_div_cancel₀ _ hn'.ne']
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ (↑m : k) = (↑(m % n) : k) + HMul.hMul (α := k) (↑n : k) (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)
have inr : (↑m : k) = HAdd.hAdd (α := k) (↑(m % n) : k) (↑(n * (m / n)) : k)
Tactic: norm_cast
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ (↑m : k) = HAdd.hAdd (α := k) (↑(m % n) : k) (↑(n * (m / n)) : k)
have inr : Eq.{u_4 + 1} (α := k) (↑m : k) (↑(m % n + n * (m / n)) : k)
Tactic: rw [← Nat.cast_add, Nat.mod_add_div m n]
-- 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
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : Eq.{u_4 + 1} (α := k) (↑m : k) (↑(m % n + n * (m / n)) : k)
⊢ (↑m : k) = HAdd.hAdd (α := k) (↑(m % n) : k) (↑(n * (m / n)) : k)
have inr₁ : Eq.{u_4 + 1} (α := k) (↑m : k) (↑m : k)
Tactic: rw [← Nat.cast_add, Nat.mod_add_div m n]