use LemmaTab in levels

2023-03-30 14:59:28 +02:00
parent 3cbe336ccb
commit 85f0a2e559
8 changed files with 8 additions and 2 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…
@@ -45,5 +45,6 @@ Conclusion
 **Mechanikerin**: Danke vielmals, jetzt bin ich schon viel ruhiger.
 "

+LemmaTab "Logic"
 NewLemma not_or_of_imp
 DisabledTactic tauto
@@ -48,3 +48,4 @@ funktioniert.

 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