ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>h : b₁ ≤ b₂<VAR>ha : a ≤ 0<GOAL>a • b₂ ≤ a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>ha : a ≤ 0<GOAL>Antitone fun x => a • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>hb : b₁ < b₂<VAR>ha : a < 0<GOAL>a • b₂ < a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>ha : a < 0<GOAL>StrictAnti fun x => a • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulReflectLE α β<VAR>h : a • b₁ ≤ a • b₂<VAR>ha : a < 0<GOAL>b₂ ≤ b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulReflectLT α β<VAR>h : a • b₁ < a • b₂<VAR>ha : a ≤ 0<GOAL>b₂ < b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>SMulPosMono α β<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>0 ≤ a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>ha : a < 0<GOAL>a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>a • b₁ < a • b₂ ↔ b₂ < b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>0 < a • b ↔ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>a • b < 0 ↔ 0 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hab : b₁ ≤ b₂<VAR>hcd : a ≤ d<GOAL>b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hba : b₂ ≤ b₁<VAR>hdc : d ≤ a<GOAL>b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hab : b₁ < b₂<VAR>hcd : a < d<GOAL>b₁ • d + b₂ • a < b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hba : b₂ < b₁<VAR>hdc : d < a<GOAL>b₁ • d + b₂ • a < b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>a : α<VAR>ha : a ≤ 0<VAR>b₁ b₂ : β<GOAL>a • max b₁ b₂ = min (a • b₁) (a • b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>a : α<VAR>ha : a ≤ 0<VAR>b₁ b₂ : β<GOAL>a • min b₁ b₂ = max (a • b₁) (a • b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>hab : 0 ≤ a • b<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>PosSMulMono α β<VAR>h : a < 0<GOAL>a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>PosSMulMono α β<VAR>h : a < 0<GOAL>b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>a : α<VAR>PosSMulMono α β<VAR>ha : a < 0<GOAL>∀ (a_1 : βᵒᵈ), (RelIso.symm (OrderIso.smulRightDual β ha)) a_1 = a⁻¹ • OrderDual.ofDual a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>a : α<VAR>PosSMulMono α β<VAR>ha : a < 0<GOAL>∀ (a_1 : β), (OrderIso.smulRightDual β ha) a_1 = a • OrderDual.toDual a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>PosSMulStrictMono α β<VAR>h : a < 0<GOAL>a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>PosSMulStrictMono α β<VAR>h : a < 0<GOAL>b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero α<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>PosSMulMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<GOAL>PosSMulMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero α<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>PosSMulStrictMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<GOAL>PosSMulStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero α<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>PosSMulReflectLE α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<GOAL>PosSMulReflectLE α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero α<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>PosSMulReflectLT α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<GOAL>PosSMulReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Zero β<VAR>Preorder β<VAR>Zero γ<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>SMulPosMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<GOAL>SMulPosMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Zero β<VAR>Preorder β<VAR>Zero γ<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>SMulPosStrictMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<GOAL>SMulPosStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Zero β<VAR>Preorder β<VAR>Zero γ<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>SMulPosReflectLE α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<GOAL>SMulPosReflectLE α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Zero β<VAR>Preorder β<VAR>Zero γ<VAR>Preorder γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>SMulPosReflectLT α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<GOAL>SMulPosReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulMono α β<VAR>a : α<VAR>b : β<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulMono α β<VAR>a : α<VAR>b : β<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 ≤ a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMul α β<VAR>NoZeroSMulDivisors α β<VAR>a : α<VAR>b : β<VAR>Preorder α<VAR>ha : 0 < a<VAR>hb : b ≠ 0<GOAL>a • b ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMul α β<VAR>NoZeroSMulDivisors α β<VAR>a : α<VAR>b : β<VAR>Preorder β<VAR>ha : a ≠ 0<VAR>hb : 0 < b<GOAL>a • b ≠ 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>a b : ι → R<VAR>OrderBot R<VAR>s : Finset ι<VAR>ha : ∀ i ∈ s, 0 ≤ a i<VAR>hb : ∀ i ∈ s, 0 ≤ b i<GOAL>s.sup (a * b) ≤ s.sup a * s.sup b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>a b : ι → R<VAR>OrderTop R<VAR>s : Finset ι<VAR>ha : ∀ i ∈ s, 0 ≤ a i<VAR>hb : ∀ i ∈ s, 0 ≤ b i<GOAL>s.inf a * s.inf b ≤ s.inf (a * b)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>a b : ι → R<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>ha : ∀ i ∈ s, 0 ≤ a i<VAR>hb : ∀ i ∈ s, 0 ≤ b i<GOAL>s.sup' H (a * b) ≤ s.sup' H a * s.sup' H b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>a b : ι → R<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>ha : ∀ i ∈ s, 0 ≤ a i<VAR>hb : ∀ i ∈ s, 0 ≤ b i<GOAL>s.inf' H a * s.inf' H b ≤ s.inf' H (a * b)
<VAR>α : Type u_4<VAR>OrderedSemiring α<VAR>self : FloorSemiring α<VAR>a : α<VAR>ha : a < 0<GOAL>FloorSemiring.floor a = 0
<VAR>α : Type u_4<VAR>OrderedSemiring α<VAR>self : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>n ≤ FloorSemiring.floor a ↔ ↑n ≤ a
<VAR>α : Type u_4<VAR>OrderedSemiring α<VAR>self : FloorSemiring α<GOAL>GaloisConnection FloorSemiring.ceil Nat.cast
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : ↑n ≤ a<GOAL>n ≤ ⌊a⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ < n ↔ a < ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ < 1 ↔ a < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : ⌊a⌋₊ < n<GOAL>a < ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>h : ⌊a⌋₊ < 1<GOAL>a < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌊a⌋₊ ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>a < ↑⌊a⌋₊.succ
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>a < ↑⌊a⌋₊ + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<GOAL>⌊↑n⌋₊ = n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>⌊0⌋₊ = 0
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>⌊1⌋₊ = 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌊OfNat.ofNat n⌋₊ = n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : a ≤ 0<GOAL>⌊a⌋₊ = 0
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>Monotone Nat.floor
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>x y : α<GOAL>x ≤ y → ⌊x⌋₊ ≤ ⌊y⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>x : α<GOAL>1 ≤ ⌊x⌋₊ ↔ 1 ≤ x
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⌊a⌋₊ < n ↔ a < ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>0 < ⌊a⌋₊ ↔ 1 ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>h : 0 < ⌊a⌋₊<GOAL>0 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : n < ⌊a⌋₊<GOAL>↑n < a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : a ≤ ↑n<GOAL>⌊a⌋₊ ≤ n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>h : a ≤ 1<GOAL>⌊a⌋₊ ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>⌊a⌋₊ = 0 ↔ a < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋₊ = n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋₊ = ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>Nat.floor ⁻¹' {0} = Set.Iio 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Nat.floor ⁻¹' {n} = Set.Ico (↑n) (↑n + 1)
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>GaloisConnection Nat.ceil Nat.cast
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌈a⌉₊ ≤ n ↔ a ≤ ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>n < ⌈a⌉₊ ↔ ↑n < a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>1 ≤ ⌈a⌉₊ ↔ 0 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>⌈a⌉₊ ≤ ⌊a⌋₊ + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>a ≤ ↑⌈a⌉₊
<VAR>α : Type u_4<VAR>LinearOrderedRing α<VAR>FloorSemiring α<VAR>z : ℤ<GOAL>⌈↑z⌉₊ = z.toNat
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<GOAL>⌈↑n⌉₊ = n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>Monotone Nat.ceil
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>x y : α<GOAL>x ≤ y → ⌈x⌉₊ ≤ ⌈y⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>⌈0⌉₊ = 0
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>⌈1⌉₊ = 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌈OfNat.ofNat n⌉₊ = n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>⌈a⌉₊ = 0 ↔ a ≤ 0
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>0 < ⌈a⌉₊ ↔ 0 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : ⌈a⌉₊ < n<GOAL>a < ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : ⌈a⌉₊ ≤ n<GOAL>a ≤ ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>⌊a⌋₊ ≤ ⌈a⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a b : α<VAR>h : a < b<VAR>h' : 0 < b<GOAL>⌊a⌋₊ < ⌈b⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>Nat.ceil ⁻¹' {0} = Set.Iic 0
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Nat.ceil ⁻¹' {n} = Set.Ioc ↑(n - 1) ↑n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a b : α<VAR>ha : 0 ≤ a<GOAL>Nat.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a b : α<GOAL>Nat.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>Nat.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a b : α<VAR>hb : 0 ≤ b<GOAL>Nat.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>Nat.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>Nat.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<GOAL>Nat.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>Nat.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<VAR>n : ℕ<GOAL>⌊a + ↑n⌋₊ = ⌊a⌋₊ + n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>⌊a + 1⌋₊ = ⌊a⌋₊ + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌊a + OfNat.ofNat n⌋₊ = ⌊a⌋₊ + OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<GOAL>⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>ExistsAddOfLE α<VAR>a : α<GOAL>⌊a - 1⌋₊ = ⌊a⌋₊ - 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<VAR>n : ℕ<GOAL>⌈a + ↑n⌉₊ = ⌈a⌉₊ + n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>⌈a + 1⌉₊ = ⌈a⌉₊ + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌈a + OfNat.ofNat n⌉₊ = ⌈a⌉₊ + OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌈a⌉₊ < a + 1
<VAR>α : Type u_2<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<VAR>a b : α<GOAL>⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorSemiring α<VAR>a : α<GOAL>a - 1 < ↑⌊a⌋₊
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>FloorSemiring α<VAR>m n : ℕ<GOAL>⌊↑m / ↑n⌋₊ = m / n
<VAR>α : Type u_4<VAR>LinearOrderedSemiring α<GOAL>Subsingleton (FloorSemiring α)
<VAR>α : Type u_4<VAR>LinearOrderedRing α<VAR>self : FloorRing α<GOAL>GaloisConnection FloorRing.ceil Int.cast
<VAR>α : Type u_4<VAR>LinearOrderedRing α<VAR>self : FloorRing α<GOAL>GaloisConnection Int.cast FloorRing.floor
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>GaloisConnection Int.cast Int.floor
<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>⌊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>0 ≤ ⌊a⌋ ↔ 0 ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊a⌋ ≤ z - 1 ↔ a < ↑z
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌊a⌋ ≤ -1 ↔ a < 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<VAR>ha : a ≤ 0<GOAL>⌊a⌋ ≤ 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>a < ↑⌊a⌋.succ
<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 - 1 < ↑⌊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 α<GOAL>⌊0⌋ = 0
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>⌊1⌋ = 1
<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.floor
<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 : α<GOAL>0 < ⌊a⌋ ↔ 1 ≤ a
<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 : α<GOAL>⌊a + 1⌋ = ⌊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⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
<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>a : α<VAR>n : ℕ<GOAL>⌊a + ↑n⌋ = ⌊a⌋ + ↑n
<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>n : ℕ<VAR>a : α<GOAL>⌊↑n + a⌋ = ↑n + ⌊a⌋
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>a : α<GOAL>⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋
<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_4<VAR>LinearOrderedCommRing α<VAR>FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<GOAL>|a - b| < 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>⌊a⌋ = 0 ↔ a ∈ Set.Ico 0 1
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℤ<VAR>a : α<GOAL>a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋ = n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>n : ℤ<VAR>a : α<GOAL>a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋ = ↑n
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>m : ℤ<GOAL>Int.floor ⁻¹' {m} = Set.Ico (↑m) (↑m + 1)
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>a : α<GOAL>a - ↑⌊a⌋ = Int.fract a
<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 : α<VAR>m : ℤ<GOAL>Int.fract (a + ↑m) = 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 : α<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>m : ℤ<VAR>a : α<GOAL>Int.fract (↑m + a) = Int.fract a