case h
F : Type ?u.77511
ι : Type ?u.77514
α : Type ?u.77517
β : Type ?u.77520
K : Type u_1
inst✝ : LinearOrderedField K
a x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Iic ↑a ↔ x ∈ Iic a
F : Type ?u.77511
ι : Type ?u.77514
α : Type ?u.77517
β : Type ?u.77520
K : Type u_1
inst✝ : LinearOrderedField K
a : ℚ
⊢ Rat.cast ⁻¹' Iic ↑a = Iic a
ext x
no goals
case h
F : Type ?u.77511
ι : Type ?u.77514
α : Type ?u.77517
β : Type ?u.77520
K : Type u_1
inst✝ : LinearOrderedField K
a x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Iic ↑a ↔ x ∈ Iic a
simp