case h
F : Type ?u.236506
α : Type u_1
β : Type ?u.236512
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ ⌈b⌉
F : Type ?u.236506
α : Type u_1
β : Type ?u.236512
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ Int.cast ⁻¹' Ioo a b = Ioo ⌊a⌋ ⌈b⌉
ext
no goals
case h
F : Type ?u.236506
α : Type u_1
β : Type ?u.236512
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ ⌈b⌉
simp [floor_lt, lt_ceil]