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