case h
F : Type ?u.74766
ι : Type ?u.74769
α : Type ?u.74772
β : Type ?u.74775
K : Type u_1
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioo ↑a ↑b ↔ x ∈ Ioo a b
F : Type ?u.74766
ι : Type ?u.74769
α : Type ?u.74772
β : Type ?u.74775
K : Type u_1
inst✝ : LinearOrderedField K
a b : ℚ
⊢ Rat.cast ⁻¹' Ioo ↑a ↑b = Ioo a b
ext x
no goals
case h
F : Type ?u.74766
ι : Type ?u.74769
α : Type ?u.74772
β : Type ?u.74775
K : Type u_1
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioo ↑a ↑b ↔ x ∈ Ioo a b
simp