message: doc: then it has to be an external link, cannot play the video inline on github, rats.
diff: @@ -4,9 +4,7 @@ This extension provides VSCode editor support for the Lean 4 programming languag
  all new [Language Server](https://docs.microsoft.com/en-us/visualstudio/extensibility/language-server-protocol)
  implemented in Lean.
  -<div>
  -<video src="https://leanassets.blob.core.windows.net/videos/Getting%20Started%20with%20Lean%204%20in%20Visual%20Studio%20Code.mp4" style="width:1024px;" controls></video>
  -</div>
  +See [Quick Start Demo Video](https://www.youtube.com/watch?v=yZo6k48L0VY).
  ## Installing the extension and Lean 4
  1. Install the extension from the [marketplace](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4).
  