Changes
7 changed files (+76/-21)
-
.devcontainer/Dockerfile (new)
-
@@ -0,0 +1,8 @@FROM mcr.microsoft.com/devcontainers/base:jammy USER vscode WORKDIR /home/vscode RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none ENV PATH="/home/vscode/.elan/bin:${PATH}"
-
-
-
@@ -0,0 +1,15 @@{ "name": "MIL dev container", "build": { "dockerfile": "Dockerfile" }, "onCreateCommand": "echo \"Downloading the Lean 4 mathematical library...\" && lake exe cache get! && lake build +MIL.Common && echo \"Finished setup! Open a file using the Explorer in the top-left of your screen.\"", "customizations": { "vscode" : { "extensions" : [ "leanprover.lean4" ] } } }
-
-
-
@@ -6,17 +6,18 @@"**/.DS_yml": true, "**/.gitpod.yml": true, "**/.vscode": true, ".docker": true, "build": true, "html": true, "lake-packages": true, ".gitignore": true, "lake-manifest.json": true, "lakefile.lean": true, "lean-toolchain": true, "mathematics_in_lean.pdf": true, "MIL.lean": true, "README.md":true, ".devcontainer.json": true, ".docker": true, "build": true, "html": true, "lake-packages": true, ".gitignore": true, "lake-manifest.json": true, "lakefile.lean": true, "lean-toolchain": true, "mathematics_in_lean.pdf": true, "MIL.lean": true, "README.md":true, }, "editor.minimap.enabled": false, "editor.acceptSuggestionOnEnter": "off",
-
-
-
@@ -111,11 +111,9 @@ example : 2 * a * b ≤ a ^ 2 + b ^ 2 := bycalc 2 * a * b = 2 * a * b + 0 := by ring _ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) := add_le_add (le_refl _) h _ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) := add_le_add (le_refl _) h _ = a ^ 2 + b ^ 2 := by ring example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2 calc
-
-
-
@@ -9,7 +9,7 @@ or as aThe book is designed to be read as you work through examples and exercises, using a copy of this repository on your computer. Alternatively, you can use Gitpod to run Lean and VS Code in the cloud. Alternatively, you can use Github Codespaces or Gitpod to run Lean and VS Code in the cloud. This version of *Mathematics in Lean* is designed for [Lean 4](https://leanprover.github.io/) and [Mathlib](https://github.com/leanprover-community/mathlib4).
-
@@ -53,16 +53,48 @@ followed by `lake exe cache get` inside the `mathematics_in_lean` folder.which is why we suggested making a copy.) ## To use this repository with Github Codespaces If you have trouble installing Lean, you can use Lean directly in your browser using Github Codespaces. This requires a Github account. If you are signed in to Github, click here: <a href='https://codespaces.new/leanprover-community/mathematics_in_lean' target="_blank" rel="noreferrer noopener"><img src='https://github.com/codespaces/badge.svg' alt='Open in GitHub Codespaces' style='max-width: 100%;'></a> Make sure the Machine type is `4-core`, and then press `Create codespace` (this might take a few minutes). This creates a virtual machine in the cloud, and installs Lean and Mathlib. Opening any `.lean` file in the MIL folder will start Lean, though this may also take a little while. We suggest making a copy of the `MIL` directory, as described in the instructions above for using MIL on your computer. You can update the repository by opening a terminal in the browser and typing `git pull` followed by `lake exe cache get` as above. Codespaces offers a certain number of free hours per month. When you are done working, press `Ctrl/Cmd+Shift+P` on your keyboard, start typing `stop codespace`, and then select `Codespaces: Stop Codespace` from the list of options. If you forget, don't worry: the virtual machine will stop itself after a certain amount of time of inactivity. To restart a previous workspace, visit <https://github.com/codespaces>. ## To use this repository with Gitpod Gitpod is an alternative to Github Codespaces, but is a little less convenient, since it requires you to verify your phone number. If you have a Gitpod account or are willing to sign up for one, just point your browser to [https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). point your browser to [https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). This creates a virtual machine in the cloud, and installs Lean and Mathlib. It then presents you with a VS Code window, running in a virtual copy of the repository. We still suggest making a copy of the `MIL` directory, as described in step 5 in the last section. We suggest making a copy of the `MIL` directory, as described in the instructions above for using MIL on your computer. You can update the repository by opening a terminal in the browser and typing `git pull` followed by `lake exe cache get` as above.
-
@@ -72,7 +104,9 @@ The workspace should also stop automatically30 minutes after the last interaction or 3 minutes after closing the tab. To restart a previous workspace, go to [https://gitpod.io/workspaces/](https://gitpod.io/workspaces/). If you change the filter from Active to All, you will see all your recent workspaces. You can pin a workspace to keep it on the list of active ones. If you change the filter from Active to All, you will see all your recent workspaces. You can pin a workspace to keep it on the list of active ones. ## Contributing
-
-
-
@@ -932,8 +932,7 @@ can also finish the job.</p><span class="k">calc</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span> <span class="n">_</span> <span class="bp">≤</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="o">(</span><span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="n">add_le_add</span> <span class="o">(</span><span class="n">le_refl</span> <span class="n">_</span><span class="o">)</span> <span class="n">h</span> <span class="n">_</span> <span class="bp">≤</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="o">(</span><span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="n">add_le_add</span> <span class="o">(</span><span class="n">le_refl</span> <span class="n">_</span><span class="o">)</span> <span class="n">h</span> <span class="n">_</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span> </pre></div> </div>
-
-