case a
α : Type ?u.10
β : Type ?u.13
n a✝ : ℕ
⊢ a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n
α : Type ?u.10
β : Type ?u.13
n : ℕ
⊢ map valEmbedding univ = Iio n
ext
no goals
case a
α : Type ?u.10
β : Type ?u.13
n a✝ : ℕ
⊢ a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n
simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]