no goals
α : Type u
n : ℕ
f : Fin (succ n) → α
⊢ length (ofFn f) = length (f 0 :: ofFn fun i => f (Fin.succ i))
simp
case zero
α : Type u
n : ℕ
f : Fin (succ n) → α
hi₁ : zero < length (ofFn f)
hi₂ : zero < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }

case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
α : Type u
n : ℕ
f : Fin (succ n) → α
i : ℕ
hi₁ : i < length (ofFn f)
hi₂ : i < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := i, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := i, isLt := hi₂ }
cases i
case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
case zero
α : Type u
n : ℕ
f : Fin (succ n) → α
hi₁ : zero < length (ofFn f)
hi₂ : zero < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }

case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
. simp
no goals
case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
. simp
no goals
case zero
α : Type u
n : ℕ
f : Fin (succ n) → α
hi₁ : zero < length (ofFn f)
hi₂ : zero < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }
simp
no goals
case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
simp