case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } =
    get x { val := ↑{ val := i, isLt := ih } + 1, isLt := (_ : ↑{ val := i, isLt := ih } + 1 < n) }
n : ℕ
α : Type u_1
x : Vector α n
i : Fin (n - 1)
⊢ get (tail x) i = get x { val := ↑i + 1, isLt := (_ : ↑i + 1 < n) }
cases' i with i ih
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } = get x { val := i + 1, isLt := (_ : i + 1 < n) }
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } =
    get x { val := ↑{ val := i, isLt := ih } + 1, isLt := (_ : ↑{ val := i, isLt := ih } + 1 < n) }
dsimp
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } = get x { val := i + 1, isLt := (_ : i + 1 < n) }
rcases x with ⟨_ | _, h⟩ <;> try rfl
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
rw [List.length] at h
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih✝ } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
rw [←h] at ih
no goals
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih✝ } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
contradiction
no goals
case mk.mk.cons
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : List.length (head✝ :: tail✝) = n
⊢ get (tail { val := head✝ :: tail✝, property := h }) { val := i, isLt := ih } =
    get { val := head✝ :: tail✝, property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
rfl