n✝ : ℕ
α✝ : Type ?u.39247
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i => f (Fin.succ i))
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i => f (Fin.succ i))
n✝ : ℕ
α✝ : Type ?u.39247
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i => pure (f i)) = pure (ofFn f)
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
no goals
n✝ : ℕ
α✝ : Type ?u.39247
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i => f (Fin.succ i))
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i => f (Fin.succ i))
simp