ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>a : α<GOAL>Int.fract (↑n + a) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract (1 + a) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>a : α<GOAL>Int.fract (OfNat.ofNat n + a) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>m : ℤ<GOAL>Int.fract (a - ↑m) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>n : ℕ<GOAL>Int.fract (a - ↑n) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract (a - 1) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Int.fract (a - OfNat.ofNat n) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.fract (a + b) ≤ Int.fract a + Int.fract b
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.fract a + Int.fract b ≤ Int.fract (a + b) + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>a - Int.fract a = ↑⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract a - a = -↑⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>0 ≤ Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>0 < Int.fract a ↔ a ≠ ↑⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract a < 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Int.fract 0 = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Int.fract 1 = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>|Int.fract a| = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>|1 - Int.fract a| = 1 - Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<GOAL>Int.fract ↑z = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<GOAL>Int.fract ↑n = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Int.fract (OfNat.ofNat n) = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract ↑⌊a⌋ = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌊Int.fract a⌋ = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.fract a = Int.fract b ↔ ∃ z, a - b = ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract a = a ↔ 0 ≤ a ∧ a < 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract (Int.fract a) = Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>∃ z, Int.fract (a + b) - Int.fract a - Int.fract b = ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>hx : Int.fract x ≠ 0<GOAL>Int.fract (-x) = 1 - Int.fract x
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<GOAL>Int.fract (-x) = 0 ↔ Int.fract x = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>b : ℕ<GOAL>∃ z, Int.fract a * ↑b - Int.fract (a * ↑b) = ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>s : Set α<GOAL>Int.fract ⁻¹' s = ⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Set.Ico 0 1)
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>s : Set α<GOAL>Int.fract '' s = ⋃ m, (fun x => x - ↑m) '' s ∩ Set.Ico 0 1
<VAR>k : Type u_4<VAR>LinearOrderedField k<VAR>FloorRing k<VAR>a b : k<VAR>ha : 0 < a<GOAL>Int.fract (b / a) * a ∈ Set.Ico 0 a
<VAR>k : Type u_4<VAR>LinearOrderedField k<VAR>FloorRing k<VAR>a b : k<VAR>ha : a ≠ 0<GOAL>Int.fract (b / a) * a + ⌊b / a⌋ • a = b
<VAR>k : Type u_4<VAR>LinearOrderedField k<VAR>FloorRing k<VAR>b : k<VAR>a : k<VAR>hb : 0 < b<GOAL>0 ≤ a - ↑⌊a / b⌋ * b
<VAR>k : Type u_4<VAR>LinearOrderedField k<VAR>FloorRing k<VAR>b : k<VAR>a : k<VAR>hb : 0 < b<GOAL>a - ↑⌊a / b⌋ * b < b
<VAR>k : Type u_4<VAR>LinearOrderedField k<VAR>FloorRing k<VAR>m n : ℕ<GOAL>Int.fract (↑m / ↑n) = ↑(m % n) / ↑n
<VAR>k : Type u_4<VAR>LinearOrderedField k<VAR>FloorRing k<VAR>m : ℤ<VAR>n : ℕ<GOAL>Int.fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>GaloisConnection Int.ceil Int.cast
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌈a⌉ ≤ z ↔ a ≤ ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌊-a⌋ = -⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌈-a⌉ = -⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>z < ⌈a⌉ ↔ ↑z < a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>z + 1 ≤ ⌈a⌉ ↔ ↑z < a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>1 ≤ ⌈a⌉ ↔ 0 < a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌈a⌉ ≤ ⌊a⌋ + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>a ≤ ↑⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<GOAL>⌈↑z⌉ = z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<GOAL>⌈↑n⌉ = ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌈OfNat.ofNat n⌉ = ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Monotone Int.ceil
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x y : α<GOAL>x ≤ y → ⌈x⌉ ≤ ⌈y⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>z : ℤ<GOAL>⌈a + ↑z⌉ = ⌈a⌉ + z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>n : ℕ<GOAL>⌈a + ↑n⌉ = ⌈a⌉ + ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌈a + 1⌉ = ⌈a⌉ + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>z : ℤ<GOAL>⌈a - ↑z⌉ = ⌈a⌉ - z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>n : ℕ<GOAL>⌈a - ↑n⌉ = ⌈a⌉ - ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌈a - 1⌉ = ⌈a⌉ - 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>↑⌈a⌉ < a + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>0 < ⌈a⌉ ↔ 0 < a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>⌈0⌉ = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>⌈1⌉ = 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ ⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌈a⌉ = 0 ↔ a ∈ Set.Ioc (-1) 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>a ∈ Set.Ioc (↑z - 1) ↑z → ⌈a⌉ = z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>a ∈ Set.Ioc (↑z - 1) ↑z → ↑⌈a⌉ = ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌊a⌋ ≤ ⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<VAR>h : a < b<GOAL>⌊a⌋ < ⌈b⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>m : ℤ<GOAL>Int.ceil ⁻¹' {m} = Set.Ioc (↑m - 1) ↑m
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.fract a = 0 ∨ Int.fract a = a + 1 - ↑⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : Int.fract a ≠ 0<GOAL>↑⌈a⌉ = a + 1 - Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : Int.fract a ≠ 0<GOAL>↑⌈a⌉ - a = 1 - Int.fract a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a b : α<GOAL>Int.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>Int.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>round 0 = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>round 1 = 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<GOAL>round ↑n = ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>round (OfNat.ofNat n) = ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℤ<GOAL>round ↑n = n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (x + ↑y) = round x + y
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>round (a + 1) = round a + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (x - ↑y) = round x - y
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>round (a - 1) = round a - 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>y : ℕ<GOAL>round (x + ↑y) = round x + ↑y
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>round (x + OfNat.ofNat n) = round x + OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>y : ℕ<GOAL>round (x - ↑y) = round x - ↑y
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>round (x - OfNat.ofNat n) = round x - OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (↑y + x) = y + round x
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>y : ℕ<GOAL>round (↑y + x) = ↑y + round x
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>x : α<GOAL>round (OfNat.ofNat n + x) = OfNat.ofNat n + round x
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<GOAL>|x - ↑(round x)| = min (Int.fract x) (1 - Int.fract x)
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>x : α<VAR>z : ℤ<GOAL>|x - ↑(round x)| ≤ |x - ↑z|
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : α<GOAL>round x = ⌊x + 1 / 2⌋
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<GOAL>round 2⁻¹ = 1
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<GOAL>round (-2⁻¹) = 0
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : α<GOAL>round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : α<GOAL>|x - ↑(round x)| ≤ 1 / 2
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>m n : ℕ<GOAL>|↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : α<GOAL>x - 1 / 2 < ↑(round x)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>x : α<GOAL>↑(round x) ≤ x + 1 / 2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>FloorSemiring α<VAR>FloorSemiring β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b<GOAL>⌊a⌋₊ = ⌊b⌋₊
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>FloorSemiring α<VAR>FloorSemiring β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℕ), a ≤ ↑n ↔ b ≤ ↑n<GOAL>⌈a⌉₊ = ⌈b⌉₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>FloorSemiring α<VAR>FloorSemiring β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>⌊f a⌋₊ = ⌊a⌋₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>FloorSemiring α<VAR>FloorSemiring β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>⌈f a⌉₊ = ⌈a⌉₊
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedRing β<VAR>FloorRing α<VAR>FloorRing β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℤ), ↑n ≤ a ↔ ↑n ≤ b<GOAL>⌊a⌋ = ⌊b⌋
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedRing β<VAR>FloorRing α<VAR>FloorRing β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℤ), a ≤ ↑n ↔ b ≤ ↑n<GOAL>⌈a⌉ = ⌈b⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedRing β<VAR>FloorRing α<VAR>FloorRing β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>⌊f a⌋ = ⌊a⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedRing β<VAR>FloorRing α<VAR>FloorRing β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>⌈f a⌉ = ⌈a⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedRing β<VAR>FloorRing α<VAR>FloorRing β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>Int.fract (f a) = f (Int.fract a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>LinearOrderedField β<VAR>FloorRing α<VAR>FloorRing β<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>round (f a) = round a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌊a⌋.toNat = ⌊a⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌈a⌉.toNat = ⌈a⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌊a⌋₊ = ⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌈a⌉₊ = ⌈a⌉
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌊a⌋₊ = ↑⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌈a⌉₊ = ↑⌈a⌉
<VAR>α : Type u_4<VAR>LinearOrderedRing α<GOAL>Subsingleton (FloorRing α)
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ ⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : 0 < a<GOAL>0 ≤ ⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>0 < a → 0 < ⌈a⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>0 < a → 0 < ⌈a⌉
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a b : α<GOAL>mabs a ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a b : α<GOAL>|a| ≤ b ↔ a ≤ b ∧ -a ≤ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a ≤ |a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a ≤ mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>-a ≤ |a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻¹ ≤ mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a b : α<VAR>h₀ : a ≤ b<VAR>h₁ : a⁻¹ ≤ b<GOAL>mabs a ≤ mabs b
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a b : α<VAR>h₀ : a ≤ b<VAR>h₁ : -a ≤ b<GOAL>|a| ≤ |b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>mabs a⁻¹ = mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>|(-a)| = |a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a b : α<GOAL>|a - b| = |b - a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a b : α<GOAL>mabs (a / b) = mabs (b / a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : 1 ≤ a<GOAL>mabs a = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : 0 ≤ a<GOAL>|a| = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : 0 < a<GOAL>|a| = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : 1 < a<GOAL>mabs a = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a ≤ 1<GOAL>mabs a = a⁻¹
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a ≤ 0<GOAL>|a| = -a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a < 1<GOAL>mabs a = a⁻¹
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a < 0<GOAL>|a| = -a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a b : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<GOAL>|a| ≤ |b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a b : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : 1 ≤ a<VAR>hab : a ≤ b<GOAL>mabs a ≤ mabs b
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>mabs 1 = 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>|0| = 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>0 ≤ |a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>|(|a|)| = |a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>mabs (mabs a) = mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>|a + b| ≤ |a| + |b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>mabs (a * b) ≤ mabs a * mabs b
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>||a| - |b|| ≤ |a - b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>mabs (mabs a / mabs b) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊔ b - a ⊓ b = |b - a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊔ b) / (a ⊓ b) = mabs (b / a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>2 • (a ⊔ b) = a + b + |b - a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊔ b) ^ 2 = a * b * mabs (b / a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊓ b) ^ 2 = a * b / mabs (b / a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>2 • (a ⊓ b) = a + b - |b - a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>|a ⊔ c - b ⊔ c| + |a ⊓ c - b ⊓ c| = |a - b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>mabs ((a ⊔ c) / (b ⊔ c)) * mabs ((a ⊓ c) / (b ⊓ c)) = mabs (a / b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>|a ⊔ c - b ⊔ c| ≤ |a - b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>mabs ((a ⊔ c) / (b ⊔ c)) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>|a ⊓ c - b ⊓ c| ≤ |a - b|
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>mabs ((a ⊔ c) / (b ⊔ c)) ⊔ mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>|a ⊔ c - b ⊔ c| ⊔ |a ⊓ c - b ⊓ c| ≤ |a - b|
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>x : α<GOAL>mabs x = x ∨ mabs x = x⁻¹
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>x : α<GOAL>|x| = x ∨ |x| = -x
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≤ |b| ↔ a ≤ b ∨ a ≤ -b
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≤ mabs b ↔ a ≤ b ∨ a ≤ b⁻¹
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a : α<GOAL>mabs a = max a a⁻¹
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a : α<GOAL>|a| = max a (-a)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a b : α<GOAL>a < |b| ↔ a < b ∨ a < -b
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a b : α<GOAL>a < mabs b ↔ a < b ∨ a < b⁻¹
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a : α<VAR>P : α → Prop<VAR>h1 : P a<VAR>h2 : P a⁻¹<GOAL>P (mabs a)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a : α<VAR>P : α → Prop<VAR>h1 : P a<VAR>h2 : P (-a)<GOAL>P |a|
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a b : α<VAR>h : |a| = b<GOAL>a = b ∨ a = -b
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a b : α<VAR>h : mabs a = b<GOAL>a = b ∨ a = b⁻¹
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a b : α<GOAL>mabs a = mabs b ↔ a = b ∨ a = b⁻¹
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a b : α<GOAL>|a| = |b| ↔ a = b ∨ a = -b
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a : α<GOAL>Even |a| ↔ Even a
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a : α<GOAL>IsSquare (mabs a) ↔ IsSquare a
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 < mabs a ↔ a ≠ 1
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>0 < |a| ↔ a ≠ 0
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : 1 < a<GOAL>1 < mabs a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : 0 < a<GOAL>0 < |a|
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : a < 0<GOAL>0 < |a|