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, denn 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; sie ist 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
```