case h
F : Type ?u.74183
α : Type u_1
β : Type ?u.74189
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉₊
F : Type ?u.74183
α : Type u_1
β : Type ?u.74189
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
⊢ Nat.cast ⁻¹' Ici a = Ici ⌈a⌉₊
ext
no goals
case h
F : Type ?u.74183
α : Type u_1
β : Type ?u.74189
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉₊
simp [ceil_le]