Merge branch 'main' into main

2023-03-30 17:35:07 +02:00
parent e907c1fd5e f46b59163b
commit b8eccf3a8e
575 changed files with 238 additions and 8860 deletions
@@ -44,6 +44,7 @@ Statement "" (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by

 NewTactic «let»
 NewLemma Function.comp_apply
+LemmaTab "Function"

 Hint (x : ℤ) : ∃ g, (g ∘ f) x = x + 1 =>
 "**Du**: Ist `g ∘ f` Komposition von Funktionen?
@@ -54,7 +54,7 @@ Statement ""
 NewTactic funext by_cases simp_rw linarith

 NewLemma not_le if_pos if_neg
-
+LemmaTab "Logic"

 Hint : f ∘ g = g ∘ f =>
 "
@@ -31,7 +31,7 @@ Statement "" : Injective (fun (n : ℤ) ↦ n^3 + (n + 3)) := by

 NewDefinition Injective
 NewLemma StrictMono.injective StrictMono.add Odd.strictMono_pow
-
+LemmaTab "Function"

 Hint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
 "**Du**: Hmm, das ist etwas schwieriger…
@@ -34,6 +34,7 @@ heißen bei `(h : A ↔ B)` die beiden Teile `h.mp` und `h.mpr`.

 **Robo**: `mp` steht für Modus Ponens`.  Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen …  Ach nee, das wolltest Du ja nicht hören.  Das \"r\" in `mpr` steht für \"reverse\", weil's die Rückrichtung ist.
 "
+
 NewTactic constructor
 DisabledTactic tauto rw

@@ -46,5 +46,6 @@ Conclusion
 Der Operationsleiter nickt zustimmend.  Offenbar war ihm `not_or_of_imp` tatsächlich bekannt.
 "

+LemmaTab "Logic"
 NewLemma not_or_of_imp
 DisabledTactic tauto
@@ -40,3 +40,4 @@ Conclusion

 DisabledTactic tauto apply
 NewLemma not_not
+LemmaTab "Logic"
@@ -46,6 +46,7 @@ Statement Nat.pos_iff_ne_zero (n : ℕ) : 0 < n ↔ n ≠ 0 := by
 NewTactic simp
 NewLemma Nat.succ_pos
 DisabledLemma Nat.pos_iff_ne_zero
+LemmaTab "Nat"

 Conclusion "**Du**: Oh `simp` ist ja echt nicht schlecht…

@@ -22,5 +22,6 @@ Statement (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by

 NewTactic linarith
 NewLemma Nat.pos_iff_ne_zero
+LemmaTab "Nat"

 Conclusion "**Du**: Naja so beeindruckend war das jetzt auch noch nicht."
@@ -43,4 +43,5 @@ Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt!
 Meine Untertanen verstehen `tauto` nicht.  Da müsst Ihr Euch schon etwas mehr anstrengen.
 "

+LemmaTab "Logic"
 NewTactic tauto
@@ -29,21 +29,8 @@ Fast immer wenn man Gleichheiten von Mengen zeigen muss, will man diese in zwei
 aufteilen.
 "

-namespace MySet
-
 open Set Subset

-- Copied some lemmas from `Matlib.Data.Set.Basic` in order to not import the entire file.
-theorem tmp {α : Type _} {s t : Set α} : s = t → s ⊆ t :=
-  fun h₁ _ h₂ => by rw [← h₁] ; exact h₂
-
-theorem Subset.antisymm_iff {α : Type _} {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a :=
-  ⟨fun e => ⟨tmp e, tmp e.symm⟩, fun ⟨h₁, h₂⟩ => Set.ext fun _ => ⟨@h₁ _, @h₂ _⟩⟩
-
-@[simp]
-theorem empty_subset {α : Type _} (s : Set α) : ∅ ⊆ s :=
-  fun.
-
 Statement subset_empty_iff {A : Type _} (s : Set A) :
    s ⊆ ∅ ↔ s = ∅ := by
  Hint "**Du**: Ja, die einzige Teilmenge der leeren Menge ist die leere Menge.
@@ -53,16 +40,16 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
  Hint (hidden := true) "**Robo**: Fang doch einmal mit `constructor` an."
  constructor
  intro h
-  Hint "**Robo**: "
+  Hint "**Robo**: Gleichheit zwischen Mengen kann man zum Beispiel zeigen,
+  indem man `A ⊆ B` und `B ⊆ A` zeigt.
+
+  Dieser Schritt ist `apply Subset.antisymm`"
  apply Subset.antisymm
  assumption
-  simp only [empty_subset]
-  intro a
-  rw [Subset.antisymm_iff] at a
-  rcases a with ⟨h₁, h₂⟩
-  assumption
+  Hint "**Robo**: Hier ist das Lemma `empty_subset` hilfreich."
+  apply empty_subset
+  intro h
+  rw [h]

 DisabledTactic tauto
-NewLemma Subset.antisymm Subset.antisymm_iff empty_subset
-
-end MySet
+NewLemma Set.Subset.antisymm Set.Subset.antisymm_iff Set.empty_subset
@@ -12,39 +12,23 @@ Game "Adam"
 World "SetTheory"
 Level 5

-Title "Nonempty"
+Title "Empty"

 Introduction
 "
-Das Gegenteil von `A = ∅` ist `A ≠ ∅`, aber in Lean wird der Ausdruck `A.Nonempty` bevorzugt.
-Dieser ist dadurch existiert, dass in `A` ein Element existiert: `∃x, x ∈ A`.
-
-Zeige dass die beiden Ausdrücke äquivalent sind:
+Zeige folgendes Lemma, welches wir gleich brauchen werden:
 "

-namespace MySet
-
 open Set

-theorem subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by
-  constructor
-  intro h
-  rw [Subset.antisymm_iff]
-  constructor
-  assumption
-  simp only [empty_subset]
-  intro a
-  rw [Subset.antisymm_iff] at a
-  rcases a with ⟨h₁, h₂⟩
-  assumption

 Statement eq_empty_iff_forall_not_mem
 ""
    {A : Type _} (s : Set A) :
    s = ∅ ↔ ∀ x, x ∉ s := by
+  Hint "Das Lemma `subset_empty_iff` von letzter Aufgabe könnte hilfreich sein."
  rw [←subset_empty_iff]
  rfl -- This is quite a miracle :)

 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-end MySet
+NewLemma Set.subset_empty_iff
@@ -25,9 +25,13 @@ Statement nonempty_iff_ne_empty
 ""
    {A : Type _} (s : Set A) :
    s.Nonempty ↔ s ≠ ∅ := by
-  rw [Set.Nonempty]
+  Hint "Am besten fängst du mit `unfold Set.Nonempty` an."
+  unfold Set.Nonempty
+  Hint "Mit `ne_eq` und `eq_empty_iff_forall_not_mem` kannst du hier weiterkommen."
  rw [ne_eq, eq_empty_iff_forall_not_mem]
+  Hint (hidden := true) "`push_neg` kann hier helfen."
  push_neg
  rfl

-NewTactic constructor intro rw assumption rcases simp tauto trivial
+NewLemma ne_eq Set.eq_empty_iff_forall_not_mem
+NewDefinition Set.Nonempty
@@ -31,3 +31,4 @@ Statement
  rw [univ_union]

 NewTactic constructor intro rw assumption rcases simp tauto trivial
+NewLemma Set.diff_inter Set.union_assoc Set.union_diff_distrib Set.univ_union