Modified starter level.

2023-01-17 15:30:49 +01:00
parent b02d55de34
commit 1eb0ac63e3
42 changed files with 580 additions and 205 deletions
@@ -76,6 +76,11 @@ p, table {
  margin-inline-end: 0px;
 }

+/* Prevent white spaces break inside a table. */
+td code  {
+  white-space:nowrap;
+}
+
 /***************************************/
 /* TODO: For development purposes only */
 /***************************************/
@@ -1,8 +1,5 @@
 import TestGame.Metadata
-import TestGame.Levels.Logic.L01_Rfl
 import TestGame.Levels.Logic.L02_Rfl
-import TestGame.Levels.Logic.L03_Assumption
-import TestGame.Levels.Logic.L03b_Assumption
 import TestGame.Levels.Logic.L04_Rewrite
 import TestGame.Levels.Logic.L04b_Rewrite
 import TestGame.Levels.Logic.L05_Apply
@@ -12,10 +9,6 @@ import TestGame.Levels.Logic.L06_Iff
 import TestGame.Levels.Logic.L06b_Iff
 import TestGame.Levels.Logic.L06c_Iff
 import TestGame.Levels.Logic.L06d_Iff
-import TestGame.Levels.Logic.L07_And
-import TestGame.Levels.Logic.L08_Or
-import TestGame.Levels.Logic.L08b_Or
-import TestGame.Levels.Logic.L08c_Or
 import TestGame.Levels.Naturals.L01_Ring
 import TestGame.Levels.Naturals.L02_Ring
 import TestGame.Levels.Naturals.L03_Exists
@@ -24,8 +17,6 @@ import TestGame.Levels.Naturals.L31_Sum
 import TestGame.Levels.Naturals.L32_Induction
 import TestGame.Levels.Naturals.L33_Prime
 import TestGame.Levels.Naturals.L34_ExistsUnique
-import TestGame.Levels.Negation.L01_False
-import TestGame.Levels.Negation.L02_Contra
 import TestGame.Levels.Negation.L03_Contra
 import TestGame.Levels.Negation.L04_Contra
 import TestGame.Levels.Negation.L05_Not
@@ -34,6 +25,10 @@ import TestGame.Levels.Negation.L07_Contrapose
 import TestGame.Levels.Negation.L08_Contrapose
 import TestGame.Levels.Negation.L09_PushNeg

+import TestGame.Levels.Proposition
+
+
+
 Game "TestGame"

 Title "Lean 4 game"
@@ -89,5 +84,5 @@ Conclusion
 "There is nothing else so far. Thanks for rescuing natural numbers!"


-Path Logic → Nat → Contradiction
-Path Nat → Nat2
+Path Proposition → Implication → Predicate → Proving
+Path Predicate → Nat2
@@ -1,8 +1,8 @@
 import TestGame.Metadata

 Game "TestGame"
-World "Logic"
-Level 2
+World "Predicate"
+Level 6

 Title "Definitionally equal"

@@ -2,8 +2,8 @@ import TestGame.Metadata
 import Mathlib

 Game "TestGame"
-World "Logic"
-Level 5
+World "Predicate"
+Level 3

 Title "Rewrite"

@@ -2,8 +2,8 @@ import TestGame.Metadata
 import Mathlib

 Game "TestGame"
-World "Logic"
-Level 6
+World "Predicate"
+Level 4

 Title "Rewrite"

@@ -2,8 +2,8 @@ import TestGame.Metadata
 import Mathlib

 Game "TestGame"
-World "Logic"
-Level 7
+World "Implication"
+Level 3

 Title "Implikation"

@@ -1,8 +1,8 @@
 import TestGame.Metadata

 Game "TestGame"
-World "Logic"
-Level 8
+World "Implication"
+Level 4

 Title "Implikation"

@@ -3,8 +3,8 @@ import TestGame.Metadata
 set_option tactic.hygienic false

 Game "TestGame"
-World "Logic"
-Level 9
+World "Implication"
+Level 1

 Title "Implikation"

@@ -1,11 +1,11 @@
 import TestGame.Metadata

 import Init.Data.ToString
-#check List UInt8
+-- #check List UInt8

 Game "TestGame"
-World "Logic"
-Level 10
+World "Implication"
+Level 6

 Title "Genau dann wenn"

@@ -1,8 +1,8 @@
 import TestGame.Metadata

 Game "TestGame"
-World "Logic"
-Level 11
+World "Implication"
+Level 5

 Title "Genau dann wenn"

@@ -3,8 +3,8 @@ import TestGame.Metadata
 set_option tactic.hygienic false

 Game "TestGame"
-World "Logic"
-Level 12
+World "Implication"
+Level 7

 Title "Genau dann wenn"

@@ -19,7 +19,7 @@ Dazu gibt es zwei Methoden:
 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.

-(PS: das `.mp` kommt von \"Modus Ponens\".)
+(PS: das `.mp` kommt von \"Modus Ponens\", ein Ausdruck as der Logik.)
 "

 Statement
@@ -3,8 +3,8 @@ import Std.Tactic.RCases
 import Mathlib.Tactic.Cases

 Game "TestGame"
-World "Logic"
-Level 13
+World "Implication"
+Level 8

 Title "Genau dann wenn"

@@ -1,90 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Logic"
-Level 14
-
-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 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
-`h.left` und `h.right` anstatt `.mp` und `.mpr`.
-"
-
-Statement
-    "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
-    (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
-  constructor
-  intro h
-  rcases h with ⟨h₁, h₂⟩
-  constructor
-  assumption
-  apply h₂
-  assumption
-  intro h
-  rcases h with ⟨h₁, h₂⟩
-  constructor
-  assumption
-  intro
-  assumption
-
-Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
-"`↔` 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` zerlegen."
-
-Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
-"Wieder in Einzelteile zerlegen..."
-
-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)`).
-
-- 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."
-
-
-
-- TODO
-
-
-Tactics apply rcases
-Tactics assumption
@@ -5,8 +5,8 @@ import Mathlib.Tactic.LeftRight
 set_option tactic.hygienic false

 Game "TestGame"
-World "Logic"
-Level 17
+World "Implication"
+Level 9

 Title "Oder"

@@ -15,10 +15,10 @@ Introduction
 Ü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` |
+|         | Und                      | Oder                      |
+|---------|:-------------------------|:--------------------------|
+| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h₁ \\| h₂` |
+| Goal    | `constructor`            | `left`/`right`            |
 "

 Statement and_or_imp
@@ -4,7 +4,7 @@ import Mathlib.Tactic.Ring
 --set_option tactic.hygienic false

 Game "TestGame"
-World "Nat"
+World "Predicate"
 Level 1

 Title "Natürliche Zahlen"
@@ -2,8 +2,8 @@ import TestGame.Metadata
 import Mathlib.Tactic.Ring

 Game "TestGame"
-World "Nat"
-Level 2
+World "Predicate"
+Level 5

 Title "Natürliche Zahlen"

@@ -7,8 +7,8 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted

 Game "TestGame"
-World "Nat"
-Level 3
+World "Predicate"
+Level 7

 Title "Gerade/Ungerade"

@@ -7,8 +7,8 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted

 Game "TestGame"
-World "Nat"
-Level 4
+World "Predicate"
+Level 8

 Title "Für alle"

@@ -1,29 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Contradiction"
-Level 2
-
-Title "Ad absurdum"
-
-Introduction
-"
-Ähnlich siehts aus, wenn man Annahmen hat, die direkte Negierung voneinander sind,
-also `(h : A)` und `(g : ¬ A)`. (`\\not`)
-"
-
-Statement absurd
-    "Sei $n$ eine natürliche Zahl die sowohl gerade wie auch nicht gerade ist.
-    Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)"
-    (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 42 := by
-  contradiction
-
-Conclusion
-"
-"
-
-Tactics contradiction
@@ -8,8 +8,8 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted

 Game "TestGame"
-World "Contradiction"
-Level 3
+World "Proving"
+Level 1

 Title "Ad absurdum"

@@ -3,10 +3,10 @@ import Std.Tactic.RCases
 import Mathlib.Tactic.LeftRight

 Game "TestGame"
-World "Contradiction"
-Level 4
+World "Predicate"
+Level 2

-Title "Ad absurdum"
+Title "Widerspruch"

 Introduction
 "
@@ -2,8 +2,8 @@ import TestGame.Metadata
 import Mathlib

 Game "TestGame"
-World "Contradiction"
-Level 5
+World "Implication"
+Level 20

 Title "Nicht-nicht"

@@ -7,8 +7,8 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted

 Game "TestGame"
-World "Contradiction"
-Level 6
+World "Proving"
+Level 2

 Title "Widerspruch"

@@ -7,8 +7,8 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted

 Game "TestGame"
-World "Contradiction"
-Level 7
+World "Proving"
+Level 3

 Title "Kontraposition"

@@ -7,8 +7,8 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted

 Game "TestGame"
-World "Contradiction"
-Level 8
+World "Implication"
+Level 2

 Title "Kontraposition"

@@ -5,7 +5,7 @@ import Mathlib
 import TestGame.ToBePorted

 Game "TestGame"
-World "Contradiction"
+World "Predicate"
 Level 9

 Title "PushNeg"
@@ -0,0 +1,14 @@
+import TestGame.Levels.Proposition.L01_Rfl
+import TestGame.Levels.Proposition.L02_Assumption
+import TestGame.Levels.Proposition.L03_Assumption
+import TestGame.Levels.Proposition.L04_True
+import TestGame.Levels.Proposition.L05_Not
+import TestGame.Levels.Proposition.L06_False
+import TestGame.Levels.Proposition.L07_ContraNotEq
+import TestGame.Levels.Proposition.L08_Contra
+import TestGame.Levels.Proposition.L09_And
+import TestGame.Levels.Proposition.L10_And
+import TestGame.Levels.Proposition.L11_Or
+import TestGame.Levels.Proposition.L12_Or
+import TestGame.Levels.Proposition.L13_Or
+import TestGame.Levels.Proposition.L14_Summary
@@ -1,7 +1,7 @@
 import TestGame.Metadata

 Game "TestGame"
-World "Logic"
+World "Proposition"
 Level 1

 Title "Aller Anfang ist... ein Einzeiler?"
@@ -20,7 +20,7 @@ man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas
 andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der
 Seite.

-Wenn der Beweis komplett ist, erscheint \"Level Completed! 🎉\".
+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.
 Gib die Taktik ein gefolgt von Enter ⏎.
@@ -1,14 +1,15 @@
 import TestGame.Metadata

 Game "TestGame"
-World "Logic"
-Level 3
+World "Proposition"
+Level 2

 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* (Assumptions). 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\".
@@ -20,7 +21,7 @@ zuerst eine natürliche Zahl $n$ und eine Annahme dass $1 < n$ gilt
 Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
 "

-Statement triviale_angelegenheit
+Statement
    "Angenommen $1 < n$. dann ist $1 < n$."
    (n : ℕ) (h : 1 < n) : 1 < n := by
  assumption
@@ -2,10 +2,10 @@ import TestGame.Metadata
 import Mathlib.Data.Nat.Basic -- TODO

 Game "TestGame"
-World "Logic"
-Level 4
+World "Proposition"
+Level 3

-Title "Logische Aussagen: `Prop`"
+Title "Logische Aussagen"

 Introduction
 "
@@ -16,7 +16,7 @@ Mit einer Annahme `(hA : A)` nimmt man an, dass $A$ wahr ist:
 `hA` ist sozusagen ein Beweis von $A$.
 "

-Statement mehr_triviales
+Statement
    "Sei $A$ eine logische Aussage und sei `hA` ein Beweis für $A$.
    Zeige, dass $A$ wahr ist."
    (A : Prop) (hA : A) : A := by
@@ -0,0 +1,34 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "Proposition"
+Level 4
+
+Title "True/False"
+
+Introduction
+"
+Unter den logischen Aussagen gibt es zwei spezielle Aussagen:
+
+- `True` ist eine Aussage, die immer und bedingungslos wahr ist.
+- `False` ist eine Aussage, die nie wahr ist.
+
+Die Aussage `True` werden wir kaum brauchen, die Aussage `False` ist jedoch wichtig, sie
+repräsentiert einen Widerspruch. Mehr dazu in den nächsten Levels.
+
+**Beachte**, dass beide gross geschrieben werden. In Lean gibt es auf das klein geschriebene
+`true` und `false`, diese sind aber etwas anderes (Typ `Bool` und nicht `Prop`)
+und werden erst mal nicht gebraucht.
+
+Wir können `True` aus dem nichts mit der Taktik `trivial` beweisen.
+
+*Bemerkung: Was die Taktik `trivial` kann und nicht kann bleibt in diesem Spiel ein bisschen eine Blackbox,
+aber manchmal ist sie nützlich.*
+"
+
+Statement "" : True := by
+  trivial
+
+Conclusion ""
+
+Tactics trivial
@@ -0,0 +1,22 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "Proposition"
+Level 5
+
+Title "Not"
+
+Introduction
+"
+Wenn eine Aussage `(A : Prop)` wahr oder falsch ist, dann ist die Umkehrung \"nicht $A$\",
+geschrieben `¬A` (`\\not`), gegenteilig falsch oder wahr.
+
+Da die Aussage `False` nie wahr ist, ist die Aussage `¬False` immer wahr, genau wie `True`.
+"
+
+Statement "Zeige dass die Aussage `¬False` immer wahr ist." : ¬False := by
+  trivial
+
+Conclusion ""
+
+Tactics trivial
@@ -3,22 +3,18 @@ import Std.Tactic.RCases
 import Mathlib.Tactic.LeftRight

 Game "TestGame"
-World "Contradiction"
-Level 1
+World "Proposition"
+Level 6

 Title "Widerspruch beweist alles."

 Introduction
 "
-Ein wichtiges Konzept ist die Verneinung und damit einhergehend die Kontraposition
-und der Widerspruch (Kontradiktion).
+Die Aussage `False` ist für uns wichtiger als `True`, da ein Beweis der falschen Aussage
+`False` einen Widerspruch repräsentiert.
+Hat man einen Widerspruch, kann man daraus mit der Taktik `contradiction` alles beweisen.

-Als allererstes der Widerspruch.
-
-Wenn man in den Annahmen einen Widerspruch hat, kann man mit `contradiction` den Beweis
-schliessen, denn ein Widerspruch beweist alles.
-
-Der einfachste Widerspruch ist wenn man einen Beweis von `False` hat:
+Der erste Widerspruch, den `contradiction` erkennt, ist ein Beweis von `False`.
 "

 Statement
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Proposition"
+Level 7
+
+Title "Widerspruch"
+
+Introduction
+"
+Zweitens kann `contradiction` auch aus Annahmen der Form `a ≠ a` einen Widerspruch finden.
+
+*Bemerkung:* Das Ungleichzeichen `≠` (`\\ne`) sollte immer als `¬(· = ·)` gelesen werden.
+"
+
+Statement
+    "Sei $n$ eine natürliche Zahl die ungleich sich selbst ist. Dann ist $n = 37$."
+    (n : ℕ) (h : n ≠ n) : n = 37 := by
+  contradiction
+
+Conclusion
+"
+"
+
+Tactics contradiction
@@ -0,0 +1,32 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Proposition"
+Level 8
+
+Title "Widerspruch"
+
+Introduction
+"
+Drittens kann die Taktik `contradiction` auch einen Widerspruch finden,
+wenn zwei Annahmen genaue Gegenteile voneinander sind.
+Also z.B. `(h : A)` und `(g : ¬ A)`.
+
+Da `≠` als `¬(· = ·)` gelesen wird, gilt dasselbe für Annahmen `(h : a = b)` und `(g : a ≠ b)`.
+"
+
+Statement absurd
+    "Sei $n$ eine natürliche Zahl die sowohl gleich als auch ungleich `10` ist.
+    Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)"
+    (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by
+  contradiction
+
+Conclusion
+"
+"
+
+Tactics contradiction
@@ -0,0 +1,104 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Proposition"
+Level 9
+
+Title "Und"
+
+Introduction
+"
+Zusätzlich zur Verneinung (`¬`) können wir logische Aussagen auch mit UND (`∧`) und ODER (`∨`) kombinieren.
+
+In einer Mathevorlesung würde man vielleicht `A ∧ B` als Tupel `⟨A, B⟩` definieren. In Lean
+sind dies *Strukturen*. Eine Struktur hat mehrere Felder, in diesem Fall zwei,
+nämlich die linke und die rechte Seite.
+
+Will man eine Aussage `A ∧ B` beweisen (im Goal), dann kann man diese mit der Taktik
+`constructor` in die einzelnen Felder aufteilen.
+"
+
+Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
+  constructor
+  assumption
+  assumption
+
+Message (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B =>
+  "`constructor` zerlegt die Struktur in Einzelteile."
+
+Hint (A : Prop) (hA : A) : A =>
+  "Du hast einen Beweis dafür in den *Annahmen*."
+
+Tactics constructor assumption
+
+-- Statement
+--     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
+--     (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
+--   constructor
+--   intro h
+--   rcases h with ⟨h₁, h₂⟩
+--   constructor
+--   assumption
+--   apply h₂
+--   assumption
+--   intro h
+--   rcases h with ⟨h₁, h₂⟩
+--   constructor
+--   assumption
+--   intro
+--   assumption
+
+-- Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
+-- "`↔` 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` zerlegen."
+
+-- Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
+-- "Wieder in Einzelteile zerlegen..."
+
+-- 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)`).
+
+-- -- 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."
+
+
+
+-- -- TODO
+
+
+-- Tactics apply rcases
+-- Tactics assumption
@@ -0,0 +1,105 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Proposition"
+Level 10
+
+Title "Und"
+
+Introduction
+"
+Hat man ein UND `(h : A ∧ B)` in den Annahmen, möchte man normalerweise die einzelnen Felder
+(linke/rechte Seite) einzeln verwenden. Dazu hat man zwei Möglichkeiten:
+
+1. Mit `h.left` und `h.right` (oder `h.1` und `h.2`) kann man die Felder direkt auswählen.
+2. Mit `rcases h with ⟨h₁, h₂⟩` kann man die Struktur `h` zerlegen und man erhält zwei
+   separate Annahmen `(h₁ : A)` und `(h₂ : B)`
+
+Die Klammern `⟨·,·⟩` sind `\\<` und `\\>` oder `\\<>` als Paar.
+"
+
+Statement "Benutze `rcases` um das UND in `(h : A ∧ (B ∧ C))` zu zerlegen und beweise, dass $B$ wahr ist."
+    (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by
+  rcases h with ⟨_, ⟨g , _⟩⟩
+  assumption
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B =>
+  "Du kannst mit `rcases` auch verschachtelt mehrere Strukturen in einem Schritt zerlegen:
+  `rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`."
+
+Hint (A : Prop) (hA : A) : A =>
+  "Du hast einen Beweis dafür in den *Annahmen*."
+
+Tactics constructor assumption
+
+-- Statement
+--     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
+--     (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
+--   constructor
+--   intro h
+--   rcases h with ⟨h₁, h₂⟩
+--   constructor
+--   assumption
+--   apply h₂
+--   assumption
+--   intro h
+--   rcases h with ⟨h₁, h₂⟩
+--   constructor
+--   assumption
+--   intro
+--   assumption
+
+-- Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
+-- "`↔` 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` zerlegen."
+
+-- Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
+-- "Wieder in Einzelteile zerlegen..."
+
+-- 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)`).
+
+-- -- 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."
+
+
+
+-- -- TODO
+
+
+-- Tactics apply rcases
+-- Tactics assumption
@@ -5,8 +5,8 @@ import Mathlib.Tactic.LeftRight
 --set_option tactic.hygienic false

 Game "TestGame"
-World "Logic"
-Level 15
+World "Proposition"
+Level 11

 Title "Oder"

@@ -14,7 +14,7 @@ Introduction
 "
 Das logische ODER `A ∨ B` (`\\or`) funktioniert ein wenig anders als das UND.

-Wenn das Goal ein `∨` ist kann man mit `left` oder `right` entscheiden,
+Wenn das Goal ein `∨` ist kann man mit den Taktiken `left` oder `right` entscheiden,
 welche Seite man beweisen möchte.
 "

@@ -8,8 +8,8 @@ import Mathlib.Tactic.LeftRight


 Game "TestGame"
-World "Logic"
-Level 16
+World "Proposition"
+Level 12

 Title "Oder - Bonus"

@@ -20,7 +20,7 @@ Wenn man hingegen ein ODER `(h : A ∨ B)` in den Annahmen hat, kann man dieses

 **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₂⟩$).
+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.
 "
@@ -0,0 +1,71 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Proposition"
+Level 13
+
+Title "Und/Oder"
+
+Introduction
+"
+Übung macht den Meister: Benutze alle vier Methoden mit UND und ODER
+umzugehen um folgende Aussage zu beweisen.
+
+|         | Und (`∧`)                | Oder (`∨`)              |
+|---------|:-------------------------|:------------------------|
+| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` |
+| Goal    | `constructor`            | `left`/`right`          |
+"
+
+-- Note: The other direction would need arguing by cases.
+
+Statement or_and_left
+    "Angenommen $A \\lor (B \\land C)$ ist wahr, zeige dass
+    $(A \\lor B) \\land (A \\lor C)$ wahr ist."
+    (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
+  constructor
+  rcases h with h | h
+  left
+  assumption
+  rcases h with ⟨h₁, h₂⟩
+  right
+  assumption
+  rcases h with h | h
+  left
+  assumption
+  rcases h with ⟨h₁, h₂⟩
+  right
+  assumption
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
+"Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
+"Das `∧` im Goal kann mit `constructor` zerlegt werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
+"Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
+"Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) =>
+"Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden."
+
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
+"Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
+"Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden."
+
+-- TODO: Message nur Anhand der Annahmen?
+
+Hint (A : Prop) (B : Prop) : A ∨ B =>
+"`left` oder `right`?"
+
+Tactics left right assumption constructor rcases
@@ -0,0 +1,79 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Proposition"
+Level 14
+
+Title "Zusammenfassung"
+
+Introduction
+"
+## Notationen / Begriffe
+
+Damit bist du am Ende der ersten Lektion angekommen. Hier ein Überblick über alle Begriffe und Notationen, die in diesem Kapitel
+eingeführt wurden.
+
+|               | Beschreibung                                                                          |
+|:--------------|:-------------------------------------------------------------------------|
+| *Goal*        | Was aktuell zu beweisen ist.                                             |
+| *Annahme*     | Objekte & Resultate, die man zur Verfügung hat.                          |
+| *Taktik*      | Befehl im Beweis. Entspricht einem Beweisschritt.                        |
+| `ℕ`           | Typ aller natürlichen Zahlen.                                            |
+| `0, 1, 2, …`  | Explizite natürliche Zahlen.                                             |
+| `=`           | Gleichheit.                                                              |
+| `≠`           | Ungleichheit. Abkürzung für `¬(·=·)`.                                    |
+| `Prop`        | Typ aller logischen Aussagen.                                            |
+| `True`        | Die logische Aussage `(True : Prop)` ist bedingungslos wahr.             |
+| `False`       | Die logische Aussage `(False : Prop)` ist bedingungslos falsch.          |
+| `¬`           | Logische Negierung.                                                      |
+| `∧`           | Logisch UND.                                                             |
+| `∨`           | Logisch ODER.                                                            |
+| `(n : ℕ)`     | Eine natürliche Zahl.                                                    |
+| `(A : Prop)`  | Eine logische Aussage.                                                   |
+| `(ha : A)`    | Ein Beweis, dass die logische Aussage `(A : Prop)` wahr ist.             |
+| `(h : A ∧ B)` | Eine Annahme, die den Namen `h` bekommen hat.                            |
+| `⟨·,·⟩`       | Schreibweise für Struktur mit mehreren Feldern (kommt später im Detail). |
+
+Im weiteren haben wir gesehen, wie wir in Lean Aufgaben/Sätze formulieren :
+
+```
+example [Annahmen] : [Aussage] := by
+  [Beweis]
+
+lemma [Name] [Annahmen] : [Aussage] := by
+  [Beweis]
+```
+
+Der Unterschied ist lediglich, dass Lemmas einen Namen haben und darum später
+wiederverwendet werden können (siehe spätere Kapitel). \"Examples\" kriegen keinen Namen.
+
+## Taktiken
+
+Für die Beweise haben wir verschiedene Taktiken kennengelernt.
+
+|   | Taktik                    | Beispiel                                          |
+|:--|:--------------------------|:--------------------------------------------------|
+| 1 | `rfl`                     | Beweist `A = A`.                                  |
+| 2 | `assumption`              | Sucht das Goal in den Annahmen.                   |
+| 3 | `contradiction`           | Sucht einen Widerspruch.                          |
+| 4 | `trivial`                 | Kombiniert die obigen drei Taktiken (und mehr).   |
+| 5 | `constructor`             | Teilt ein UND im Goal auf.                        |
+| 6 | `left`/`right`            | Beweist eine Seite eines ODER im Goal.            |
+| 7ᵃ | `rcases h with ⟨h₁, h₂⟩` | Teilt ein UND in den Annahmen auf.                |
+| 7ᵇ | `rcases h with h \\| h`  | Teilt ein ODER in den Annahmen in zwei Fälle auf. |
+
+
+Zum Schluss gibt es noch eine kleine Übungsaufgabe:
+
+"
+
+Statement
+    "TODO"
+    : True := by
+  trivial
+
+Tactics rfl assumption trivial left right constructor rcases
@@ -124,6 +124,13 @@ TacticDoc simp
 TODO
 "

+TacticDoc trivial
+"
+## Beschreibung
+
+TODO
+"
+
 TacticDoc contradiction
 "
 ## Beschreibung