case a
n : ℕ
a b : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioi a) = Ioc (↑a) (n - 1)
ext x
case a
n : ℕ
a b : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1
case a
n : ℕ
a b : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)
simp only [exists_prop, Embedding.coe_subtype, mem_Ioi, mem_map, mem_Ioc]
case a.mp
n : ℕ
a b : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) → ↑a < x ∧ x ≤ n - 1

case a.mpr
n : ℕ
a b : Fin n
x : ℕ
⊢ ↑a < x ∧ x ≤ n - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
case a
n : ℕ
a b : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1
constructor
case a.mpr.zero
x : ℕ
a b : Fin Nat.zero
⊢ ↑a < x ∧ x ≤ Nat.zero - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x

case a.mpr.succ
x n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ ↑a < x ∧ x ≤ Nat.succ n✝ - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
case a.mpr
n : ℕ
a b : Fin n
x : ℕ
⊢ ↑a < x ∧ x ≤ n - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
cases n
case a.mp.intro.intro
n : ℕ
a b x : Fin n
hx : a < x
⊢ ↑a < ↑valEmbedding x ∧ ↑valEmbedding x ≤ n - 1
case a.mp
n : ℕ
a b : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ ↑valEmbedding a_1 = x) → ↑a < x ∧ x ≤ n - 1
rintro ⟨x, hx, rfl⟩
no goals
case a.mp.intro.intro
n : ℕ
a b x : Fin n
hx : a < x
⊢ ↑a < ↑valEmbedding x ∧ ↑valEmbedding x ≤ n - 1
exact ⟨hx, le_tsub_of_add_le_right <| x.2⟩
no goals
case a.mpr.zero
x : ℕ
a b : Fin Nat.zero
⊢ ↑a < x ∧ x ≤ Nat.zero - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
exact Fin.elim0 a
no goals
case a.mpr.succ
x n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ ↑a < x ∧ x ≤ Nat.succ n✝ - 1 → ∃ a_2, a < a_2 ∧ ↑valEmbedding a_2 = x
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩