case h
F : Type ?u.65750
α : Type u_1
β : Type ?u.65756
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋₊ ⌊b⌋₊
F : Type ?u.65750
α : Type u_1
β : Type ?u.65756
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Ioc a b = Ioc ⌊a⌋₊ ⌊b⌋₊
ext
no goals
case h
F : Type ?u.65750
α : Type u_1
β : Type ?u.65756
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋₊ ⌊b⌋₊
simp [floor_lt, le_floor_iff, hb, ha]