α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ (∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f
simp only [mem_iff_get, Set.mem_range, get_ofFn]
no goals
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ (∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a
exact ⟨fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩⟩
no goals
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a
i : Fin (length (ofFn f))
hi : f (↑(Fin.cast (_ : length (ofFn f) = n)) i) = a
⊢ length (ofFn f) = n
simp
no goals
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ y, f y = a
i : Fin n
hi : f i = a
⊢ n = length (ofFn f)
simp