case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))

case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α : Type u
n : ℕ
f : Fin (succ n) → α
⊢ ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
induction' n with n IH
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ [f 0] = [f (Fin.last zero)]
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero]
no goals
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ [f 0] = [f (Fin.last zero)]
rfl
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ f 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =
    f 0 :: concat (ofFn fun i => f (↑Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n)))
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero]
no goals
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ f 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =
    f 0 :: concat (ofFn fun i => f (↑Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n)))
congr