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