awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : 0 < a - 1
⊢ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉ = ⌈(a - 1)⁻¹⌉
have inr : ⌈(a - 1)⁻¹⌉ ≤ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉
Tactic: refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_
-- 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
this : 0 < a - 1
⊢ ⌈(a - 1)⁻¹⌉ ≤ ⌈(↑⌈(a - 1)⁻¹⌉ : k) / a⌉
have inr : (↑⌈(a - 1)⁻¹⌉ : k) < 1 / (1 - a⁻¹)
Tactic: rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
    ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ 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 : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ (↑⌈(a - 1)⁻¹⌉ : k) < 1 / (1 - a⁻¹)
have h : 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1
Tactic: convert! ceil_lt_add_one (R := k) _ using 1
-- 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 : 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.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 : 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.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 : 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.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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hab : a ≤ (b - 1)⁻¹
⊢ (↑⌈a⌉ : k) < b * a
have by : LE.le.{u_4} (α := 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.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 : 1 < b
hba : (↑⌈(b - 1)⁻¹⌉ : k) / b < a
hab : a ≤ (b - 1)⁻¹
by : LE.le.{u_4} (α := 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.Ring (hypothesis)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing 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.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 - 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.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 - 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.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 - 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.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 - 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.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 - 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 _
      _ = 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.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 - 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 _
      _ = 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.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 - 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 _
      _ = 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.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 : 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.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 : 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.Ring (goal)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing 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 ≠ 0
Tactic: rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
-- 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 / 2 < (↑⌊a⌋ : k)
have rw : 2⁻¹ * a < (↑⌊a⌋ : k)
Tactic: rw [div_eq_inv_mul]
-- 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
⊢ 2⁻¹ * a < (↑⌊a⌋ : k)
have refine_1 : LT.lt.{u_4} (α := k) 0 2⁻¹
Tactic: refine mul_lt_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
refine_1 : LT.lt.{u_4} (α := k) 0 2⁻¹
⊢ 2⁻¹ * a < (↑⌊a⌋ : k)
have refine_2 : LT.lt.{u_4} (α := k) 2⁻¹ 1
Tactic: refine mul_lt_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
refine_1 : LT.lt.{u_4} (α := k) 0 2⁻¹
refine_2 : LT.lt.{u_4} (α := 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.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 : 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.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 : 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.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a b : R
⊢ Int.cast ⁻¹' Ioo a b = Ioo ⌊a⌋ ⌈b⌉
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋ ⌈b⌉
Tactic: ext
-- 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 b : R
⊢ Int.cast ⁻¹' Ico a b = Ico ⌈a⌉ ⌈b⌉
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉ ⌈b⌉
Tactic: ext
-- 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 b : R
⊢ Int.cast ⁻¹' Ioc a b = Ioc ⌊a⌋ ⌊b⌋
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋ ⌊b⌋
Tactic: ext
-- 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 b : R
⊢ Int.cast ⁻¹' Icc a b = Icc ⌈a⌉ ⌊b⌋
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉ ⌊b⌋
Tactic: ext
-- 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
⊢ Int.cast ⁻¹' Ioi a = Ioi ⌊a⌋
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋
Tactic: ext
-- 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
⊢ Int.cast ⁻¹' Ici a = Ici ⌈a⌉
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉
Tactic: ext
-- 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
⊢ Int.cast ⁻¹' Iio a = Iio ⌈a⌉
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉
Tactic: ext
-- 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
⊢ Int.cast ⁻¹' Iic a = Iic ⌊a⌋
have h : ∀ (x : ℤ), x ∈ Int.cast ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℤ
⊢ LE.le.{u_3} (α := S) ((↑n : S) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
have rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
Tactic: rw [← map_intCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℤ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
⊢ LE.le.{u_3} (α := S) ((↑n : S) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
have rw₁ : (↑n : R) ≤ a ↔ (↑n : R) ≤ a
Tactic: rw [← map_intCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℤ
⊢ LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((↑n : S) : S) ↔ a ≤ (↑n : R)
have rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑n : R) : S) ↔ a ≤ (↑n : R)
Tactic: rw [← map_intCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℤ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑n : R) : S) ↔ a ≤ (↑n : R)
⊢ LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((↑n : S) : S) ↔ a ≤ (↑n : R)
have rw₁ : a ≤ (↑n : R) ↔ a ≤ (↑n : R)
Tactic: rw [← map_intCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
⊢ Eq.{u_3 + 1} (α := S) (fract ((f : (a : R) → S) a) : S) ((f : (a : R) → S) (fract a) : S)
have simp_rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
  (f : (a : R) → S) (a - (↑⌊a⌋ : R))
Tactic: simp_rw [fract, map_sub, map_intCast, map_floor _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
simp_rw :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
    (f : (a : R) → S) (a - (↑⌊a⌋ : R))
⊢ Eq.{u_3 + 1} (α := S) (fract ((f : (a : R) → S) a) : S) ((f : (a : R) → S) (fract a) : S)
have simp_rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑⌊a⌋ : R) : S)
Tactic: simp_rw [fract, map_sub, map_intCast, map_floor _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : Ring S
inst_3 : LinearOrder S
inst_4 : FloorRing R
inst_5 : FloorRing S
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_2, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
simp_rw :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
    (f : (a : R) → S) (a - (↑⌊a⌋ : R))
simp_rw₁ :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
    HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑⌊a⌋ : R) : S)
⊢ Eq.{u_3 + 1} (α := S) (fract ((f : (a : R) → S) a) : S) ((f : (a : R) → S) (fract a) : S)
have simp_rw₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑(floor.{u_3} (α := S) ((f : (a : R) → S) a : S)) : S) : S) =
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) a : S) ((↑⌊a⌋ : S) : S)
Tactic: simp_rw [fract, map_sub, map_intCast, map_floor _ hf]
-- 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 : IsStrictOrderedRing R
a : R
ha : -1 < a
⊢ (↑⌈a⌉₊ : R) < a + 1
have pos : ∀ (h : 0 ≤ a), (↑⌈a⌉₊ : R) < a + 1
Tactic: by_cases! h : 0 ≤ 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
inst_3 : IsStrictOrderedRing R
a : R
ha : -1 < a
pos : ∀ (h : 0 ≤ a), (↑⌈a⌉₊ : R) < a + 1
⊢ (↑⌈a⌉₊ : R) < a + 1
have neg : ∀ (h : a < 0), (↑⌈a⌉₊ : R) < a + 1
Tactic: by_cases! h : 0 ≤ 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
inst_3 : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ (↑⌈a⌉₊ : R) < a + 1
have neg : 0 < a + 1
Tactic: rw [ceil_eq_zero.mpr h.le, cast_zero]
-- 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
⊢ (↑⌊a⌋₊ : ℤ) = ⌊a⌋
have rw : (↑⌊a⌋.toNat : ℤ) = ⌊a⌋
Tactic: rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
rw : (↑⌊a⌋.toNat : ℤ) = ⌊a⌋
⊢ (↑⌊a⌋₊ : ℤ) = ⌊a⌋
have rw₁ : ⌊a⌋ = ⌊a⌋
Tactic: rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
⊢ (↑⌈a⌉₊ : ℤ) = ⌈a⌉
have rw : (↑⌈a⌉.toNat : ℤ) = ⌈a⌉
Tactic: rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
rw : (↑⌈a⌉.toNat : ℤ) = ⌈a⌉
⊢ (↑⌈a⌉₊ : ℤ) = ⌈a⌉
have rw₁ : ⌈a⌉ = ⌈a⌉
Tactic: rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : -1 < a
⊢ (↑⌈a⌉₊ : ℤ) = ⌈a⌉
have rw : (↑⌈a⌉.toNat : ℤ) = ⌈a⌉
Tactic: rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg_of_neg_one_lt 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : -1 < a
rw : (↑⌈a⌉.toNat : ℤ) = ⌈a⌉
⊢ (↑⌈a⌉₊ : ℤ) = ⌈a⌉
have rw₁ : ⌈a⌉ = ⌈a⌉
Tactic: rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg_of_neg_one_lt 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑⌊a⌋ : R)
have rw : Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑(↑⌊a⌋₊ : ℤ) : R)
Tactic: rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]
-- 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
rw : Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑(↑⌊a⌋₊ : ℤ) : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑⌊a⌋ : R)
have rw₁ : Eq.{u_2 + 1} (α := R) (↑⌊a⌋₊ : R) (↑⌊a⌋₊ : R)
Tactic: rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]
-- 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉ : R)
have rw : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑(↑⌈a⌉₊ : ℤ) : R)
Tactic: rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]
-- 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : 0 ≤ a
rw : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑(↑⌈a⌉₊ : ℤ) : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉ : R)
have rw₁ : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉₊ : R)
Tactic: rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]
-- 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : -1 < a
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉ : R)
have rw : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑(↑⌈a⌉₊ : ℤ) : R)
Tactic: rw [← Int.natCast_ceil_eq_ceil_of_neg_one_lt ha, Int.cast_natCast]
-- 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 : IsOrderedRing R
inst_3 : FloorRing R
a : R
ha : -1 < a
rw : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑(↑⌈a⌉₊ : ℤ) : R)
⊢ Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉ : R)
have rw₁ : Eq.{u_2 + 1} (α := R) (↑⌈a⌉₊ : R) (↑⌈a⌉₊ : R)
Tactic: rw [← Int.natCast_ceil_eq_ceil_of_neg_one_lt ha, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
⊢ Subsingleton.{u_4 + 1} (FloorRing R)
have refine : ∀ (H₁ H₂ : FloorRing R), H₁ = H₂
Tactic: refine ⟨fun H₁ H₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₁ H₂ : FloorRing R
⊢ H₁ = H₂
have this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
Tactic: have : H₁.floor = H₂.floor :=
    funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₁ H₂ : FloorRing R
this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
⊢ H₁ = H₂
have this₁ : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)
Tactic: have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
H₁ H₂ : FloorRing R
this_1 : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _)
this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)
⊢ H₁ = H₂
have mk : ∀ (floor ceil : R → ℤ) (gc_coe_floor : GaloisConnection Int.cast floor) (gc_ceil_coe : GaloisConnection ceil Int.cast)
  (this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.floor _ inst inst_1 _) (@FloorRing.floor _ inst inst_1 _))
  (this : Eq.{u_4 + 1} (α := R → ℤ) (@FloorRing.ceil _ inst inst_1 _) (@FloorRing.ceil _ inst inst_1 _)),
  { floor := floor, ceil := ceil, gc_coe_floor := gc_coe_floor, gc_ceil_coe := gc_ceil_coe : FloorRing R } = H₂
Tactic: cases H₁
Cleared hypotheses: H₁, this_1, this