1. World 1: Conjunction🔗

Two rules, for conjunction (∧, “and”):

∧-introduction (∧I) makes A ∧ B from A and B,
∧-elimination (∧E) takes A ∧ B apart into A and B.

Zwei Regeln für die Konjunktion (∧, „und“):

∧-Einführung (∧I) macht aus A und B die Aussage A ∧ B,
∧-Beseitigung (∧E) zerlegt A ∧ B in A und B.

Tap the red circle on top of the goal A; the assumption A glows green. Tap it.

Tippe den roten Kreis oben am Ziel A an; die Annahme A leuchtet grün. Tippe sie an.

How to play: a red circle is something still to prove, a blue dot something you have. Tap one of them, then one of the parts that glow green: a line connects them. You are done when no red circle is left.

So wird gespielt: Ein roter Kreis ist etwas, das noch zu beweisen ist, ein blauer Punkt etwas, das du hast. Tippe eines davon an, dann eines der grün leuchtenden Teile: Eine Linie verbindet sie. Du bist fertig, wenn kein roter Kreis mehr übrig ist.

Not every assumption has to be used.

Nicht jede Annahme muss verwendet werden.

Two goals.

Zwei Ziele.

Your first rule. Tap the red circle of the goal, then ＋ below the picture, and choose ∧I. A new block appears: connect its output to the goal, then fill its two red circles.

Deine erste Regel. Tippe den roten Kreis des Ziels an, dann ＋ unter dem Bild, und wähle ∧I. Ein neuer Block erscheint: Verbinde seinen Ausgang mit dem Ziel und fülle dann seine beiden roten Kreise.

Your first rule block: it comes from ＋ below the board. ∧I has two inputs (red circles ?1 and ?2) and one output (blue dot ?1 ∧ ?2). Connect its output to the goal: then ?1 and ?2 become A and B, and its two red circles are what is left to prove.

Dein erster Regelblock: Er kommt über ＋ unter dem Spielfeld. ∧I hat zwei Eingänge (rote Kreise ?1 und ?2) und einen Ausgang (blauer Punkt ?1 ∧ ?2). Verbinde seinen Ausgang mit dem Ziel: Dann werden ?1 und ?2 zu A und B, und seine zwei roten Kreise sind, was noch zu beweisen bleibt.

An assumption can be used more than once.

Eine Annahme kann mehrfach verwendet werden.

From the Lean course, sheet 01-b. P ∧ Q ∧ R means P ∧ (Q ∧ R).

Aus dem Lean-Kurs, Blatt 01-b. P ∧ Q ∧ R bedeutet P ∧ (Q ∧ R).

Now take a conjunction apart. Add an ∧E block with ＋, feed A ∧ B into it and connect the right one of its outputs to the goal.

Jetzt zerlegst du eine Konjunktion. Nimm mit ＋ einen ∧E-Block, gib A ∧ B hinein und verbinde den richtigen seiner Ausgänge mit dem Ziel.

∧E takes a conjunction apart: one input ?1 ∧ ?2, two outputs ?1 and ?2. Feed A ∧ B into it, and use the output you need.

∧E zerlegt eine Konjunktion: ein Eingang ?1 ∧ ?2, zwei Ausgänge ?1 und ?2. Gib A ∧ B hinein und verwende den Ausgang, den du brauchst.

One ∧-elimination gives both parts.

Eine ∧-Beseitigung liefert beide Teile.

The shortest way is the best.

Der kürzeste Weg ist der beste.

Take apart, then put together again.

Zerlegen und wieder zusammensetzen.

Three goals from one assumption.

Drei Ziele aus einer Annahme.

Pick the parts you need.

Nimm die Teile, die du brauchst.

The final level of the world: regroup. In Lean, A ∧ B ∧ C means A ∧ (B ∧ C).

Das letzte Level der Welt: Umgruppieren. In Lean bedeutet A ∧ B ∧ C dasselbe wie A ∧ (B ∧ C).