case h
F : Type ?u.72759
ι : Type ?u.72762
α : Type ?u.72765
β : Type ?u.72768
K : Type u_1
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioc ↑a ↑b ↔ x ∈ Ioc a b
F : Type ?u.72759
ι : Type ?u.72762
α : Type ?u.72765
β : Type ?u.72768
K : Type u_1
inst✝ : LinearOrderedField K
a b : ℚ
⊢ Rat.cast ⁻¹' Ioc ↑a ↑b = Ioc a b
ext x
no goals
case h
F : Type ?u.72759
ι : Type ?u.72762
α : Type ?u.72765
β : Type ?u.72768
K : Type u_1
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioc ↑a ↑b ↔ x ∈ Ioc a b
simp