case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)

case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
f : Fin (m + succ n) → α
⊢ ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α : Type u
m n : ℕ
f : Fin (m + n) → α
⊢ ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
induction' n with n IH
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = ofFn fun i => f (↑(OrderIso.refl (Fin m)) i)
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
rw [ofFn_zero, append_nil, Fin.castAdd_zero, Fin.cast_refl]
no goals
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = ofFn fun i => f (↑(OrderIso.refl (Fin m)) i)
rfl
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
f : Fin (m + succ n) → α
⊢ concat ((ofFn fun i => f (↑Fin.castSucc (↑(Fin.castAdd n) i))) ++ ofFn fun j => f (↑Fin.castSucc (↑(Fin.natAdd m) j)))
      (f (Fin.last (Nat.add m n))) =
    concat ((ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun i => f (↑(Fin.natAdd m) (↑Fin.castSucc i)))
      (f (↑(Fin.natAdd m) (Fin.last n)))
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
f : Fin (m + succ n) → α
⊢ ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
rw [ofFn_succ', ofFn_succ', IH, append_concat]
no goals
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
f : Fin (m + succ n) → α
⊢ concat ((ofFn fun i => f (↑Fin.castSucc (↑(Fin.castAdd n) i))) ++ ofFn fun j => f (↑Fin.castSucc (↑(Fin.natAdd m) j)))
      (f (Fin.last (Nat.add m n))) =
    concat ((ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun i => f (↑(Fin.natAdd m) (↑Fin.castSucc i)))
      (f (↑(Fin.natAdd m) (Fin.last n)))
rfl