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