rintro ⟨a, ha, v, hv, rfl⟩ i
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) → ∀ (i : Fin (n + 1)), w.get i ∈ v i
case intro.intro.intro.intro
α : Type u_1
n : ℕ
v✝ : Fin (n + 1) →. α
a : α
ha : a ∈ v✝ 0
v : Vector α n
hv : ∀ (i : Fin n), v.get i ∈ v✝ i.succ
i : Fin (n + 1)
⊢ (a ::ᵥ v).get i ∈ v✝ i