import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
-- `#min_imports`, ergänzt um Taktik-Module und ℚ.
import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Rat.Defs
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum

open Verso.Genre Manual
open Verso.Genre.Manual.InlineLean

set_option pp.rawOnError true
set_option verso.docstring.allowMissing true

#doc (Manual) "Erste Schritte" =>
%%%
htmlSplit := .never
tag := "erste-schritte"
file := "erste-schritte"
%%%

Ein Beweis in Lean beginnt mit `by` und besteht aus _Taktiken_.
Öffnen Sie die Übungsdatei `AlgebraInLean/Basics.lean`, setzen Sie den
Cursor in einen Beweis und beobachten Sie das _Infoview_-Panel: Es
zeigt zu jedem Zeitpunkt die Hypothesen und das noch zu zeigende Ziel.

# Vier Taktiken für den Anfang

* `norm_num` verrechnet konkrete Zahlen,
* `ring` beweist Gleichungen, die in jedem kommutativen Ring gelten,
* `omega` löst lineare Arithmetik über `ℕ` und `ℤ`,
* `rw [h]` schreibt mit einer Gleichung `h` um.

```lean
example : 2 + 3 = 5 := by norm_num

example (a b : ℤ) :
    (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

example (n : ℕ) (h : n < 5) : n ≤ 7 := by omega

example (x y : ℚ) (h : x = y) : x + 1 = y + 1 := by
  rw [h]
```

# Gruppen in Mathlib

Definition 2.1.1 des Skripts:

> *Definition (Gruppe).* Eine Gruppe ist eine nicht-leere Menge $`G`
  mit einer Abbildung $`m : G \times G \to G`, sodass folgende
  Eigenschaften gelten.  _Assoziativität:_ … _Neutrales Element:_ Es
  gibt genau ein Element $`e` aus $`G`, sodass für alle $`a` aus $`G`
  gilt: $`m(e,a) = m(a,e) = a`.  _Inverse Elemente:_ Für alle $`a`
  aus $`G` gibt es genau ein Element $`b` aus $`G`, sodass
  $`m(a,b) = m(b,a) = e` ist.

In Mathlib ist eine Gruppe eine Typklasse `Group G`.  Die Verknüpfung
schreibt sich `a * b`, das neutrale Element `1`, das Inverse `a⁻¹`;
die Axiome heißen `mul_assoc`, `one_mul`, `mul_one`,
`inv_mul_cancel`, `mul_inv_cancel`.

Ein Unterschied fällt auf: Das Skript _fordert_ die Eindeutigkeit von
neutralem Element und Inversen, Mathlib nicht.  Das ist kein
Widerspruch — die Eindeutigkeit folgt aus den übrigen Axiomen.  Genau
das beweisen wir jetzt, mit dem Standardargument aus der linearen
Algebra:

> Es sei $`e` ein weiteres Element, das von links neutral wirkt.
  Weil $`1` neutral ist, gilt $`e \cdot 1 = e`.  Weil $`e` neutral
  wirkt, gilt $`e \cdot 1 = 1`.  Zusammen folgt
  $`e = e \cdot 1 = 1`.

Der Lean-Beweis benutzt die Taktik `calc`, die eine Kette von
Gleichungen Schritt für Schritt abarbeitet — das Lean-Gegenstück zur
Gleichungskette am Ende des Textbeweises:

```lean
theorem neutral_eindeutig {G : Type*} [Group G] (e : G)
    (he : ∀ a : G, e * a = a) : e = 1 := by
  -- „Weil 1 neutral ist, gilt e·1 = e.  Weil e neutral
  --  wirkt, gilt e·1 = 1.  Zusammen folgt e = e·1 = 1.“
  calc e = e * 1 := (mul_one e).symm
    _ = 1 := he 1
```

# Übungsaufgabe

Zeigen Sie ebenso die Eindeutigkeit des Inversen: Wenn
$`a \cdot b = 1` ist, dann ist $`b` bereits _das_ Inverse $`a^{-1}`.
Das Standardargument:

$$`b = 1 \cdot b = (a^{-1} \cdot a) \cdot b = a^{-1} \cdot (a \cdot b) = a^{-1} \cdot 1 = a^{-1}`

Öffnen Sie
`AlgebraInLean/Basics.lean` und ersetzen Sie das `sorry` durch einen
Beweis — `calc` und die Lemmata `one_mul`, `inv_mul_cancel`,
`mul_assoc`, `mul_one` genügen.

```lean
theorem inverses_eindeutig {G : Type*} [Group G] (a b : G)
    (h : a * b = 1) : b = a⁻¹ := by
  sorry
```