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