case h
F : Type ?u.245095
α : Type u_1
β : Type ?u.245101
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋
F : Type ?u.245095
α : Type u_1
β : Type ?u.245101
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ Int.cast ⁻¹' Ioi a = Ioi ⌊a⌋
ext
no goals
case h
F : Type ?u.245095
α : Type u_1
β : Type ?u.245101
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋
simp [floor_lt]