case h
F : Type ?u.246936
α : Type u_1
β : Type ?u.246942
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉
F : Type ?u.246936
α : Type u_1
β : Type ?u.246942
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ Int.cast ⁻¹' Iio a = Iio ⌈a⌉
ext
no goals
case h
F : Type ?u.246936
α : Type u_1
β : Type ?u.246942
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉
simp [lt_ceil]