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