diff --git a/client/src/components/Markdown.tsx b/client/src/components/Markdown.tsx
index 2380bda..b441f00 100644
--- a/client/src/components/Markdown.tsx
+++ b/client/src/components/Markdown.tsx
@@ -3,11 +3,12 @@ import ReactMarkdown from 'react-markdown';
 import remarkMath from 'remark-math'
 import rehypeKatex from 'rehype-katex'
 import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
+import gfm from "remark-gfm";
 
 function Markdown(props) {
     const newProps = {
         ...props,
-        remarkPlugins: [...props.remarkPlugins ?? [], remarkMath],
+        remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
         rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex],
       };
       return (
diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx
index 7aeb317..0409b3e 100644
--- a/client/src/components/TacticState.tsx
+++ b/client/src/components/TacticState.tsx
@@ -102,6 +102,7 @@ function TacticState({ goals, diagnostics, completed }) {
   const hasManyGoal = hasGoal && goals.length > 1
   return (
     <Box sx={{ height: "100%" }}>
+      {completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
       {hasGoal &&
         <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
           <Typography variant="h5">Main Goal
@@ -114,7 +115,6 @@ function TacticState({ goals, diagnostics, completed }) {
           No goals
           (at <FontAwesomeIcon icon={faArrowPointer}></FontAwesomeIcon>)
         </Typography>}
-      {completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
       {hasError &&
         <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
           <Typography variant="h5" sx={{ mb: 2 }}>Lean says</Typography>
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 29f71e0..ed7b804 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -48,6 +48,30 @@
   white-space: normal;
 }
 
+/* TODO: Adjust Mathjax styling. 1em vertical is excessive. */
+mjx-container[jax="CHTML"][display="true"] {
+  margin: 0.2em 0 !important;
+}
+
+
+/* Styling tables for Markdown */
+.message-panel table, .message-panel th, .message-panel td {
+  /* border: 1px solid rgb(0, 0, 0, 0.12); */
+  border-collapse: collapse;
+}
+
+.message-panel th, .message-panel td {
+  padding-left: .5em;
+  padding-right: .5em;
+}
+
+p, table {
+  margin-block-start: 1em;
+  margin-block-end: 1em;
+  margin-inline-start: 0px;
+  margin-inline-end: 0px;
+}
+
 /***************************************/
 /* TODO: For development purposes only */
 /***************************************/
diff --git a/package-lock.json b/package-lock.json
index 96b6298..45f46c5 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -26,6 +26,7 @@
         "react-redux": "^8.0.5",
         "react-router-dom": "^6.4.4",
         "rehype-katex": "^6.0.2",
+        "remark-gfm": "^3.0.1",
         "remark-math": "^5.1.1",
         "vscode-ws-jsonrpc": "^2.0.0",
         "ws": "^8.9.0"
@@ -3132,6 +3133,15 @@
         }
       ]
     },
+    "node_modules/ccount": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/ccount/-/ccount-2.0.1.tgz",
+      "integrity": "sha512-eyrF0jiFpY+3drT6383f1qhkbGsLSifNAjA61IUjZjmLCWjItY6LB9ft9YhoDgwfmclB2zhu51Lc7+95b8NRAg==",
+      "funding": {
+        "type": "github",
+        "url": "https://github.com/sponsors/wooorm"
+      }
+    },
     "node_modules/chalk": {
       "version": "2.4.2",
       "resolved": "https://registry.npmjs.org/chalk/-/chalk-2.4.2.tgz",
@@ -5376,6 +5386,15 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
+    "node_modules/markdown-table": {
+      "version": "3.0.3",
+      "resolved": "https://registry.npmjs.org/markdown-table/-/markdown-table-3.0.3.tgz",
+      "integrity": "sha512-Z1NL3Tb1M9wH4XESsCDEksWoKTdlUafKc4pt0GRwjUyXaCFZ+dc3g2erqB6zm3szA2IUSi7VnPI+o/9jnxh9hw==",
+      "funding": {
+        "type": "github",
+        "url": "https://github.com/sponsors/wooorm"
+      }
+    },
     "node_modules/marked": {
       "version": "4.2.3",
       "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.3.tgz",
@@ -5401,6 +5420,31 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/mdast-util-find-and-replace": {
+      "version": "2.2.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-find-and-replace/-/mdast-util-find-and-replace-2.2.1.tgz",
+      "integrity": "sha512-SobxkQXFAdd4b5WmEakmkVoh18icjQRxGy5OWTCzgsLRm1Fu/KCtwD1HIQSsmq5ZRjVH0Ehwg6/Fn3xIUk+nKw==",
+      "dependencies": {
+        "escape-string-regexp": "^5.0.0",
+        "unist-util-is": "^5.0.0",
+        "unist-util-visit-parents": "^5.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/mdast-util-find-and-replace/node_modules/escape-string-regexp": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/escape-string-regexp/-/escape-string-regexp-5.0.0.tgz",
+      "integrity": "sha512-/veY75JbMK4j1yjvuUxuVsiS/hr/4iHs9FTT6cgTexxdE0Ly/glccBAkloH/DofkjRbZU3bnoj38mOmhkZ0lHw==",
+      "engines": {
+        "node": ">=12"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/sindresorhus"
+      }
+    },
     "node_modules/mdast-util-from-markdown": {
       "version": "1.2.0",
       "resolved": "https://registry.npmjs.org/mdast-util-from-markdown/-/mdast-util-from-markdown-1.2.0.tgz",
@@ -5424,6 +5468,94 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/mdast-util-gfm": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm/-/mdast-util-gfm-2.0.1.tgz",
+      "integrity": "sha512-42yHBbfWIFisaAfV1eixlabbsa6q7vHeSPY+cg+BBjX51M8xhgMacqH9g6TftB/9+YkcI0ooV4ncfrJslzm/RQ==",
+      "dependencies": {
+        "mdast-util-from-markdown": "^1.0.0",
+        "mdast-util-gfm-autolink-literal": "^1.0.0",
+        "mdast-util-gfm-footnote": "^1.0.0",
+        "mdast-util-gfm-strikethrough": "^1.0.0",
+        "mdast-util-gfm-table": "^1.0.0",
+        "mdast-util-gfm-task-list-item": "^1.0.0",
+        "mdast-util-to-markdown": "^1.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/mdast-util-gfm-autolink-literal": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-autolink-literal/-/mdast-util-gfm-autolink-literal-1.0.2.tgz",
+      "integrity": "sha512-FzopkOd4xTTBeGXhXSBU0OCDDh5lUj2rd+HQqG92Ld+jL4lpUfgX2AT2OHAVP9aEeDKp7G92fuooSZcYJA3cRg==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "ccount": "^2.0.0",
+        "mdast-util-find-and-replace": "^2.0.0",
+        "micromark-util-character": "^1.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/mdast-util-gfm-footnote": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-footnote/-/mdast-util-gfm-footnote-1.0.1.tgz",
+      "integrity": "sha512-p+PrYlkw9DeCRkTVw1duWqPRHX6Ywh2BNKJQcZbCwAuP/59B0Lk9kakuAd7KbQprVO4GzdW8eS5++A9PUSqIyw==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-to-markdown": "^1.3.0",
+        "micromark-util-normalize-identifier": "^1.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/mdast-util-gfm-strikethrough": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-strikethrough/-/mdast-util-gfm-strikethrough-1.0.2.tgz",
+      "integrity": "sha512-T/4DVHXcujH6jx1yqpcAYYwd+z5lAYMw4Ls6yhTfbMMtCt0PHY4gEfhW9+lKsLBtyhUGKRIzcUA2FATVqnvPDA==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-to-markdown": "^1.3.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/mdast-util-gfm-table": {
+      "version": "1.0.6",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-table/-/mdast-util-gfm-table-1.0.6.tgz",
+      "integrity": "sha512-uHR+fqFq3IvB3Rd4+kzXW8dmpxUhvgCQZep6KdjsLK4O6meK5dYZEayLtIxNus1XO3gfjfcIFe8a7L0HZRGgag==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "markdown-table": "^3.0.0",
+        "mdast-util-from-markdown": "^1.0.0",
+        "mdast-util-to-markdown": "^1.3.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/mdast-util-gfm-task-list-item": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-task-list-item/-/mdast-util-gfm-task-list-item-1.0.1.tgz",
+      "integrity": "sha512-KZ4KLmPdABXOsfnM6JHUIjxEvcx2ulk656Z/4Balw071/5qgnhz+H1uGtf2zIGnrnvDC8xR4Fj9uKbjAFGNIeA==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-to-markdown": "^1.3.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/mdast-util-math": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/mdast-util-math/-/mdast-util-math-2.0.1.tgz",
@@ -5591,6 +5723,121 @@
         "uvu": "^0.5.0"
       }
     },
+    "node_modules/micromark-extension-gfm": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm/-/micromark-extension-gfm-2.0.1.tgz",
+      "integrity": "sha512-p2sGjajLa0iYiGQdT0oelahRYtMWvLjy8J9LOCxzIQsllMCGLbsLW+Nc+N4vi02jcRJvedVJ68cjelKIO6bpDA==",
+      "dependencies": {
+        "micromark-extension-gfm-autolink-literal": "^1.0.0",
+        "micromark-extension-gfm-footnote": "^1.0.0",
+        "micromark-extension-gfm-strikethrough": "^1.0.0",
+        "micromark-extension-gfm-table": "^1.0.0",
+        "micromark-extension-gfm-tagfilter": "^1.0.0",
+        "micromark-extension-gfm-task-list-item": "^1.0.0",
+        "micromark-util-combine-extensions": "^1.0.0",
+        "micromark-util-types": "^1.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/micromark-extension-gfm-autolink-literal": {
+      "version": "1.0.3",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-autolink-literal/-/micromark-extension-gfm-autolink-literal-1.0.3.tgz",
+      "integrity": "sha512-i3dmvU0htawfWED8aHMMAzAVp/F0Z+0bPh3YrbTPPL1v4YAlCZpy5rBO5p0LPYiZo0zFVkoYh7vDU7yQSiCMjg==",
+      "dependencies": {
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-sanitize-uri": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/micromark-extension-gfm-footnote": {
+      "version": "1.0.4",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-footnote/-/micromark-extension-gfm-footnote-1.0.4.tgz",
+      "integrity": "sha512-E/fmPmDqLiMUP8mLJ8NbJWJ4bTw6tS+FEQS8CcuDtZpILuOb2kjLqPEeAePF1djXROHXChM/wPJw0iS4kHCcIg==",
+      "dependencies": {
+        "micromark-core-commonmark": "^1.0.0",
+        "micromark-factory-space": "^1.0.0",
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-normalize-identifier": "^1.0.0",
+        "micromark-util-sanitize-uri": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/micromark-extension-gfm-strikethrough": {
+      "version": "1.0.4",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-strikethrough/-/micromark-extension-gfm-strikethrough-1.0.4.tgz",
+      "integrity": "sha512-/vjHU/lalmjZCT5xt7CcHVJGq8sYRm80z24qAKXzaHzem/xsDYb2yLL+NNVbYvmpLx3O7SYPuGL5pzusL9CLIQ==",
+      "dependencies": {
+        "micromark-util-chunked": "^1.0.0",
+        "micromark-util-classify-character": "^1.0.0",
+        "micromark-util-resolve-all": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/micromark-extension-gfm-table": {
+      "version": "1.0.5",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-table/-/micromark-extension-gfm-table-1.0.5.tgz",
+      "integrity": "sha512-xAZ8J1X9W9K3JTJTUL7G6wSKhp2ZYHrFk5qJgY/4B33scJzE2kpfRL6oiw/veJTbt7jiM/1rngLlOKPWr1G+vg==",
+      "dependencies": {
+        "micromark-factory-space": "^1.0.0",
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/micromark-extension-gfm-tagfilter": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-tagfilter/-/micromark-extension-gfm-tagfilter-1.0.1.tgz",
+      "integrity": "sha512-Ty6psLAcAjboRa/UKUbbUcwjVAv5plxmpUTy2XC/3nJFL37eHej8jrHrRzkqcpipJliuBH30DTs7+3wqNcQUVA==",
+      "dependencies": {
+        "micromark-util-types": "^1.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/micromark-extension-gfm-task-list-item": {
+      "version": "1.0.3",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-task-list-item/-/micromark-extension-gfm-task-list-item-1.0.3.tgz",
+      "integrity": "sha512-PpysK2S1Q/5VXi72IIapbi/jliaiOFzv7THH4amwXeYXLq3l1uo8/2Be0Ac1rEwK20MQEsGH2ltAZLNY2KI/0Q==",
+      "dependencies": {
+        "micromark-factory-space": "^1.0.0",
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/micromark-extension-math": {
       "version": "2.0.2",
       "resolved": "https://registry.npmjs.org/micromark-extension-math/-/micromark-extension-math-2.0.2.tgz",
@@ -7242,6 +7489,21 @@
       "resolved": "https://registry.npmjs.org/parse5/-/parse5-6.0.1.tgz",
       "integrity": "sha512-Ofn/CTFzRGTTxwpNEs9PP93gXShHcTq255nzRYSKe8AkVpZY7e1fpmTfOyoIvjP5HG7Z2ZM7VS9PPhQGW2pOpw=="
     },
+    "node_modules/remark-gfm": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/remark-gfm/-/remark-gfm-3.0.1.tgz",
+      "integrity": "sha512-lEFDoi2PICJyNrACFOfDD3JlLkuSbOa5Wd8EPt06HUdptv8Gn0bxYTdbU/XXQ3swAPkEaGxxPN9cbnMHvVu1Ig==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-gfm": "^2.0.0",
+        "micromark-extension-gfm": "^2.0.0",
+        "unified": "^10.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/remark-math": {
       "version": "5.1.1",
       "resolved": "https://registry.npmjs.org/remark-math/-/remark-math-5.1.1.tgz",
@@ -11382,6 +11644,11 @@
       "integrity": "sha512-OnyeJ9ascFA9roEj72ok2Ikp7PHJTKubtEJIQ/VK3fdsS50q4KWy+Z5X0A1/GswEItKX0ctAp8n4SYDE7wTu6A==",
       "dev": true
     },
+    "ccount": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/ccount/-/ccount-2.0.1.tgz",
+      "integrity": "sha512-eyrF0jiFpY+3drT6383f1qhkbGsLSifNAjA61IUjZjmLCWjItY6LB9ft9YhoDgwfmclB2zhu51Lc7+95b8NRAg=="
+    },
     "chalk": {
       "version": "2.4.2",
       "resolved": "https://registry.npmjs.org/chalk/-/chalk-2.4.2.tgz",
@@ -13038,6 +13305,11 @@
         "semver": "^6.0.0"
       }
     },
+    "markdown-table": {
+      "version": "3.0.3",
+      "resolved": "https://registry.npmjs.org/markdown-table/-/markdown-table-3.0.3.tgz",
+      "integrity": "sha512-Z1NL3Tb1M9wH4XESsCDEksWoKTdlUafKc4pt0GRwjUyXaCFZ+dc3g2erqB6zm3szA2IUSi7VnPI+o/9jnxh9hw=="
+    },
     "marked": {
       "version": "4.2.3",
       "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.3.tgz",
@@ -13053,6 +13325,23 @@
         "unist-util-visit": "^4.0.0"
       }
     },
+    "mdast-util-find-and-replace": {
+      "version": "2.2.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-find-and-replace/-/mdast-util-find-and-replace-2.2.1.tgz",
+      "integrity": "sha512-SobxkQXFAdd4b5WmEakmkVoh18icjQRxGy5OWTCzgsLRm1Fu/KCtwD1HIQSsmq5ZRjVH0Ehwg6/Fn3xIUk+nKw==",
+      "requires": {
+        "escape-string-regexp": "^5.0.0",
+        "unist-util-is": "^5.0.0",
+        "unist-util-visit-parents": "^5.0.0"
+      },
+      "dependencies": {
+        "escape-string-regexp": {
+          "version": "5.0.0",
+          "resolved": "https://registry.npmjs.org/escape-string-regexp/-/escape-string-regexp-5.0.0.tgz",
+          "integrity": "sha512-/veY75JbMK4j1yjvuUxuVsiS/hr/4iHs9FTT6cgTexxdE0Ly/glccBAkloH/DofkjRbZU3bnoj38mOmhkZ0lHw=="
+        }
+      }
+    },
     "mdast-util-from-markdown": {
       "version": "1.2.0",
       "resolved": "https://registry.npmjs.org/mdast-util-from-markdown/-/mdast-util-from-markdown-1.2.0.tgz",
@@ -13072,6 +13361,70 @@
         "uvu": "^0.5.0"
       }
     },
+    "mdast-util-gfm": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm/-/mdast-util-gfm-2.0.1.tgz",
+      "integrity": "sha512-42yHBbfWIFisaAfV1eixlabbsa6q7vHeSPY+cg+BBjX51M8xhgMacqH9g6TftB/9+YkcI0ooV4ncfrJslzm/RQ==",
+      "requires": {
+        "mdast-util-from-markdown": "^1.0.0",
+        "mdast-util-gfm-autolink-literal": "^1.0.0",
+        "mdast-util-gfm-footnote": "^1.0.0",
+        "mdast-util-gfm-strikethrough": "^1.0.0",
+        "mdast-util-gfm-table": "^1.0.0",
+        "mdast-util-gfm-task-list-item": "^1.0.0",
+        "mdast-util-to-markdown": "^1.0.0"
+      }
+    },
+    "mdast-util-gfm-autolink-literal": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-autolink-literal/-/mdast-util-gfm-autolink-literal-1.0.2.tgz",
+      "integrity": "sha512-FzopkOd4xTTBeGXhXSBU0OCDDh5lUj2rd+HQqG92Ld+jL4lpUfgX2AT2OHAVP9aEeDKp7G92fuooSZcYJA3cRg==",
+      "requires": {
+        "@types/mdast": "^3.0.0",
+        "ccount": "^2.0.0",
+        "mdast-util-find-and-replace": "^2.0.0",
+        "micromark-util-character": "^1.0.0"
+      }
+    },
+    "mdast-util-gfm-footnote": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-footnote/-/mdast-util-gfm-footnote-1.0.1.tgz",
+      "integrity": "sha512-p+PrYlkw9DeCRkTVw1duWqPRHX6Ywh2BNKJQcZbCwAuP/59B0Lk9kakuAd7KbQprVO4GzdW8eS5++A9PUSqIyw==",
+      "requires": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-to-markdown": "^1.3.0",
+        "micromark-util-normalize-identifier": "^1.0.0"
+      }
+    },
+    "mdast-util-gfm-strikethrough": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-strikethrough/-/mdast-util-gfm-strikethrough-1.0.2.tgz",
+      "integrity": "sha512-T/4DVHXcujH6jx1yqpcAYYwd+z5lAYMw4Ls6yhTfbMMtCt0PHY4gEfhW9+lKsLBtyhUGKRIzcUA2FATVqnvPDA==",
+      "requires": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-to-markdown": "^1.3.0"
+      }
+    },
+    "mdast-util-gfm-table": {
+      "version": "1.0.6",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-table/-/mdast-util-gfm-table-1.0.6.tgz",
+      "integrity": "sha512-uHR+fqFq3IvB3Rd4+kzXW8dmpxUhvgCQZep6KdjsLK4O6meK5dYZEayLtIxNus1XO3gfjfcIFe8a7L0HZRGgag==",
+      "requires": {
+        "@types/mdast": "^3.0.0",
+        "markdown-table": "^3.0.0",
+        "mdast-util-from-markdown": "^1.0.0",
+        "mdast-util-to-markdown": "^1.3.0"
+      }
+    },
+    "mdast-util-gfm-task-list-item": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-task-list-item/-/mdast-util-gfm-task-list-item-1.0.1.tgz",
+      "integrity": "sha512-KZ4KLmPdABXOsfnM6JHUIjxEvcx2ulk656Z/4Balw071/5qgnhz+H1uGtf2zIGnrnvDC8xR4Fj9uKbjAFGNIeA==",
+      "requires": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-to-markdown": "^1.3.0"
+      }
+    },
     "mdast-util-math": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/mdast-util-math/-/mdast-util-math-2.0.1.tgz",
@@ -13194,6 +13547,93 @@
         "uvu": "^0.5.0"
       }
     },
+    "micromark-extension-gfm": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm/-/micromark-extension-gfm-2.0.1.tgz",
+      "integrity": "sha512-p2sGjajLa0iYiGQdT0oelahRYtMWvLjy8J9LOCxzIQsllMCGLbsLW+Nc+N4vi02jcRJvedVJ68cjelKIO6bpDA==",
+      "requires": {
+        "micromark-extension-gfm-autolink-literal": "^1.0.0",
+        "micromark-extension-gfm-footnote": "^1.0.0",
+        "micromark-extension-gfm-strikethrough": "^1.0.0",
+        "micromark-extension-gfm-table": "^1.0.0",
+        "micromark-extension-gfm-tagfilter": "^1.0.0",
+        "micromark-extension-gfm-task-list-item": "^1.0.0",
+        "micromark-util-combine-extensions": "^1.0.0",
+        "micromark-util-types": "^1.0.0"
+      }
+    },
+    "micromark-extension-gfm-autolink-literal": {
+      "version": "1.0.3",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-autolink-literal/-/micromark-extension-gfm-autolink-literal-1.0.3.tgz",
+      "integrity": "sha512-i3dmvU0htawfWED8aHMMAzAVp/F0Z+0bPh3YrbTPPL1v4YAlCZpy5rBO5p0LPYiZo0zFVkoYh7vDU7yQSiCMjg==",
+      "requires": {
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-sanitize-uri": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      }
+    },
+    "micromark-extension-gfm-footnote": {
+      "version": "1.0.4",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-footnote/-/micromark-extension-gfm-footnote-1.0.4.tgz",
+      "integrity": "sha512-E/fmPmDqLiMUP8mLJ8NbJWJ4bTw6tS+FEQS8CcuDtZpILuOb2kjLqPEeAePF1djXROHXChM/wPJw0iS4kHCcIg==",
+      "requires": {
+        "micromark-core-commonmark": "^1.0.0",
+        "micromark-factory-space": "^1.0.0",
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-normalize-identifier": "^1.0.0",
+        "micromark-util-sanitize-uri": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      }
+    },
+    "micromark-extension-gfm-strikethrough": {
+      "version": "1.0.4",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-strikethrough/-/micromark-extension-gfm-strikethrough-1.0.4.tgz",
+      "integrity": "sha512-/vjHU/lalmjZCT5xt7CcHVJGq8sYRm80z24qAKXzaHzem/xsDYb2yLL+NNVbYvmpLx3O7SYPuGL5pzusL9CLIQ==",
+      "requires": {
+        "micromark-util-chunked": "^1.0.0",
+        "micromark-util-classify-character": "^1.0.0",
+        "micromark-util-resolve-all": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      }
+    },
+    "micromark-extension-gfm-table": {
+      "version": "1.0.5",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-table/-/micromark-extension-gfm-table-1.0.5.tgz",
+      "integrity": "sha512-xAZ8J1X9W9K3JTJTUL7G6wSKhp2ZYHrFk5qJgY/4B33scJzE2kpfRL6oiw/veJTbt7jiM/1rngLlOKPWr1G+vg==",
+      "requires": {
+        "micromark-factory-space": "^1.0.0",
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      }
+    },
+    "micromark-extension-gfm-tagfilter": {
+      "version": "1.0.1",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-tagfilter/-/micromark-extension-gfm-tagfilter-1.0.1.tgz",
+      "integrity": "sha512-Ty6psLAcAjboRa/UKUbbUcwjVAv5plxmpUTy2XC/3nJFL37eHej8jrHrRzkqcpipJliuBH30DTs7+3wqNcQUVA==",
+      "requires": {
+        "micromark-util-types": "^1.0.0"
+      }
+    },
+    "micromark-extension-gfm-task-list-item": {
+      "version": "1.0.3",
+      "resolved": "https://registry.npmjs.org/micromark-extension-gfm-task-list-item/-/micromark-extension-gfm-task-list-item-1.0.3.tgz",
+      "integrity": "sha512-PpysK2S1Q/5VXi72IIapbi/jliaiOFzv7THH4amwXeYXLq3l1uo8/2Be0Ac1rEwK20MQEsGH2ltAZLNY2KI/0Q==",
+      "requires": {
+        "micromark-factory-space": "^1.0.0",
+        "micromark-util-character": "^1.0.0",
+        "micromark-util-symbol": "^1.0.0",
+        "micromark-util-types": "^1.0.0",
+        "uvu": "^0.5.0"
+      }
+    },
     "micromark-extension-math": {
       "version": "2.0.2",
       "resolved": "https://registry.npmjs.org/micromark-extension-math/-/micromark-extension-math-2.0.2.tgz",
@@ -14310,6 +14750,17 @@
         }
       }
     },
+    "remark-gfm": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/remark-gfm/-/remark-gfm-3.0.1.tgz",
+      "integrity": "sha512-lEFDoi2PICJyNrACFOfDD3JlLkuSbOa5Wd8EPt06HUdptv8Gn0bxYTdbU/XXQ3swAPkEaGxxPN9cbnMHvVu1Ig==",
+      "requires": {
+        "@types/mdast": "^3.0.0",
+        "mdast-util-gfm": "^2.0.0",
+        "micromark-extension-gfm": "^2.0.0",
+        "unified": "^10.0.0"
+      }
+    },
     "remark-math": {
       "version": "5.1.1",
       "resolved": "https://registry.npmjs.org/remark-math/-/remark-math-5.1.1.tgz",
diff --git a/package.json b/package.json
index 3e827b8..59b23f5 100644
--- a/package.json
+++ b/package.json
@@ -22,6 +22,7 @@
     "react-redux": "^8.0.5",
     "react-router-dom": "^6.4.4",
     "rehype-katex": "^6.0.2",
+    "remark-gfm": "^3.0.1",
     "remark-math": "^5.1.1",
     "vscode-ws-jsonrpc": "^2.0.0",
     "ws": "^8.9.0"
diff --git a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
index ed9f7c5..8a9573b 100644
--- a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
@@ -22,7 +22,7 @@ Seite.
 
 Wenn der Beweis komplett ist, erscheint \"Level Completed! 🎉\".
 
-Deine erste Taktik ist `rfl`, welche dazu da ist, ein Goal der Form `X = X` zu schliessen.
+Deine erste Taktik ist `rfl`, welche dazu da ist, ein Goal der Form $X = X$ zu schliessen.
 Gib die Taktik ein gefolgt von Enter ⏎.
 "
 
@@ -33,7 +33,7 @@ Message : 42 = 42 =>
 "Die Taktik `rfl` beweist ein Goal der Form `X = X`."
 
 Hint : 42 = 42 =>
-"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein und geh mit Enter ⏎ auf eine neue Zeile."
+"Man schreibt eine Taktik pro Zeile, also gib `rfl` ein und geh mit Enter ⏎ auf eine neue Zeile."
 
 Conclusion "Bravo!"
 
diff --git a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean
index d0240f0..f714651 100644
--- a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean
@@ -12,7 +12,7 @@ Introduction
 definiert sind, auch wenn diese unterschiedlich dargestellt werden. Das kann anfänglich
 zu Verwirrung führen.
 
-So sind `2` definiert als `1 + 1`, deshalb funktioniert `rfl` auch hier.
+So ist `2` als `1 + 1` definiert, deshalb funktioniert `rfl` auch hier.
 "
 
 Statement "Zeige dass $1 + 1$ zwei ist." : 1 + 1 = 2 := by
diff --git a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean
index cef86d2..e7cc86a 100644
--- a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean
@@ -8,20 +8,20 @@ Title "Annahmen"
 
 Introduction
 "
-Um Aussagen zu formulieren brauchen wir Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine
+Um Aussagen zu formulieren brauchen wir Annahmen. Das sind zum einen Objekte, wie \"sei $n$ eine
 natürliche Zahl\", und Annahmen über diese Objekte, von denen wir wissen, dass sie wahr sind.
 Zum Beispiel
-\"und angenommen, dass `n` strikt grösser als `1` ist\".
+\"und angenommen, dass $n$ strikt grösser als $1$ ist\".
 
 In Lean schreibt man beides mit dem gleichen Syntax: `(n : ℕ) (h : 1 < n)` definiert
-zuerst eine natürliche Zahl `n` und eine Annahme dass `1 < n` (die Annahme kriegt
+zuerst eine natürliche Zahl $n$ und eine Annahme dass $1 < n$ (die Annahme kriegt
 den Namen `h`).
 
 Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
 "
 
 Statement triviale_angelegenheit
-    "Angenommen `1 < n`. dann ist `1 < n`."
+    "Angenommen $1 < n$. dann ist $1 < n$."
     (n : ℕ) (h : 1 < n) : 1 < n := by
   assumption
 
diff --git a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
index 21ad625..7efc63f 100644
--- a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
@@ -11,14 +11,14 @@ Introduction
 "
 Eine allgemeine logische Aussage definiert man mit `(A : Prop)`.
 
-Damit sagt man noch nicht, ob die Aussage `A` wahr oder falsch ist.
-Mit einer Annahme `(hA : A)` nimmt man an, dass `A` wahr ist:
-`hA` ist sozusagen ein Beweis von `A`.
+Damit sagt man noch nicht, ob die Aussage $A$ wahr oder falsch ist.
+Mit einer Annahme `(hA : A)` nimmt man an, dass $A$ wahr ist:
+`hA` ist sozusagen ein Beweis von $A$.
 "
 
 Statement mehr_triviales
-    "Sei $ A $ eine logische Aussage und sei `hA` ein Beweis für $A$.
-    Zeige, dass $ A $ wahr ist."
+    "Sei $A$ eine logische Aussage und sei `hA` ein Beweis für $A$.
+    Zeige, dass $A$ wahr ist."
     (A : Prop) (hA : A) : A := by
   assumption
 
diff --git a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
index 62138d5..5aabca3 100644
--- a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
@@ -13,14 +13,17 @@ Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern man bra
 mehrere Schritte im Beweis.
 
 Wenn man eine Annahme `(h : X = Y)` hat,
-kann die Taktik `rw [h]` im Goal `X` durch `Y` ersetzen.
+kann die Taktik `rw [h]` im Goal $X$ durch $Y$ ersetzen.
 (`rw` steht für *rewrite*)
-
 "
 
 Statement umschreiben
     "Angenommen man hat die Gleichheiten
-    $a = b$, $a = d$, $c = d$.
+    $$ \\begin{aligned}
+      a &= b \\\\\\\\
+      a &= d \\\\\\\\
+      c &= d
+    \\end{aligned} $$
     Zeige dass $b = c$."
     (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
   rw [h₁]
@@ -42,14 +45,6 @@ Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h
 Hint (a : ℕ) (b : ℕ) (h : a = b) : a = b =>
 "Schau mal durch die Annahmen durch."
 
-
--- -- TODO: Muss ich das wirklich mehrmals auflisten?
--- Message (x : ℕ) : x = x =>
--- "Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
--- anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-
-Conclusion "Übrigens, mit `rw [h₁] at h₂` kann man auch eine andere Annahme umschreiben
-anstatt dem Goal."
--- TODO: Das macht es doch unmöglich mit den Messages...
+Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
 
 Tactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
index bf37e6a..5dbacfa 100644
--- a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
@@ -8,29 +8,37 @@ Level 6
 Title "Implikation"
 
 Introduction
-"Als nächstes widmen wir uns der Implikation &A \\Rightarrow B&. TODO
+"Als nächstes widmen wir uns der Implikation $A \\Rightarrow B$.
 
-Logische Aussagen `(A : Prop)`, `(B : Prop)`
-Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und
-die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der
-Aussage `A`.
+Mit zwei logischen Aussagen `(A : Prop)`, `(B : Prop)` schreibt man eine Implikation
+als `A → B` (`\\to`).
 
-Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Zeichen dafür:
-`A ↔ B` (`\\iff`) bedeutet \"Genau dann wenn\" und `A → B` (`\\to`) bedeutet \"`A` impliziert `B`\".
+Wenn man als Goal $B$ hat und eine Impikation `(g : A → B)` kann man mit `apply g` diese
+anwenden, worauf das Goal $A$ ist. Auf Papier würde man an der Stelle
+folgendes zu schreiben: \"Es genügt $A$ zu zeigen, denn $A$ impliziert $B$\".
+
+*Bemerke:* Das ist der selbe Pfeil, der später auch für Funktionen wie `ℕ → ℕ` gebraucht
+wird, deshalb heisst er `\\to`."
 
-Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man
-diese mit `apply h` anwenden.
-Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\"."
 
 Statement
-    "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
-    Zeige, dass `B` wahr ist."
+    "Seien $A$, $B$ logische Aussagen, wobei $A$ wahr ist und $A$ impliziert $B$.
+    Zeige, dass $B$ wahr ist."
     (A B : Prop) (hA : A) (g : A → B) : B := by
   apply g
   assumption
 
-Message (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
-"Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch `A` zeigen,
+Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
+"Mit `apply g` kannst du die Implikation `g` anwenden."
+
+Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
+"Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch $A$ zeigen,
 dafür hast du bereits einen Beweis in den Annahmen."
 
 Tactics apply assumption
+
+-- Mathjax notes
+-- `\\\\(    \\\\)` or `$   $` for inline
+-- and `$$  $$` block.
+-- align block:
+-- $$\\begin{aligned} 2x - 4 &= 6 \\\\\\\\ 2x &= 10 \\\\\\\\ x &= 5 \\end{aligned}$$
diff --git a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean
index 398de77..a151963 100644
--- a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean
@@ -8,18 +8,19 @@ Title "Implikation"
 
 Introduction
 "
-Angenommen man hat folgende Implikationen und weiss dass Aussage `A` wahr ist.
-```
-A → B ← C
-    ↓   ↓
-D → E → F
-```
-Beweise Aussage `F`.
+Angenommen man hat folgende Implikationen
+$$
+\\begin{CD}
+  A  @>{f}>> B       @<{g}<< C       \\\\
+  @. @V{h}VV @V{m}VV \\\\
+  D  @>{i}>> E       @>{k}>> F
+\\end{CD}
+$$
+und weiss, dass Aussage $A$ wahr ist.
 "
 
 Statement
-    "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
-    Zeige, dass `B` wahr ist."
+    "Beweise Aussage $F$."
     (A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E)
      (i : D → E) (k : E → F) (m : C → F) : F := by
   apply k
@@ -37,5 +38,6 @@ Message  (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
     (i : D → E) (k : E → F) (m : C → F) : D =>
 "Sackgasse. Probier doch einen anderen Weg."
 
-Tactics apply
-Tactics assumption
+Tactics apply assumption
+
+-- https://www.jmilne.org/not/Mamscd.pdf
diff --git a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
index d184925..cc07e24 100644
--- a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
@@ -10,9 +10,8 @@ Title "Implikation"
 
 Introduction
 "
-Wenn das Goal von der Form `A → B` ist, kann man mit `intro hA` annehmen, dass `A` wahr ist
-(i.e. erstellt eine Annahme `(hA : A)`)
-und das Goal wird zu `B`.
+Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit
+`intro hA` annehmen, dass $A$ wahr ist. Dann muss man $B$ beweisen.
 "
 
 Statement
@@ -23,4 +22,11 @@ Statement
   apply f
   assumption
 
+Message (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C =>
+"mit `intro hA` kann man eine Implikation angehen."
+
+Message (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
+"Jetzt ist es ein altbekanntes Spiel von `apply`-Anwendungen."
+
+
 Tactics intro apply assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
index ab4e558..483bcca 100644
--- a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
@@ -11,12 +11,13 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Genau-dann-wenn `A ↔ B` (`\\iff`) besteht aus zwei Implikationen `A → B` und `B → A`.
+Genau-dann-wenn, $A \\iff B$, wird als `A ↔ B (`\\iff`) geschrieben.
 
 Als erstes kann man mit `rw` Annahmen der Form `(h : A ↔ B)` genau gleich wie Gleichungen
 `(h : a = b)` benützen, um das Goal umzuschreiben.
 
-Hier also nochmals die Gleiche Aufgabe, aber diesmal mit Iff-Statements von Aussagen anstatt
+Hier also nochmals die Gleiche Aufgabe wie zuvor,
+aber diesmal mit Iff-Statements von Aussagen anstatt
 Gleichungen von natürlichen Zahlen.
 "
 
@@ -27,4 +28,17 @@ Statement
   rw [←h₂]
   assumption
 
+Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C =>
+"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
+Probiers doch mit `rw [h₁]`."
+
+Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D =>
+"Zur Erinnerung: Man kann auch rückwärts umschreiben: `h₂` sagt `A ↔ b` mit
+`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)"
+
+Hint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B =>
+"Schau mal durch die Annahmen durch."
+
+
+
 Tactics rw assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
index 0c91995..c72e80c 100644
--- a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
@@ -8,12 +8,11 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Als nächstes will man oft ein Iff-Statement `A ↔ B` wie zwei einzelne Implikationen
-`A → B` und `B → A` behandeln.
-
-Wenn das Goal `A ↔ B` ist, kann man mit der `constructor` Taktik, dieses in die Einzelteile
-`A → B` und `B → A` zerlegen.
+Ein $A \\iff B$ besteht intern aus zwei Implikationen, $\\textrm{mp} : A \\Rightarrow B$
+und $\\textrm{mpr} : B \\Rightarrow A$.
 
+Wenn man ein `A ↔ B` im Goal hat, kann man dieses mit `constructor` in die
+Einzelteile zerlegen.
 "
 
 Statement
@@ -23,6 +22,11 @@ Statement
   assumption
   assumption
 
+Message (A : Prop) (B : Prop) : A ↔ B =>
+"Eine Struktur wie `A ↔ B` kann man mit `constructor` zerlegen."
+
+Hint (A : Prop) (B : Prop) (h : A → B) : A → B =>
+"Such mal in den Annahmen."
 
 Conclusion
 "
diff --git a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean
index a3a0394..c340a91 100644
--- a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean
@@ -1,6 +1,4 @@
 import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Cases
 
 set_option tactic.hygienic false
 
@@ -12,52 +10,35 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Umgekehrt, wenn man eine Annahme `(h : A ↔ B)` hat, kann man auf verschiedene
-Arten die Einzelteile `A → B` und `B → A` extrahieren.
+Wenn man eine Annahme `(h : A ↔ B)` hat, kann man auch davon die Einzelnen
+Implikationen $\\textrm{mp} : A \\Rightarrow B$ und $\\textrm{mpr} : B \\Rightarrow A$
+brauchen.
 
-- mit `rcases h` oder `rcases h with ⟨h₁, h₂⟩` teilt man die Annahme `h` auf. (Im zweiten Fall gibt
-man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<` und `\\>`).
+Dazu gibt es zwei Methoden:
 
-"
-Statement
-    ""
-    (A B : Prop) : (A ↔ B) → (A → B) := by
-  intro h
-  rcases h
-  exact mp
-
-Message (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
-"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
+1.) `h.mp` (oder `h.1`) und `h.mpr` (oder `h.2`) sind direkt die einzelnen Richtungen.
+Man kann also z.B. mit `apply h.mp` die Implikation `A → B` auf ein Goal `B` anwenden.
 
-Conclusion
+(PS: das `.mp` kommt von \"Modus Ponens\".)
 "
-Anstatt
-```
-intro h
-rcases h with ⟨h₁, h₂⟩
-```
-kann man direkt `intro ⟨h₁, h₂⟩` schreiben.
-Wie du schon gesehen hast, sind diese Klammern `⟨⟩` Lean's Syntax für eine Struktur aus
-mehreren Teilen.
-
-"
-
-Tactics intro apply rcases assumption
-
-
 
+Statement
+    "Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
+    (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+  intro hA
+  apply g
+  apply h.mp
+  assumption
 
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C =>
+"Zuerst kannst du wieder `intro` benützen um die Implikation anzugehen."
 
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C =>
+"Der nächste Schritt kommt auch noch aus dem Implikationen-Level."
 
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
+"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
 
--- TODO: The new `cases` works differntly. There is also `cases'`
-example (A B : Prop) : (A ↔ B) → (A → B) := by
-  intro h
-  cases h with
-  | intro a b =>
-    assumption
+Conclusion "Im nächsten Level findest du die zweite Option."
 
-example (A B : Prop) : (A ↔ B) → (A → B) := by
-  intro h
-  cases' h with a b
-  assumption
+Tactics apply assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean
index b986b1f..1f89d16 100644
--- a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean
@@ -1,4 +1,6 @@
 import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
 
 Game "TestGame"
 World "Logic"
@@ -8,24 +10,44 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Man kann auch die einzelnen Richtungen benützen, ohne `h` selber zu verändern:
+Als zweite Option, kann man eine Annahme `(h : A ↔ B)` in zwei neue Annahmen
+`(h₁ : A → B)` und `(h₂ : B → A)` aufteilen.
 
-- `h.1` und `h.2` sind direkt die einzelnen Richtungen. Man kann also z.B. mit `apply h.1` die
-Implikation `A → B` auf ein Goal `B` anwenden.
-- `h.mp` und `h.mpr` sind die bevorzugten Namen anstatt `.1` und `.2`. \"mp\" kommt von
-\"Modus Ponens\", aber das ist hier irrelevant.
-"
+2.) Mit `rcases h` teilt man die Annahme `h` auf.
+
+(Mit `rcases h with ⟨h₁, h₂⟩` (`\\<`, `\\>`) kann man zudem die neuen Annahmen benennen.)
 
+"
 Statement
-    "Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen."
-    (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
-  intro hA
-  apply g
-  apply h.mp
+    "Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
+    (A B : Prop) : (A ↔ B) → (A → B) := by
+  intro h
+  rcases h
   assumption
 
-Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
-"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
+Message (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
+"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
+
+Message (A : Prop) (B : Prop) (h : A ↔ B): A → B =>
+"Mit `rcases h with ⟨h₁, h₂⟩` kannst du jetzt die Annahme `(h : A ↔ B)` zerlegen."
+
+
+Conclusion
+"
+Note: In der Mathematik definieren wir oft Strukturen als Tupels, z.B. \"Sei (G, +) eine Gruppe\".
+In Lean brauchen wir dafür immer die Klammern von oben: `⟨_, _⟩`.
+"
+
+Tactics intro apply rcases assumption
+
+-- -- TODO: The new `cases` works differntly. There is also `cases'`
+-- example (A B : Prop) : (A ↔ B) → (A → B) := by
+--   intro h
+--   cases h with
+--   | intro a b =>
+--     assumption
 
-Tactics apply
-Tactics assumption
+-- example (A B : Prop) : (A ↔ B) → (A → B) := by
+--   intro h
+--   cases' h with a b
+--   assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L07_And.lean b/server/testgame/TestGame/Levels/Logic/L07_And.lean
index 1af28d7..5a1317b 100644
--- a/server/testgame/TestGame/Levels/Logic/L07_And.lean
+++ b/server/testgame/TestGame/Levels/Logic/L07_And.lean
@@ -12,7 +12,8 @@ Title "Und"
 Introduction
 "
 Das logische UND `A ∧ B` (`\\and`) funktioniert sehr ähnlich zum Iff (`↔`).
-Grund dafür ist, dass `A ∧ B` auch eine Struktur aus zwei Teilen `⟨A, B⟩` ist.
+Grund dafür ist, dass `A ∧ B` auch eine Struktur aus zwei Teilen ist, nämlich
+der linken und rechten Seite.
 
 Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man
 `.1` und `.2` für die Einzelteile brauchen, diese heissen lediglich
@@ -20,7 +21,7 @@ Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man
 "
 
 Statement
-    ""
+    "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
     (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
   constructor
   intro h
@@ -37,32 +38,49 @@ Statement
   assumption
 
 Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
-"`↔` oder `∧` im Goal kann man mit `constructor` aufteilen."
+"`↔` oder `∧` im Goal kann man mit `constructor` zerlegen."
+
+Message (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B =>
+"Hier würdest du mit `intro` die Implikation angehen.
+
+(Experten können mit `intro ⟨h₁, h₂⟩` im gleichen Schritt noch ein `rcases` auf
+das UND in der Implikationsannahme)"
 
 -- if they don't use `intro ⟨_, _⟩`.
 Message (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B =>
 "Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen."
 
+Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
+"Wie wär's mit `apply`? Hast du ne Implikation, die anwendbar ist?"
+
+-- Rückrichtung
+Message (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) =>
+"Das Goal ist ne Implikation $\\ldots \\Rightarrow \\ldots$
+Da hilft `intro`.
+
+(auch hier kann man wieder mit `intro ⟨ha, hb⟩` gleich noch die Premisse zerlegen.)"
+
+
+
+
 -- if they don't use `intro ⟨_, _⟩`.
 Message (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) =>
-"Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` aufteilen."
+"Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` zerlegen."
 
 Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
-"Wieder in Einzelteile aufteilen..."
+"Wieder in Einzelteile zerlegen..."
 
-Message (A : Prop) (B : Prop) : A ∧ (A → B) =>
-"Immer das gleiche ... noch mehr aufteilen."
+Message (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) =>
+"Immer das gleiche ... noch mehr zerlegen."
 
-Message (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B =>
-"Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen,
-wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`).
+-- Message (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B =>
+-- "Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen,
+-- wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`).
 
-Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht,
-dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen,
-dass `B` wahr ist."
+-- Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht,
+-- dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen,
+-- dass `B` wahr ist."
 
-Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
-"Sieht nach einem Fall für `apply` aus."
 
 
 -- TODO
diff --git a/server/testgame/TestGame/Levels/Logic/L08_Or.lean b/server/testgame/TestGame/Levels/Logic/L08_Or.lean
index e4e6cb1..cd27569 100644
--- a/server/testgame/TestGame/Levels/Logic/L08_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08_Or.lean
@@ -18,8 +18,16 @@ Wenn das Goal ein `∨` ist kann man mit `left` oder `right` entscheiden,
 welche Seite man beweisen möchte.
 "
 
-Statement "" (A B : Prop) (hA : A) : A ∨ (¬ B) := by
+Statement
+    "Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$"
+    (A B : Prop) (hA : A) : A ∨ (¬ B) := by
   left
   assumption
 
+Hint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) =>
+"Entscheide dich, `right` oder `left`?"
+
+Message (A : Prop) (B : Prop) (hA : A) : ¬ B =>
+"Sackgasse. Probier's nochmals."
+
 Tactics left right assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
index 6923ff6..63e43d7 100644
--- a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
@@ -15,42 +15,89 @@ Title "Oder - Bonus"
 
 Introduction
 "
-Wenn man hingegen ein ODER - `(h : A ∨ B)` - in den Annahmen hat, kann man dieses
+Wenn man hingegen ein ODER `(h : A ∨ B)` in den Annahmen hat, kann man dieses
 ähnlich wie beim UND mit `rcases h` aufteilen.
 
-ABER! Beim UND `(h : A ∧ B)` hat man dann zwei neue Annahmen erhalten, und diese hat man mit
-`rcases h with ⟨hA, hB⟩` benannt. Beim ODER `(h : A ∨ B)` kriegt man stattdessen zwei **Goals**
-wo man annimmt, dass entweder die linke oder rechte Seite von `h` war ist.
-Diese Annahme benennt man dann mit `rcases h with hA | hB`.
+**Wichtig:** der Syntax dafür ist `rcases h with h₁ | h₂`.
+
+Der Unterschied ist, dass man beim UND eine Annahme in zwei Einzelteile zerlegt (mit $⟨h₁, h₂⟩$).
+Beim ODER hingegen, kriegt man stattdessen zwei *Goals*, nämlich eines wo man annimmt,
+die linke Seite sei wahr und eines wo man annimmt, rechts sei wahr.
 "
 
-Statement
-    ""
-    (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by
-  rcases h with ⟨ha, hb⟩ | (h | h)
-  left
+Statement distributivity
+    "Angenommen $ A \\lor (B \\land C)$ is wahr, zeige, dass $(A \\lor B) \\land (A \\lor C)$."
+    (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
+  rcases h with ha | h
   constructor
+  left
   assumption
+  left
   assumption
-  right
+  rcases h with ⟨h₁, h₂⟩
+  constructor
   right
   assumption
   right
-  left
   assumption
 
-Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) =>
-"Man kann hier entweder in mehren Schritten `rcases` anwenden:
-```
-  rcases h with h₁ | h₂
-  rcases h₁ with ⟨hA, hB⟩
-  [...]
-  rcases h₂ with h | h
-```
-oder man kann dies in einem Schritt verschachteln:
-```
-rcases h with ⟨ha, hb⟩ | (h | h)
-```
-"
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
+"Als erstes solltest du das OR in der Annahme `(h: A ∨ (B ∧ C))` aufteilen:"
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A) : (A ∨ B) ∧ (A ∨ C) =>
+"Wie wär's mit zerlegen?"
+
+Hint (A : Prop) (B : Prop) : (A ∨ B) =>
+"`left` oder `right`?"
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
+"Und jetzt der Fall, falls die rechte Seite $B \\land C$ wahr ist. Zerlege diese
+Annahme doch als erstes."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
+"Jetzt musst du die Annahme $A \\lor (B \\land C)$ trotzdem noch mit `rcases` zerlegen."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) =>
+"So musst du die Annahme $A \\lor (B \\land C)$ nochmals mit `rcases` zerlegen...
+
+Wenn du am Anfang zuerst `rcases` und dann `constructor` aufrufst,
+musst du das hier nur einmal machen..."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : A ∨ B =>
+"Die Annahme `B ∧ C` kannst du auch mit `rcases` zerlegen."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : A ∨ C =>
+"Die Annahme `B ∧ C` kannst du auch mit `rcases` zerlegen."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : C =>
+"Die Annahme `B ∧ C` kannst du auch mit `rcases` zerlegen."
+
+
+-- Statement umsortieren
+--     "Angenommen $(A \\land B) \\lor (D \\lor C)$ is wahr, zeige, dass "
+--     (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by
+--   rcases h with x | (h | h)
+--   left
+--   assumption
+--   right
+--   right
+--   assumption
+--   right
+--   left
+--   assumption
+
+-- Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) =>
+-- "Man kann hier entweder in mehren Schritten `rcases` anwenden:
+-- ```
+--   rcases h with h₁ | h₂
+--   rcases h₁ with ⟨hA, hB⟩
+--   [...]
+--   rcases h₂ with h | h
+-- ```
+-- oder man kann dies in einem Schritt verschachteln:
+-- ```
+-- rcases h with ⟨ha, hb⟩ | (h | h)
+-- ```
+-- "
 
 Tactics left right assumption constructor rcases apply
diff --git a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean
index a8fa8b0..ea836ae 100644
--- a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean
@@ -12,11 +12,18 @@ Title "Oder"
 
 Introduction
 "
-Übung macht den Meister...
+Übung macht den Meister... Benutze alle vier Methoden mit UND und ODER
+umzugehen um folgende Aussage zu beweisen.
+
+|         | Und           | Oder           |
+|---------|:--------------|:---------------|
+| Annahme | `rcases h`    | `rcases h`     |
+| Goal    | `constructor` | `left`/`right` |
 "
 
 Statement and_or_imp
-    "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
+    "Angenommen $(A \\land B) \\lor (A \\Rightarrow C)$ und $A$ sind wahr, zeige dass
+    $B \\lor (C \\land A)$ wahr ist."
     (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
   rcases h with h₁ | h₂
   left
@@ -28,17 +35,28 @@ Statement and_or_imp
   assumption
   assumption
 
-Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) =>
-"Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`. Der `|` signalisiert
-dass `h₁` und `h2` die Namen der neuen Annahmen in den verschiedenen Fällen sind."
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) =>
+"Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`."
+
+-- If starting with `left`.
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : B =>
+"Da kommst du nicht mehr weiter..."
+
+-- If starting with `right`.
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : (C ∧ A) =>
+"Da kommst du nicht mehr weiter..."
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
+"`left` oder `right`?"
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : B) (hA : A) : B ∨ (C ∧ A) =>
+"`left` oder `right`?"
 
 Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
-"Ein ODER im Goal kann mit `left` oder `right` angegangen werden."
+"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen."
 
 Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B =>
-"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen.
-Der Konstruktor `⟨⟩` signalisiert hier, dass dann nur ein Goal aber zwei neu benannte
-Annahmen erhält."
+"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen."
 
 Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C =>
 "Sackgasse."