From a4623a82414f9d6e262ab3d2ea81cd28e2df4308 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 23 Mar 2023 16:00:11 +0100
Subject: [PATCH] css

---
 client/src/components/Level.tsx               | 12 ++++----
 client/src/components/infoview/hints.tsx      |  2 +-
 client/src/components/infoview/infoview.css   |  6 ++--
 .../Levels/Lean/L03_ImplicitArguments.lean    |  2 +-
 .../Levels/Lean/L04_InstanceArguments.lean    |  2 +-
 .../Levels/LinearAlgebra/L01_Module.lean      |  7 ++++-
 .../LinearAlgebra/L02_VectorNotation.lean     | 28 ++++---------------
 .../TestGame/Levels/SetTheory/L03_Subset.lean | 17 ++++++-----
 .../TestGame/Levels/Sum/L01_Simp.lean         |  2 +-
 .../testgame/TestGame/Levels/Sum/L02_Sum.lean |  2 +-
 .../TestGame/Levels/Sum/L03_ArithSum.lean     |  2 +-
 .../TestGame/Levels/Sum/L04_SumOdd.lean       |  2 +-
 .../TestGame/Levels/Sum/L05_SumComm.lean      |  2 +-
 .../TestGame/Levels/Sum/L06_Summary.lean      |  2 +-
 .../TestGame/Levels/Sum/T01_Induction.lean    |  2 +-
 .../TestGame/Levels/Sum/T02_Induction.lean    |  2 +-
 .../TestGame/Levels/Sum/T03__Bernoulli.lean   |  2 +-
 .../TestGame/Options/BigOperators.lean        | 17 -----------
 server/testgame/TestGame/ToBePorted.lean      | 23 +++++++++++++++
 19 files changed, 64 insertions(+), 70 deletions(-)
 delete mode 100644 server/testgame/TestGame/Options/BigOperators.lean

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index fa3fa54..89a9de4 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -179,9 +179,9 @@ function PlayableLevel({worldId, levelId}) {
     <Split minSize={0} snapOffset={200} sizes={[50, 25, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
       <div className="exercise-panel">
         <div ref={introductionPanelRef} className="introduction-panel">
-          <Alert severity="info" sx={{ mt: 1 }}>
+          <div className="message info">
             <Markdown>{level?.data?.introduction}</Markdown>
-          </Alert>
+          </div>
         </div>
         <div className="exercise">
           {/* <h4>Aufgabe:</h4> */}
@@ -205,9 +205,9 @@ function PlayableLevel({worldId, levelId}) {
         </EditorContext.Provider>
 
         {completed && <div className="conclusion">
-          <Alert severity="info" sx={{ mt: 1 }}>
+          <div className="message info">
             <Markdown>{level?.data?.conclusion}</Markdown>
-          </Alert>
+          </div>
           {levelId >= gameInfo.data?.worldSize[worldId] ?
           <Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button> :
           <Button to={`/world/${worldId}/level/${levelId + 1}`}>
@@ -237,11 +237,11 @@ function Introduction({worldId}) {
     <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Einführung" worldId={worldId} levelId={0} />
     <div style={gameInfo.isLoading ? {display: "none"} : null} className="exercise-panel">
       <div className="introduction-panel">
-        <Alert severity="info" sx={{ mt: 1 }}>
+        <div className="message info">
           <Markdown>
             {gameInfo.data?.worlds.nodes[worldId].introduction}
           </Markdown>
-        </Alert>
+        </div>
       </div>
       <div className="conclusion">
         {0 == gameInfo.data?.worldSize[worldId] ?
diff --git a/client/src/components/infoview/hints.tsx b/client/src/components/infoview/hints.tsx
index 4a290fc..b7ba2b9 100644
--- a/client/src/components/infoview/hints.tsx
+++ b/client/src/components/infoview/hints.tsx
@@ -4,7 +4,7 @@ import { Alert, FormControlLabel, Switch } from '@mui/material';
 import Markdown from '../Markdown';
 
 function Hint({hint} : {hint: GameHint}) {
-  return <Alert severity="info" sx={{ mt: 1 }}><Markdown>{hint.text}</Markdown></Alert>
+  return <div className="message info"><Markdown>{hint.text}</Markdown></div>
 }
 
 export function Hints({hints} : {hints: GameHint[]}) {
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css
index 650a679..f90c0d3 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -4,9 +4,9 @@
   padding: 5px 10px;
   border-radius: 3px 3px 3px 3px;
 }
-.message.information {
-  color: #059;
-  background-color: #BEF;
+.message.info {
+  /* color: #059; */
+  background-color: #DDF6FF;
 }
 .message.warning {
   color: #9F6000;
diff --git a/server/testgame/TestGame/Levels/Lean/L03_ImplicitArguments.lean b/server/testgame/TestGame/Levels/Lean/L03_ImplicitArguments.lean
index d68da37..3b1c398 100644
--- a/server/testgame/TestGame/Levels/Lean/L03_ImplicitArguments.lean
+++ b/server/testgame/TestGame/Levels/Lean/L03_ImplicitArguments.lean
@@ -1,7 +1,7 @@
 import TestGame.Metadata
 
 import Mathlib
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 
 set_option tactic.hygienic false
 
diff --git a/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean b/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean
index 8339fbf..10da5bc 100644
--- a/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean
+++ b/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean
@@ -1,7 +1,7 @@
 import TestGame.Metadata
 
 import Mathlib
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 
 set_option tactic.hygienic false
 
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean b/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
index b37f4ae..e0c0082 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
@@ -74,13 +74,14 @@ Statement
   · Hint "**Robo**: Jetzt musst du alle eigenschaften eines $\\mathbb\{Q}$-Moduls zeigen,
     das sind also 6 einzelne Goals."
     intro b
-    Hint "**Robo**: Mit `change (1 : ℚ) * b = b` kannst du das Goal umschreiben, damit
+    Hint "**Robo**: Mit `change (1 : ℚ) * {b} = {b}` kannst du das Goal umschreiben, damit
     dann andere Taktiken besser damit arbeiten können."
     change (1 : ℚ) * b = b
     Hint "**Robo**: Den Teil kannst du mit `simp` beweisen."
     simp
   · intro x y b
     Hint "**Robo**: Benutze `change` um `•` durch `*` zu ersetzen."
+    Hint (hidden := true) "**Robo**: Explizit `change ({x} * {y} : ℚ) * {b} = {x} * ({y} * {b})`"
     change (x * y : ℚ) * b = x * (y * b)
     Hint "**Robo**: Mit `simp` und `ring` kannst du den Rest beweisen."
     simp
@@ -88,13 +89,17 @@ Statement
   · intro a
     simp
   · intro a x y
+    Hint (hidden := true) "**Robo**: Explizit `change {a} * ({x} + {y}) = {a} * {x} + {a} * {y}`"
     change a * (x + y) = a * x + a * y
     ring
   · intro r s x
+    Hint (hidden := true) "**Robo**: Explizit
+    `change ({r} + {s} : ℚ) * {x} = {r} * {x} + {s} * {x}`"
     change (r + s : ℚ) * x = r * x + s * x
     simp
     ring
   · intro a
+    Hint (hidden := true) "**Robo**: Explizit `change (0 : ℚ) * {a} = 0`"
     change (0 : ℚ) * a = 0
     simp
 
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean b/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
index 0e77ca7..ad71161 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
@@ -15,30 +15,14 @@ Title "Konkrete Vektorräume"
 
 Introduction
 "
-Häufig in der linearen Algebra hat man ganz einfach Vektoren über `ℚ` oder `ℝ`
-und möchte diese explizit definieren.
-
-Reele Vektorräume definiert man in Lean am besten als Funktion von einem Indexset.
-
-So ist `Fin 2` eine Menge, die nur `0` und `1` enthält
-und `ℚ²` wird als `Fin 2 → ℚ` definiert. Hier machen wir uns eine
-lokale notation dafür:
+Den $\\mathbb{Q}$-Vektorraum $\\mathbb{Q}^3$ definiert man am besten mit
+der lokalen Notation
 
 ```
-notation `ℚ²` := Fin 2 → ℚ
+local notation `ℚ³` := Fin 3 → ℚ
 ```
 
-Das mag auf den ersten Blick etwas unintuitiv erscheinen, hat aber den Vorteil,
-dass man die ganze
-Infrastruktur für Funktionen einfach direkt für Vektoren und
-Matrizen mitgebrauchen kann.
-
-Wir können uns auch noch ein paar andere standardmässige `ℚ`-Vektorräume definieren.
-
-```
-notation \"ℚ³\" => Fin 3 → ℚ
-notation \"ℚ^(\" n \")\" => (Fin n) → ℚ
-```
+Dabei ist `Fin 3` die Indexmenge $\\{0, 1, 2\\}$.
 
 Die schreibweise für einen Vektor ist `![ _, _ ]`. Zu beachten ist,
 dass man bei Zahlen explizit einen Typ angeben muss, sonst denkt sich
@@ -61,8 +45,8 @@ Dann eine Vektorgleichung komponentenweise aufteilt.
 Für jede Komponente kann man dann mit `simp` und `ring` weiterkommen.
 "
 
-notation "ℚ³" => Fin 3 → ℚ
-notation "ℚ^(" n ")" => (Fin n) → ℚ
+local notation "ℚ³" => Fin 3 → ℚ
+local notation "ℚ^(" n ")" => (Fin n) → ℚ
 
 Statement
 ""
diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
index 15acf84..4a04171 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
@@ -16,18 +16,17 @@ Introduction
 "
 Ihr bemerkt, dass mit dem Jungen noch zwei andere
 Kinder zuhörten. Eines der beiden Mädchen hat ebenfalls eine Frage.
+"
 
+-- Hat man zwei Mengen `(A B : Set ℕ)` kann man fragen, ob diese Teilmengen
+-- voneinander sind: `A ⊆ B` (`\\sub`/`\\ss`) ist die Notation für Teilmengen, die auch gleich
+-- sein können.
 
-Hat man zwei Mengen `(A B : Set ℕ)` kann man fragen, ob diese Teilmengen
-voneinander sind: `A ⊆ B` (`\\sub`/`\\ss`) ist die Notation für Teilmengen, die auch gleich
-sein können.
-
-`A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert, das heisst, ein `⊆` kann immer auch mit `intro x hx`
-angegangen werden.
+-- `A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert, das heisst, ein `⊆` kann immer auch mit `intro x hx`
+-- angegangen werden.
 
-Die Taktik `tauto` macht das automatisch, aber um dies zu lernen ist `tauto` hier deaktiviert.
-Benutze also `intro`:
-"
+-- Die Taktik `tauto` macht das automatisch, aber um dies zu lernen ist `tauto` hier deaktiviert.
+-- Benutze also `intro`:
 
 namespace MySet
 
diff --git a/server/testgame/TestGame/Levels/Sum/L01_Simp.lean b/server/testgame/TestGame/Levels/Sum/L01_Simp.lean
index bb8deb2..ec2c5c4 100644
--- a/server/testgame/TestGame/Levels/Sum/L01_Simp.lean
+++ b/server/testgame/TestGame/Levels/Sum/L01_Simp.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 
 set_option tactic.hygienic false
 
diff --git a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
index 5ab6f40..039c2b7 100644
--- a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
+++ b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib
 
 set_option tactic.hygienic false
diff --git a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
index b378431..526b720 100644
--- a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
+++ b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
@@ -3,7 +3,7 @@ import TestGame.Metadata
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 
 set_option tactic.hygienic false
 
diff --git a/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean
index fefeca5..da9b27a 100644
--- a/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean
+++ b/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
diff --git a/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean b/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean
index 48d69d0..b6f8d62 100644
--- a/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean
+++ b/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
diff --git a/server/testgame/TestGame/Levels/Sum/L06_Summary.lean b/server/testgame/TestGame/Levels/Sum/L06_Summary.lean
index d4462d2..6aea6a2 100644
--- a/server/testgame/TestGame/Levels/Sum/L06_Summary.lean
+++ b/server/testgame/TestGame/Levels/Sum/L06_Summary.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
diff --git a/server/testgame/TestGame/Levels/Sum/T01_Induction.lean b/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
index 9b095f7..b65d4c5 100644
--- a/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib.Algebra.BigOperators.Fin
 
 set_option tactic.hygienic false
diff --git a/server/testgame/TestGame/Levels/Sum/T02_Induction.lean b/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
index b424a4d..42df47d 100644
--- a/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
+++ b/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib.Algebra.BigOperators.Fin
 
 set_option tactic.hygienic false
diff --git a/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean b/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean
index 003a584..85c2807 100644
--- a/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean
+++ b/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean
@@ -1,6 +1,6 @@
 import TestGame.Metadata
 
-import TestGame.Options.BigOperators
+import TestGame.ToBePorted
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
diff --git a/server/testgame/TestGame/Options/BigOperators.lean b/server/testgame/TestGame/Options/BigOperators.lean
deleted file mode 100644
index 8a5f1c2..0000000
--- a/server/testgame/TestGame/Options/BigOperators.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathlib.Algebra.BigOperators.Fin
-
-open BigOperators
-
-open Lean PrettyPrinter Delaborator SubExpr
-
-@[ delab app.Finset.sum]
-def delabFinsetSum : Delab := do
-  guard $ (← getExpr).getAppNumArgs == 5
-  guard $ ((← getExpr).getArg! 3).isAppOf' ``Finset.univ
-  guard $ ((← getExpr).getArg! 4).isLambda
-  withNaryArg 4 do
-    let α ← withBindingDomain delab
-    withBindingBodyUnusedName fun n => do
-      let n : TSyntax `ident := ⟨n⟩
-      let b ← delab
-      `(∑ $n:ident : $α, $b)
diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean
index 9e01935..7c66039 100644
--- a/server/testgame/TestGame/ToBePorted.lean
+++ b/server/testgame/TestGame/ToBePorted.lean
@@ -1,5 +1,28 @@
 import Mathlib
 
+open BigOperators
+
+/-! # Delab Problems -/
+
+open Lean PrettyPrinter Delaborator SubExpr
+
+@[delab app.Finset.sum]
+def delabFinsetSum : Delab := do
+  guard $ (← getExpr).getAppNumArgs == 5
+  guard $ ((← getExpr).getArg! 3).isAppOf' ``Finset.univ
+  guard $ ((← getExpr).getArg! 4).isLambda
+  withNaryArg 4 do
+    let α ← withBindingDomain delab
+    withBindingBodyUnusedName fun n => do
+      let n : TSyntax `ident := ⟨n⟩
+      let b ← delab
+      `(∑ $n:ident : $α, $b)
+
+
+
+
+/-! # Other Stuff -/
+
 -- lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by
 --   sorry