case e_a
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ get (tail (ofFn f)) = fun i => f (Fin.succ i)
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ ofFn (get (tail (ofFn f))) = ofFn fun i => f (Fin.succ i)
congr
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ get (tail (ofFn f)) i = f (Fin.succ i)
case e_a
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ get (tail (ofFn f)) = fun i => f (Fin.succ i)
funext i
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ f { val := ↑i + 1, isLt := (_ : ↑i + 1 < Nat.succ n) } = f (Fin.succ i)
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ get (tail (ofFn f)) i = f (Fin.succ i)
rw [get_tail, get_ofFn]
no goals
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ f { val := ↑i + 1, isLt := (_ : ↑i + 1 < Nat.succ n) } = f (Fin.succ i)
rfl