diff --git a/server/adam/Adam/Levels/Contradiction/L01_Have.lean b/server/adam/Adam/Levels/Contradiction/L01_Have.lean index 39c85bc..2543477 100644 --- a/server/adam/Adam/Levels/Contradiction/L01_Have.lean +++ b/server/adam/Adam/Levels/Contradiction/L01_Have.lean @@ -1,9 +1,4 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean index 8b33da1..9b1b902 100644 --- a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean +++ b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean @@ -1,9 +1,4 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean index 6d3e7cb..6111d61 100644 --- a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean @@ -1,10 +1,4 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring -import Mathlib import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean index c16ae6c..406a41c 100644 --- a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean @@ -1,10 +1,4 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring -import Mathlib import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean index a040cec..33b9308 100644 --- a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean +++ b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean @@ -1,8 +1,5 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean index c578ce3..3acae7a 100644 --- a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean +++ b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean @@ -1,8 +1,4 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Function/L01_Function.lean b/server/adam/Adam/Levels/Function/L01_Function.lean index ea9852d..93774d5 100644 --- a/server/adam/Adam/Levels/Function/L01_Function.lean +++ b/server/adam/Adam/Levels/Function/L01_Function.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" @@ -50,7 +51,7 @@ Statement "" : ∃ f : ℤ → ℤ, ∀ x, f x < x := by Branch intro x Hint (hidden := true) "**Du**: Zu was sich das wohl vereinfacht?" - simp + simp only [sub_lt_self_iff, forall_const] NewDefinition Symbol.function LemmaTab "Function" diff --git a/server/adam/Adam/Levels/Function/L02_Let.lean b/server/adam/Adam/Levels/Function/L02_Let.lean index 681dce4..8ce9817 100644 --- a/server/adam/Adam/Levels/Function/L02_Let.lean +++ b/server/adam/Adam/Levels/Function/L02_Let.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Function/L03_Piecewise.lean b/server/adam/Adam/Levels/Function/L03_Piecewise.lean index 8a65132..410fb40 100644 --- a/server/adam/Adam/Levels/Function/L03_Piecewise.lean +++ b/server/adam/Adam/Levels/Function/L03_Piecewise.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Function/L04_Injective.lean b/server/adam/Adam/Levels/Function/L04_Injective.lean index cc7060e..a6243d9 100644 --- a/server/adam/Adam/Levels/Function/L04_Injective.lean +++ b/server/adam/Adam/Levels/Function/L04_Injective.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Function/L05_Injective.lean b/server/adam/Adam/Levels/Function/L05_Injective.lean index 25b3f48..032c91f 100644 --- a/server/adam/Adam/Levels/Function/L05_Injective.lean +++ b/server/adam/Adam/Levels/Function/L05_Injective.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Function/L06_Injective.lean b/server/adam/Adam/Levels/Function/L06_Injective.lean index 4dbe301..41122ef 100644 --- a/server/adam/Adam/Levels/Function/L06_Injective.lean +++ b/server/adam/Adam/Levels/Function/L06_Injective.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Function/L07_Surjective.lean b/server/adam/Adam/Levels/Function/L07_Surjective.lean index 43fc61c..8cc739f 100644 --- a/server/adam/Adam/Levels/Function/L07_Surjective.lean +++ b/server/adam/Adam/Levels/Function/L07_Surjective.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Function/L08_Bijective.lean b/server/adam/Adam/Levels/Function/L08_Bijective.lean index 80336b7..e444faa 100644 --- a/server/adam/Adam/Levels/Function/L08_Bijective.lean +++ b/server/adam/Adam/Levels/Function/L08_Bijective.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Function/L09_Inverse.lean b/server/adam/Adam/Levels/Function/L09_Inverse.lean index a8353ec..04c909f 100644 --- a/server/adam/Adam/Levels/Function/L09_Inverse.lean +++ b/server/adam/Adam/Levels/Function/L09_Inverse.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/Implication/L01_Intro.lean b/server/adam/Adam/Levels/Implication/L01_Intro.lean index 6da930a..f72c1ba 100644 --- a/server/adam/Adam/Levels/Implication/L01_Intro.lean +++ b/server/adam/Adam/Levels/Implication/L01_Intro.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Tauto +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Implication/L03_Apply.lean b/server/adam/Adam/Levels/Implication/L03_Apply.lean index e1f348f..bf6f44e 100644 --- a/server/adam/Adam/Levels/Implication/L03_Apply.lean +++ b/server/adam/Adam/Levels/Implication/L03_Apply.lean @@ -1,5 +1,4 @@ import Adam.Metadata -import Mathlib Game "Adam" World "Implication" @@ -11,7 +10,7 @@ Introduction " Leider läuft das Telefonat nicht so gut. Er legt wieder auf und schüttelt mit dem Kopf. -**Operationsleiter**: Der Kollege auf der anderen Seite des Mondes versteht kein `revert`. Oder er tut zumindest so. Habt Ihr noch eine andere Idee? +**Operationsleiter**: Der Kollege auf der anderen Seite des Mondes versteht kein `revert`. Oder er tut zumindest so. Habt Ihr noch eine andere Idee? Er zieht eine Linie unter Euren Beweis, ergänzt ein durchgestrichenes ~`revert`~, und legt Euch das Blatt ein zweites Mal vor. " diff --git a/server/adam/Adam/Levels/Implication/L09_Iff.lean b/server/adam/Adam/Levels/Implication/L09_Iff.lean index cb94a05..7e86e99 100644 --- a/server/adam/Adam/Levels/Implication/L09_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L09_Iff.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.Cases +import Adam.Options.MathlibPart Game "Adam" World "Implication" @@ -10,9 +10,9 @@ Title "Genau dann wenn" Introduction " -**Operationsleiter**: Ah, die nächste Seite ist auch von diesem Kollegen. Aber da ist noch eine Notiz bei. Wir hatten hierfür schon einmal einen Beweis, aber den mochte er nicht. Er wollte einen Beweis, der weder `rw` noch `apply` verwendet!! +**Operationsleiter**: Ah, die nächste Seite ist auch von diesem Kollegen. Aber da ist noch eine Notiz bei. Wir hatten hierfür schon einmal einen Beweis, aber den mochte er nicht. Er wollte einen Beweis, der weder `rw` noch `apply` verwendet!! -Er holt tief Luft und seuft. +Er holt tief Luft und seuft. **Operationsleiter**: Ich glaube, der stellt sich immer viel dümmer, als er ist. Aber meint Ihr, Ihr schafft das? " diff --git a/server/adam/Adam/Levels/Implication/L10_Apply.lean b/server/adam/Adam/Levels/Implication/L10_Apply.lean index e88a6ed..5223c4e 100644 --- a/server/adam/Adam/Levels/Implication/L10_Apply.lean +++ b/server/adam/Adam/Levels/Implication/L10_Apply.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Cases -import Mathlib +import Adam.Options.MathlibPart + Game "Adam" World "Implication" @@ -20,13 +19,13 @@ Statement (A : Prop) : ¬A ∨ A := by Hint "**Du**: Das scheint wieder ziemlich offensichtlich. **Robo**: Nee, offensichtlich ist das nicht. Aber ich glaube, es gibt ein wohlbekanntens Lemma, das hier weiterhilft: - `not_or_of_imp` besagt `(A → B) → ¬ A ∨ B`. Da die rechte Seite der Implikation mit deinem Beweisziel übereinstimmt, + `not_or_of_imp` besagt `(A → B) → ¬ A ∨ B`. Da die rechte Seite der Implikation mit deinem Beweisziel übereinstimmt, kannst du es mit `apply not_or_of_imp` anwenden. **Du**: `Wohlbekannt` auf Implis? **Robo**: Werden wir sehen. Probiers aus!" - Branch + Branch right Hint "**Du**: Und jetzt? diff --git a/server/adam/Adam/Levels/Implication/L11_ByCases.lean b/server/adam/Adam/Levels/Implication/L11_ByCases.lean index ccdf73a..61f121c 100644 --- a/server/adam/Adam/Levels/Implication/L11_ByCases.lean +++ b/server/adam/Adam/Levels/Implication/L11_ByCases.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Cases -import Mathlib +import Adam.Options.MathlibPart + Game "Adam" World "Implication" @@ -11,7 +10,7 @@ Title "by_cases" Introduction " -**Du**: Sag mal, hätten wir nicht auch einfach zwei Fälle anschauen können? +**Du**: Sag mal, hätten wir nicht auch einfach zwei Fälle anschauen können? Wenn `A` wahr ist, beweisen wir die rechte Seite, sonst die Linke. **Robo**: Tatsächlich, `by_cases h : A` würde genau das machen! diff --git a/server/adam/Adam/Levels/Implication/L12_Rw.lean b/server/adam/Adam/Levels/Implication/L12_Rw.lean index 44e455a..4ca425e 100644 --- a/server/adam/Adam/Levels/Implication/L12_Rw.lean +++ b/server/adam/Adam/Levels/Implication/L12_Rw.lean @@ -1,7 +1,5 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Cases -import Mathlib.Logic.Basic +import Adam.Options.MathlibPart Game "Adam" World "Implication" diff --git a/server/adam/Adam/Levels/Implication/L13_Summary.lean b/server/adam/Adam/Levels/Implication/L13_Summary.lean index 660971a..b2d4d6f 100644 --- a/server/adam/Adam/Levels/Implication/L13_Summary.lean +++ b/server/adam/Adam/Levels/Implication/L13_Summary.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib + +import Adam.Options.MathlibPart set_option tactic.hygienic false @@ -17,7 +16,7 @@ Introduction **Du**: Klar, zeig her! Robo, kannst du mir vielleicht auch noch einmal so eine nette Zusammenfassung anzeigen, was ich theoretisch in den letzten fünf Minuten gelernt habe? -**Robo**: Hier ist die Übersicht: +**Robo**: Hier ist die Übersicht: ## Notationen / Begriffe @@ -41,10 +40,10 @@ Introduction Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by constructor - Hint "**Du** *(flüsternd)*: Ist das nicht die Definition von `→`? + Hint "**Du** *(flüsternd)*: Ist das nicht die Definition von `→`? - **Robo** *(flüsternd)*: Könnte man so sehen. Aber auf Leansch ist das bloß eine Äquivalenz. - So oder so kennst du ja eine Richtung schon als Lemma. + **Robo** *(flüsternd)*: Könnte man so sehen. Aber auf Leansch ist das bloß eine Äquivalenz. + So oder so kennst du ja eine Richtung schon als Lemma. Also wende das doch einfach an." apply not_or_of_imp Hint "**Du**: Gibt es für die Gegenrichtung auch ein Lemma? @@ -69,7 +68,7 @@ Ihr wollt bestimmt weiter zu Quantus, unserem Schestermond, oder? **Du**: Klar! Robo, halt mal. -Robo nimmt das Päckchen und lässt es irgendwo in seinem Innern verschwinden. +Robo nimmt das Päckchen und lässt es irgendwo in seinem Innern verschwinden. Der Operationsleiter sieht ihn entgeistert an. **Robo**: Keine Angst, ich verdaue nichts!" diff --git a/server/adam/Adam/Levels/Induction/L01_Induction.lean b/server/adam/Adam/Levels/Induction/L01_Induction.lean index 66a8473..b9c9c92 100644 --- a/server/adam/Adam/Levels/Induction/L01_Induction.lean +++ b/server/adam/Adam/Levels/Induction/L01_Induction.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib + set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Inequality/L02_Pos.lean b/server/adam/Adam/Levels/Inequality/L02_Pos.lean index ea47042..1cb0a3d 100644 --- a/server/adam/Adam/Levels/Inequality/L02_Pos.lean +++ b/server/adam/Adam/Levels/Inequality/L02_Pos.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Tactic.LibrarySearch +import Adam.Options.MathlibPart set_option tactic.hygienic false @@ -39,9 +39,11 @@ Statement Nat.pos_iff_ne_zero (n : ℕ) : 0 < n ↔ n ≠ 0 := by simp Hint "**Du**: Ah und jetzt falls `n ≠ 0`." Branch - simp + simp only [ne_eq, succ_ne_zero, not_false_iff, iff_true] Hint "**Robo**: Warte! Den Rest geb ich dir als Lemma: `Nat.suc_pos`." apply Nat.succ_pos + Branch + simp? constructor intro simp @@ -51,7 +53,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 +DisabledLemma Nat.pos_iff_ne_zero Nat.succ_pos' LemmaTab "Nat" Conclusion "**Du**: Oh `simp` ist ja echt nicht schlecht… diff --git a/server/adam/Adam/Levels/Inequality/L03_Linarith.lean b/server/adam/Adam/Levels/Inequality/L03_Linarith.lean index 958bfe9..0cb4095 100644 --- a/server/adam/Adam/Levels/Inequality/L03_Linarith.lean +++ b/server/adam/Adam/Levels/Inequality/L03_Linarith.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Linarith +import Adam.Options.MathlibPart Game "Adam" World "Inequality" diff --git a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean index 1509966..6a8b886 100644 --- a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean +++ b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Linarith +import Adam.Options.MathlibPart Game "Adam" World "Inequality" diff --git a/server/adam/Adam/Levels/Inequality/T_Induction.lean b/server/adam/Adam/Levels/Inequality/T_Induction.lean index 0d0830b..1a4add5 100644 --- a/server/adam/Adam/Levels/Inequality/T_Induction.lean +++ b/server/adam/Adam/Levels/Inequality/T_Induction.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib + Game "Adam" World "Inequality" diff --git a/server/adam/Adam/Levels/Lean/L01_Type.lean b/server/adam/Adam/Levels/Lean/L01_Type.lean index eb4a62d..878296e 100644 --- a/server/adam/Adam/Levels/Lean/L01_Type.lean +++ b/server/adam/Adam/Levels/Lean/L01_Type.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Lean/L02_Universe.lean b/server/adam/Adam/Levels/Lean/L02_Universe.lean index 91ae55e..ee3dbdd 100644 --- a/server/adam/Adam/Levels/Lean/L02_Universe.lean +++ b/server/adam/Adam/Levels/Lean/L02_Universe.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean b/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean index 4a75f22..6590917 100644 --- a/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean +++ b/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean @@ -1,6 +1,7 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart + import Adam.ToBePorted set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean b/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean index 9573286..a362bd4 100644 --- a/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean +++ b/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean @@ -1,6 +1,7 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart + import Adam.ToBePorted set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/LeftOvers/L09_Or.lean b/server/adam/Adam/Levels/LeftOvers/L09_Or.lean index b572c8a..703fc5c 100644 --- a/server/adam/Adam/Levels/LeftOvers/L09_Or.lean +++ b/server/adam/Adam/Levels/LeftOvers/L09_Or.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean b/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean index 419f94a..8d9ad9d 100644 --- a/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean +++ b/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "Nat2" diff --git a/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean b/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean index 49188d0..a16cebb 100644 --- a/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean +++ b/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "Nat2" diff --git a/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean b/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean index f1847f8..bf246d2 100644 --- a/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean +++ b/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean @@ -1,8 +1,5 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart -- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet def even (a : ℕ) : Prop := ∃ r, a = 2 * r diff --git a/server/adam/Adam/Levels/LeftOvers/Playground.lean b/server/adam/Adam/Levels/LeftOvers/Playground.lean index b1f5e6a..8ccfefa 100644 --- a/server/adam/Adam/Levels/LeftOvers/Playground.lean +++ b/server/adam/Adam/Levels/LeftOvers/Playground.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib + -- -- INCORPORATED -- example (A B : Prop) : (A → B) ↔ (¬ B → ¬A) := by diff --git a/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean b/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean index 87d457f..403a75b 100644 --- a/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean +++ b/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "Function" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean b/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean index d1866ec..4e6eb93 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean @@ -1,8 +1,7 @@ import Adam.Metadata -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Algebra.Module.Basic -- definiert `module` -import Mathlib.Tactic.LibrarySearch +import Adam.Options.MathlibPart + import Adam.StructInstWithHoles set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean b/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean index c0b6be3..e322d11 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean @@ -1,9 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Algebra.Module.Pi -- definiert `Module ℚ (fin 2 → ℚ)` -import Mathlib.Data.Fin.VecNotation -import Mathlib.Tactic.FinCases +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean b/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean index b49b982..53d2fe4 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean @@ -1,9 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Algebra.Module.Pi -- definiert `Module ℚ (fin 2 → ℚ)` -import Mathlib.Data.Fin.VecNotation -import Mathlib.Tactic.FinCases +import Adam.Options.MathlibPart Game "Adam" World "Module" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean b/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean index 964e47a..294f05a 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice +import Adam.Options.MathlibPart Game "Adam" World "Module" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean b/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean index 6709165..2884d6b 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice +import Adam.Options.MathlibPart Game "Adam" World "Module" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean index 9a22ee5..7d4b557 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean @@ -1,12 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Data.Fin.VecNotation -- Importiert Matrix/Vektor-Notation ---import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun` -import Mathlib.Tactic.FinCases -import Mathlib.Algebra.BigOperators.Finsupp -- default? -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart Game "Adam" World "Module" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean index a50946b..e7854df 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean @@ -1,14 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Data.Fin.VecNotation -- Importiert Matrix/Vektor-Notation ---import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun` -import Mathlib.Tactic.FinCases -import Mathlib.Algebra.BigOperators.Finsupp -- default? -import Mathlib.LinearAlgebra.Span -import Mathlib.Tactic.LibrarySearch -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "Module" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean b/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean index 9d20601..271aa84 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean @@ -1,12 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Data.Fin.VecNotation -- Importiert Matrix/Vektor-Notation ---import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun` -import Mathlib.Tactic.FinCases -import Mathlib.Algebra.BigOperators.Finsupp -- default? -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart Game "Adam" World "Module" diff --git a/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean b/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean index 258e0d4..1391df8 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean @@ -1,9 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ` -import Mathlib.Tactic.FinCases -import Mathlib.Data.Fin.VecNotation +import Adam.Options.MathlibPart Game "Adam" World "Basis" diff --git a/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean b/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean index 359fe45..200db01 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean @@ -1,14 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ` -import Mathlib.Tactic.FinCases -import Mathlib.Data.Fin.VecNotation --- import Mathlib.LinearAlgebra.Finsupp -import Mathlib.Algebra.BigOperators.Basic -- default --- import Mathlib.LinearAlgebra.LinearIndependent -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "Basis" diff --git a/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean b/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean index c8145e1..887d7e9 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "Basis" diff --git a/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean index c9d4aaf..d824f0e 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean @@ -1,12 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Data.Fin.VecNotation -- Importiert Matrix/Vektor-Notation ---import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun` -import Mathlib.Tactic.FinCases -import Mathlib.Algebra.BigOperators.Finsupp -- default? -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart Game "Adam" World "Module2" diff --git a/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean index decc953..850491a 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean @@ -1,13 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -- definiert `ℝ` -import Mathlib.Data.Fin.VecNotation -- Importiert Matrix/Vektor-Notation ---import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun` -import Mathlib.Tactic.FinCases -import Mathlib.Algebra.BigOperators.Finsupp -- default? -import Mathlib.LinearAlgebra.Span -import Mathlib +import Adam.Options.MathlibPart open Submodule diff --git a/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean b/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean index ceb7558..90400e1 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -import Mathlib.LinearAlgebra.Basic +import Adam.Options.MathlibPart Game "Adam" World "Module2" diff --git a/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean b/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean index fecaebb..6c53e4f 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -import Mathlib.LinearAlgebra.Basic +import Adam.Options.MathlibPart Game "Adam" World "Module2" diff --git a/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean b/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean index 18ad88c..401562e 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart open Submodule diff --git a/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean b/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean index d571449..52c2e03 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart open Submodule diff --git a/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean b/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean index ff1f973..09341f4 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart Game "Adam" World "Module2" diff --git a/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean b/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean index 3dcc9a0..a800016 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart universe u diff --git a/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean b/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean index 5b08aa3..672b5fa 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Data.Real.Basic -import Mathlib.LinearAlgebra.Span +import Adam.Options.MathlibPart Game "Adam" World "Module2" diff --git a/server/adam/Adam/Levels/Numbers/L01_PNat.lean b/server/adam/Adam/Levels/Numbers/L01_PNat.lean index d45f07a..66cf131 100644 --- a/server/adam/Adam/Levels/Numbers/L01_PNat.lean +++ b/server/adam/Adam/Levels/Numbers/L01_PNat.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib + Game "Adam" World "Numbers" diff --git a/server/adam/Adam/Levels/Numbers/L02_PNat.lean b/server/adam/Adam/Levels/Numbers/L02_PNat.lean index b073a3c..f5fbc73 100644 --- a/server/adam/Adam/Levels/Numbers/L02_PNat.lean +++ b/server/adam/Adam/Levels/Numbers/L02_PNat.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib + Game "Adam" World "Numbers" diff --git a/server/adam/Adam/Levels/Predicate/L01_Ring.lean b/server/adam/Adam/Levels/Predicate/L01_Ring.lean index ba94755..80d1876 100644 --- a/server/adam/Adam/Levels/Predicate/L01_Ring.lean +++ b/server/adam/Adam/Levels/Predicate/L01_Ring.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart --set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean index b75d669..4434f17 100644 --- a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean +++ b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib + Game "Adam" World "Predicate" diff --git a/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean index 0b7d2ba..eb5f3ef 100644 --- a/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean +++ b/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib + Game "Adam" World "Predicate" diff --git a/server/adam/Adam/Levels/Predicate/L04_Ring.lean b/server/adam/Adam/Levels/Predicate/L04_Ring.lean index fd3bf00..8a4e243 100644 --- a/server/adam/Adam/Levels/Predicate/L04_Ring.lean +++ b/server/adam/Adam/Levels/Predicate/L04_Ring.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "Predicate" diff --git a/server/adam/Adam/Levels/Predicate/L05_Rfl.lean b/server/adam/Adam/Levels/Predicate/L05_Rfl.lean index aeedf8e..1a45df8 100644 --- a/server/adam/Adam/Levels/Predicate/L05_Rfl.lean +++ b/server/adam/Adam/Levels/Predicate/L05_Rfl.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "Predicate" diff --git a/server/adam/Adam/Levels/Predicate/L06_Exists.lean b/server/adam/Adam/Levels/Predicate/L06_Exists.lean index 340751f..5532d23 100644 --- a/server/adam/Adam/Levels/Predicate/L06_Exists.lean +++ b/server/adam/Adam/Levels/Predicate/L06_Exists.lean @@ -1,10 +1,5 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring - -import Mathlib.Algebra.Parity +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Predicate/L07_Exists.lean b/server/adam/Adam/Levels/Predicate/L07_Exists.lean index 59e7309..e8736c4 100644 --- a/server/adam/Adam/Levels/Predicate/L07_Exists.lean +++ b/server/adam/Adam/Levels/Predicate/L07_Exists.lean @@ -1,10 +1,5 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring - -import Mathlib.Algebra.Parity +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Predicate/L08_Forall.lean b/server/adam/Adam/Levels/Predicate/L08_Forall.lean index cacf56a..c16b6b6 100644 --- a/server/adam/Adam/Levels/Predicate/L08_Forall.lean +++ b/server/adam/Adam/Levels/Predicate/L08_Forall.lean @@ -1,11 +1,5 @@ import Adam.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring - -import Mathlib.Algebra.Parity -import Mathlib +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean index 189290f..773369b 100644 --- a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean +++ b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Tactic.PushNeg -import Mathlib +import Adam.Options.MathlibPart -import Mathlib.Algebra.Parity import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Prime/L01_Dvd.lean b/server/adam/Adam/Levels/Prime/L01_Dvd.lean index 5e826eb..91a5901 100644 --- a/server/adam/Adam/Levels/Prime/L01_Dvd.lean +++ b/server/adam/Adam/Levels/Prime/L01_Dvd.lean @@ -1,7 +1,7 @@ import Adam.Metadata -import Mathlib.Tactic.Ring -import Mathlib +import Adam.Options.MathlibPart + Game "Adam" World "Prime" diff --git a/server/adam/Adam/Levels/Prime/L02_Prime.lean b/server/adam/Adam/Levels/Prime/L02_Prime.lean index 58231bf..bbd083f 100644 --- a/server/adam/Adam/Levels/Prime/L02_Prime.lean +++ b/server/adam/Adam/Levels/Prime/L02_Prime.lean @@ -1,13 +1,5 @@ import Adam.Metadata -import Mathlib.Data.Nat.Prime - -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring - --- import Data.Nat.Prime +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Prime/L03_Prime.lean b/server/adam/Adam/Levels/Prime/L03_Prime.lean index a437d02..ff5f64e 100644 --- a/server/adam/Adam/Levels/Prime/L03_Prime.lean +++ b/server/adam/Adam/Levels/Prime/L03_Prime.lean @@ -1,11 +1,5 @@ import Adam.Metadata -import Mathlib.Data.Nat.Prime - -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean b/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean index 3094ea7..e03c0a7 100644 --- a/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean +++ b/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean @@ -1,11 +1,5 @@ import Adam.Metadata -import Mathlib.Data.Nat.Prime - -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Proposition/L00_Tauto.lean b/server/adam/Adam/Levels/Proposition/L00_Tauto.lean index bc0d692..6b13754 100644 --- a/server/adam/Adam/Levels/Proposition/L00_Tauto.lean +++ b/server/adam/Adam/Levels/Proposition/L00_Tauto.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Tactic.Tauto +import Adam.Options.MathlibPart Game "Adam" World "Proposition" diff --git a/server/adam/Adam/Levels/Proposition/L03_Assumption.lean b/server/adam/Adam/Levels/Proposition/L03_Assumption.lean index 2f1ee24..91b0115 100644 --- a/server/adam/Adam/Levels/Proposition/L03_Assumption.lean +++ b/server/adam/Adam/Levels/Proposition/L03_Assumption.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Data.Nat.Basic -- TODO +import Adam.Options.MathlibPart Game "Adam" World "Proposition" diff --git a/server/adam/Adam/Levels/Proposition/L06_False.lean b/server/adam/Adam/Levels/Proposition/L06_False.lean index 6b888e6..55e29b3 100644 --- a/server/adam/Adam/Levels/Proposition/L06_False.lean +++ b/server/adam/Adam/Levels/Proposition/L06_False.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart Game "Adam" World "Proposition" diff --git a/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean b/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean index c941a88..7a64979 100644 --- a/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Proposition/L08_Contra.lean b/server/adam/Adam/Levels/Proposition/L08_Contra.lean index 94f4aa4..79244df 100644 --- a/server/adam/Adam/Levels/Proposition/L08_Contra.lean +++ b/server/adam/Adam/Levels/Proposition/L08_Contra.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Proposition/L11_Or.lean b/server/adam/Adam/Levels/Proposition/L11_Or.lean index b18eb3d..97925e5 100644 --- a/server/adam/Adam/Levels/Proposition/L11_Or.lean +++ b/server/adam/Adam/Levels/Proposition/L11_Or.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart --set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Proposition/L12_Or.lean b/server/adam/Adam/Levels/Proposition/L12_Or.lean index 58538d7..d5128f3 100644 --- a/server/adam/Adam/Levels/Proposition/L12_Or.lean +++ b/server/adam/Adam/Levels/Proposition/L12_Or.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/Proposition/L13_Summary.lean b/server/adam/Adam/Levels/Proposition/L13_Summary.lean index 7f16956..ec23431 100644 --- a/server/adam/Adam/Levels/Proposition/L13_Summary.lean +++ b/server/adam/Adam/Levels/Proposition/L13_Summary.lean @@ -1,6 +1,6 @@ import Adam.Metadata import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetFunction/L01_Image.lean b/server/adam/Adam/Levels/SetFunction/L01_Image.lean index 330d746..2499c3a 100644 --- a/server/adam/Adam/Levels/SetFunction/L01_Image.lean +++ b/server/adam/Adam/Levels/SetFunction/L01_Image.lean @@ -1,5 +1,6 @@ import Adam.Metadata -import Mathlib + +import Adam.Options.MathlibPart Game "Adam" World "SetFunction" diff --git a/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean b/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean index 657f18f..26dbd23 100644 --- a/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean +++ b/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "SetFunction" diff --git a/server/adam/Adam/Levels/SetFunction/L03_Range.lean b/server/adam/Adam/Levels/SetFunction/L03_Range.lean index 4809e8f..e30baf6 100644 --- a/server/adam/Adam/Levels/SetFunction/L03_Range.lean +++ b/server/adam/Adam/Levels/SetFunction/L03_Range.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "SetFunction" diff --git a/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean b/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean index f4cfd84..36090e2 100644 --- a/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean +++ b/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "SetFunction" diff --git a/server/adam/Adam/Levels/SetTheory/L01_Univ.lean b/server/adam/Adam/Levels/SetTheory/L01_Univ.lean index 25e22bb..b6017b8 100644 --- a/server/adam/Adam/Levels/SetTheory/L01_Univ.lean +++ b/server/adam/Adam/Levels/SetTheory/L01_Univ.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Mathlib.Init.Set -import Mathlib.Tactic.Tauto +import Adam.Options.MathlibPart set_option tactic.hygienic false set_option autoImplicit false diff --git a/server/adam/Adam/Levels/SetTheory/L02_Empty.lean b/server/adam/Adam/Levels/SetTheory/L02_Empty.lean index 10444aa..3f45c6d 100644 --- a/server/adam/Adam/Levels/SetTheory/L02_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L02_Empty.lean @@ -1,7 +1,5 @@ import Adam.Metadata - -import Mathlib.Init.Set -import Mathlib.Tactic.Tauto +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L03_Subset.lean b/server/adam/Adam/Levels/SetTheory/L03_Subset.lean index 8c1aeb9..eea45e1 100644 --- a/server/adam/Adam/Levels/SetTheory/L03_Subset.lean +++ b/server/adam/Adam/Levels/SetTheory/L03_Subset.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Mathlib.Init.Set -import Mathlib.Tactic.Tauto +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean index e43c949..56a15af 100644 --- a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean +++ b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean @@ -1,9 +1,7 @@ import Adam.Metadata import Adam.Levels.SetTheory.L03_Subset -import Mathlib.Init.Set -import Mathlib.Tactic.Tauto -import Mathlib +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean index 4c7cd3f..5581575 100644 --- a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean @@ -1,10 +1,7 @@ import Adam.Metadata import Adam.Levels.SetTheory.L04_SubsetEmpty ---import Mathlib.Data.Set.Basic -import Mathlib.Init.Set -import Mathlib.Tactic.Tauto -import Mathlib.Tactic.PushNeg +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean index ae29646..ae0c905 100644 --- a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean +++ b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean @@ -1,7 +1,7 @@ import Adam.Metadata import Adam.Levels.SetTheory.L05_Empty -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean index 8aefff9..772a94e 100644 --- a/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean index 23ff787..7b0076a 100644 --- a/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart set_option tactic.hygienic false diff --git a/server/adam/Adam/Levels/SetTheory/L09_Complement.lean b/server/adam/Adam/Levels/SetTheory/L09_Complement.lean index f0aed5c..a776fa2 100644 --- a/server/adam/Adam/Levels/SetTheory/L09_Complement.lean +++ b/server/adam/Adam/Levels/SetTheory/L09_Complement.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart Game "Adam" World "SetTheory" diff --git a/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean b/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean index 304f7b0..b9141a4 100644 --- a/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean +++ b/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart Game "Adam" World "SetTheory" diff --git a/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean b/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean index d45d422..969d7d0 100644 --- a/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean +++ b/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean @@ -1,5 +1,5 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart Game "Adam" World "SetTheory" diff --git a/server/adam/Adam/Levels/SetTheory/L12_Insert.lean b/server/adam/Adam/Levels/SetTheory/L12_Insert.lean index ac66274..a1195c4 100644 --- a/server/adam/Adam/Levels/SetTheory/L12_Insert.lean +++ b/server/adam/Adam/Levels/SetTheory/L12_Insert.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart Game "Adam" World "SetTheory" diff --git a/server/adam/Adam/Levels/SetTheory/L13_Insert.lean b/server/adam/Adam/Levels/SetTheory/L13_Insert.lean index c15c212..6dde7b9 100644 --- a/server/adam/Adam/Levels/SetTheory/L13_Insert.lean +++ b/server/adam/Adam/Levels/SetTheory/L13_Insert.lean @@ -1,6 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic +import Adam.Options.MathlibPart Game "Adam" World "SetTheory" diff --git a/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean b/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean index a6db524..88faf47 100644 --- a/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean +++ b/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "SetTheory2" diff --git a/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean b/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean index 49676c6..85ba280 100644 --- a/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean +++ b/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean b/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean index e590883..5fc21eb 100644 --- a/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean +++ b/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean @@ -1,8 +1,7 @@ import Adam.Metadata -import Mathlib -import Mathlib.Algebra.Parity -import Mathlib.Tactic.Ring + +import Adam.Options.MathlibPart Game "Adam" World "SetTheory2" diff --git a/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean b/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean index 5a2d9db..8a0c62b 100644 --- a/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean +++ b/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean @@ -1,8 +1,7 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib +import Adam.Options.MathlibPart + Game "Adam" World "SetTheory2" diff --git a/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean b/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean index 41fb86f..e183071 100644 --- a/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean +++ b/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean @@ -1,8 +1,7 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib +import Adam.Options.MathlibPart + Game "Adam" World "SetTheory2" diff --git a/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean b/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean index 8049e0a..d0ce8da 100644 --- a/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean +++ b/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "SetTheory2" diff --git a/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean index 0a60f72..b149cb1 100644 --- a/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib +import Adam.Options.MathlibPart Game "Adam" World "SetTheory2" diff --git a/server/adam/Adam/Levels/SetTheory/L21_Summary.lean b/server/adam/Adam/Levels/SetTheory/L21_Summary.lean index 91bcda1..bde2d22 100644 --- a/server/adam/Adam/Levels/SetTheory/L21_Summary.lean +++ b/server/adam/Adam/Levels/SetTheory/L21_Summary.lean @@ -1,8 +1,6 @@ import Adam.Metadata -import Mathlib.Data.Set.Basic -import Mathlib.Algebra.Parity -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "SetTheory" diff --git a/server/adam/Adam/Levels/SetTheory/PowersetPlayground.lean b/server/adam/Adam/Levels/SetTheory/PowersetPlayground.lean index 01f9e22..ef09c7f 100644 --- a/server/adam/Adam/Levels/SetTheory/PowersetPlayground.lean +++ b/server/adam/Adam/Levels/SetTheory/PowersetPlayground.lean @@ -1,4 +1,4 @@ -import Mathlib + open Set diff --git a/server/adam/Adam/Levels/SetTheory/T01_Set.lean b/server/adam/Adam/Levels/SetTheory/T01_Set.lean index 21e9d0b..f781751 100644 --- a/server/adam/Adam/Levels/SetTheory/T01_Set.lean +++ b/server/adam/Adam/Levels/SetTheory/T01_Set.lean @@ -1,296 +1,286 @@ -import Adam.Metadata +-- import Adam.Metadata -import Mathlib.Order.SymmDiff -import Mathlib.Logic.Function.Iterate -import Mathlib.Tactic.Use -import Mathlib.Tactic.SolveByElim -import Mathlib.Tactic.Tauto -import Mathlib.Tactic.ByContra -import Mathlib.Tactic.Lift -import Mathlib.Data.Set.Basic -import Mathlib.Data.Finset.Powerset -import Mathlib.Tactic.LibrarySearch -import Mathlib +-- import Adam.Options.MathlibPart -set_option tactic.hygienic false +-- set_option tactic.hygienic false -Game "Adam" -World "SetTheory" -Level 1 +-- Game "Adam" +-- World "SetTheory" +-- Level 1 -Title "Mengen" +-- Title "Mengen" -Introduction -" -In diesem Kapitel schauen wir uns Mengen an. +-- Introduction +-- " +-- In diesem Kapitel schauen wir uns Mengen an. -Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst, -alle Elemente in einer Menge haben den gleichen Typ. +-- Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst, +-- alle Elemente in einer Menge haben den gleichen Typ. -Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine -Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben. +-- Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine +-- Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben. -Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus -`X`. `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied -zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht -austauschbar! +-- Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus +-- `X`. `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied +-- zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht +-- austauschbar! -Am anderen Ende sitzt die leere Menge `(∅ : set X)` (`\\empty`). Bei `univ` und `∅` versucht Lean -automatisch den Typ zu erraten, in exotischen Beispielen muss man wie oben diesen explizit angeben. +-- Am anderen Ende sitzt die leere Menge `(∅ : set X)` (`\\empty`). Bei `univ` und `∅` versucht Lean +-- automatisch den Typ zu erraten, in exotischen Beispielen muss man wie oben diesen explizit angeben. -Als erste Operationen schauen wir uns `∪` (`\\union` oder `\\cup`), `∩` -(`\\inter` oder `\\cap`) und `\\` (`\\\\` oder `\\ `) +-- Als erste Operationen schauen wir uns `∪` (`\\union` oder `\\cup`), `∩` +-- (`\\inter` oder `\\cap`) und `\\` (`\\\\` oder `\\ `) -" +-- " -open Set +-- open Set -Statement - "Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr." - {X : Type _} {A B : Set X} : univ \ (A ∩ B) ∪ ∅ = (univ \ A) ∪ (univ \ B) ∪ (A \ B) := by - rw [Set.diff_inter] - rw [Set.union_empty] - rw [Set.union_assoc] - rw [←Set.union_diff_distrib] - rw [Set.univ_union] +-- Statement +-- "Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr." +-- {X : Type _} {A B : Set X} : univ \ (A ∩ B) ∪ ∅ = (univ \ A) ∪ (univ \ B) ∪ (A \ B) := by +-- rw [Set.diff_inter] +-- rw [Set.union_empty] +-- rw [Set.union_assoc] +-- rw [←Set.union_diff_distrib] +-- rw [Set.univ_union] -NewTactic rw +-- NewTactic rw -example : 4 ∈ (univ : Set ℕ) := by - trivial +-- example : 4 ∈ (univ : Set ℕ) := by +-- trivial -example (A : Set ℕ) : 4 ∉ (∅ : Set ℕ) := by - trivial +-- example (A : Set ℕ) : 4 ∉ (∅ : Set ℕ) := by +-- trivial -example (A : Set ℕ) : A ⊆ univ := by - intro x h - trivial +-- example (A : Set ℕ) : A ⊆ univ := by +-- intro x h +-- trivial --- -- subset_empty_iff --- example {s : Set α} : s ⊆ ∅ ↔ s = ∅ := by +-- -- -- subset_empty_iff +-- -- example {s : Set α} : 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 + +-- -- -- eq_empty_iff_forall_not_mem +-- -- example {s : Set α} : s = ∅ ↔ ∀ x, x ∉ s := by +-- -- rw [←subset_empty_iff] +-- -- rfl + +-- -- -- nonempty_iff_ne_empty +-- -- example (X : Type _) (s : Set X) : Set.Nonempty s ↔ s ≠ ∅ := by +-- -- rw [Set.Nonempty] +-- -- rw [ne_eq, eq_empty_iff_forall_not_mem] +-- -- push_neg +-- -- rfl + + +-- -- example (A B : ℝ): A = B ↔ A ≤ B ∧ B ≤ A := by library_search + +-- namespace Finset + +-- theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) : +-- Finset.powerset {x} = {∅, {x}} := by +-- ext y +-- rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton] + +-- end Finset + +-- /- The powerset of a singleton contains only `∅` and the singleton. -/ +-- theorem powerset_singleton {U : Type _} (x : U) : +-- 𝒫 ({x} : Set U) = {∅, {x}} := by +-- ext y +-- rw [mem_powerset_iff, subset_singleton_iff_eq] +-- rw [mem_insert_iff, mem_singleton_iff] + + +-- lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) : +-- S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by +-- rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff] + +-- -- lemma powerset_insert {U : Type _} (A : Set U) (x : U) : +-- -- 𝒫 (insert x A) = 𝒫 A ∪ ({B : Set U | B \ {x} ∈ 𝒫 A}) := by +-- -- sorry + +-- theorem subset_insert_iff_of_not_mem {U : Type _ }{s t : Set U} (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t := by +-- rw [subset_insert_iff, erase_eq_of_not_mem h] + +-- lemma mem_powerset_insert_iff₂ {U : Type _} (A S : Set U) (x : U) : +-- S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by +-- simp_rw [mem_powerset_iff] -- constructor --- intro h +-- · intro h +-- by_cases hs : x ∈ S +-- · sorry +-- · left +-- rw [Finset.subset_insert_iff_of_not_mem] +-- · intro h +-- rcases h with h | ⟨B, h₁, h₂⟩ +-- · exact le_trans h (subset_insert x A) +-- · rw [←h₂] +-- exact insert_subset_insert h₁ + +-- lemma powerset_insert {U : Type _} (A : Set U) (x : U) : +-- 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by -- rw [Subset.antisymm_iff] --- constructor --- assumption --- simp only [empty_subset] --- intro a --- rw [Subset.antisymm_iff] at a --- rcases a with ⟨h₁, h₂⟩ +-- constructor <;> +-- intro B hB <;> +-- simp_rw [mem_powerset_insert_iff₂, mem_union, mem_image] at hB ⊢ <;> -- assumption --- -- eq_empty_iff_forall_not_mem --- example {s : Set α} : s = ∅ ↔ ∀ x, x ∉ s := by --- rw [←subset_empty_iff] --- rfl --- -- nonempty_iff_ne_empty --- example (X : Type _) (s : Set X) : Set.Nonempty s ↔ s ≠ ∅ := by --- rw [Set.Nonempty] --- rw [ne_eq, eq_empty_iff_forall_not_mem] --- push_neg --- rfl +-- example : powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by +-- simp_rw [powerset_insert, powerset_singleton, Finset.powerset_insert, Finset.powerset_singleton] +-- simp only [image_insert_eq, union_insert, image_singleton, union_singleton] +-- simp only [insert_comm, ←insert_emptyc_eq] +-- example [DecidableEq ℕ] : Finset.powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by +-- repeat' rw [@ Finset.powerset_insert ℕ] +-- repeat' rw [@Finset.powerset_singleton ℕ] +-- --simp only [image_insert_eq, union_insert, image_singleton, union_singleton] --- example (A B : ℝ): A = B ↔ A ≤ B ∧ B ≤ A := by library_search -namespace Finset +-- example : powerset {0, 1, 2, 4} = +-- {∅, {0}, {1}, {0, 1}, {2}, {1, 2}, {0, 2}, {0, 1, 2}, +-- {4}, {0, 4}, {1, 4}, {0, 1, 4}, {2, 4}, {1, 2, 4}, {0, 2, 4}, {0, 1, 2, 4}} := by +-- simp_rw [powerset_insert, powerset_singleton] +-- simp_rw [image_insert_eq, image_singleton] -theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) : - Finset.powerset {x} = {∅, {x}} := by - ext y - rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton] -end Finset -/- The powerset of a singleton contains only `∅` and the singleton. -/ -theorem powerset_singleton {U : Type _} (x : U) : - 𝒫 ({x} : Set U) = {∅, {x}} := by - ext y - rw [mem_powerset_iff, subset_singleton_iff_eq] - rw [mem_insert_iff, mem_singleton_iff] +-- example : Finset.powerset ({0, 1} : Finset ℕ) = {{0, 1}, ∅, {1}, {0}} := by +-- have h : Finset.powerset ({0, 1} : Finset ℕ) = {∅, {0}, {1}, {0, 1}} +-- rfl +-- rw [h] +-- simp only [] -lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) : - S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by - rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff] +-- example : ({∅, {0}, {1}, {0, 1}} : Finset (Finset ℕ)) = {∅, {1}, {0}, {0, 1}} := by +-- simp only [] + --- lemma powerset_insert {U : Type _} (A : Set U) (x : U) : --- 𝒫 (insert x A) = 𝒫 A ∪ ({B : Set U | B \ {x} ∈ 𝒫 A}) := by --- sorry -theorem subset_insert_iff_of_not_mem {U : Type _ }{s t : Set U} (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t := by - rw [subset_insert_iff, erase_eq_of_not_mem h] - -lemma mem_powerset_insert_iff₂ {U : Type _} (A S : Set U) (x : U) : - S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by - simp_rw [mem_powerset_iff] - constructor - · intro h - by_cases hs : x ∈ S - · sorry - · left - rw [Finset.subset_insert_iff_of_not_mem] - · intro h - rcases h with h | ⟨B, h₁, h₂⟩ - · exact le_trans h (subset_insert x A) - · rw [←h₂] - exact insert_subset_insert h₁ - -lemma powerset_insert {U : Type _} (A : Set U) (x : U) : - 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by - rw [Subset.antisymm_iff] - constructor <;> - intro B hB <;> - simp_rw [mem_powerset_insert_iff₂, mem_union, mem_image] at hB ⊢ <;> - assumption - - -example : powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by - simp_rw [powerset_insert, powerset_singleton, Finset.powerset_insert, Finset.powerset_singleton] - simp only [image_insert_eq, union_insert, image_singleton, union_singleton] - simp only [insert_comm, ←insert_emptyc_eq] - -example [DecidableEq ℕ] : Finset.powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by - repeat' rw [@ Finset.powerset_insert ℕ] - repeat' rw [@Finset.powerset_singleton ℕ] - --simp only [image_insert_eq, union_insert, image_singleton, union_singleton] - - -example : powerset {0, 1, 2, 4} = - {∅, {0}, {1}, {0, 1}, {2}, {1, 2}, {0, 2}, {0, 1, 2}, - {4}, {0, 4}, {1, 4}, {0, 1, 4}, {2, 4}, {1, 2, 4}, {0, 2, 4}, {0, 1, 2, 4}} := by - simp_rw [powerset_insert, powerset_singleton] - simp_rw [image_insert_eq, image_singleton] - - - -example : Finset.powerset ({0, 1} : Finset ℕ) = {{0, 1}, ∅, {1}, {0}} := by - have h : Finset.powerset ({0, 1} : Finset ℕ) = {∅, {0}, {1}, {0, 1}} - rfl - rw [h] - simp only [] - - -example : ({∅, {0}, {1}, {0, 1}} : Finset (Finset ℕ)) = {∅, {1}, {0}, {0, 1}} := by - simp only [] - - - -lemma subset_of_subset_diff {U : Type _} (A B C : Set U) (h : A ⊆ B \ C) : A ⊆ B := - fun _ hx => mem_of_mem_diff (h hx) - -lemma subset_of_subset_diff' {U : Type _} (A B C : Set U) (h : A ⊆ B) : A \ C ⊆ B := - sorry - -lemma mem_powerset' {U : Type _} {A B C : Set U} - (h' : B ∈ 𝒫 C) (h : A ⊆ B) : - A ∈ 𝒫 C := by - rw [mem_powerset_iff] at h' ⊢ - exact le_trans h h' - -example (A B : Set ℕ) : A = B ↔ ∀ x, x ∈ A ↔ x ∈ B := by - exact ext_iff - - - -lemma NO.powerset_insert {U : Type _} (A : Set U) (x : U) : - 𝒫 (insert x A) = 𝒫 A ∪ ({insert x B | B ∈ 𝒫 A}) := by - ext y - rw [mem_powerset_insert_iff] - constructor - · intro h - rw [mem_union, mem_setOf] - by_cases hx : x ∈ y - · right - use y \ {x} - constructor - · assumption - · rw [insert_diff_singleton, insert_eq_of_mem hx] - · left - rw [diff_singleton_eq_self hx] at h - assumption - · intro h - rw [mem_union, mem_setOf] at h - rcases h with h | h - · apply mem_powerset' h - simp - · rcases h with ⟨B, hB⟩ - rw [←hB.2] - apply mem_powerset' hB.1 - simp - --- lemma xxx {U : Type _} (x y : U): --- ({insert x B | B ∈ {∅, }}) = {({x} : Set U), {x, y}} := by +-- lemma subset_of_subset_diff {U : Type _} (A B C : Set U) (h : A ⊆ B \ C) : A ⊆ B := +-- fun _ hx => mem_of_mem_diff (h hx) + +-- lemma subset_of_subset_diff' {U : Type _} (A B C : Set U) (h : A ⊆ B) : A \ C ⊆ B := -- sorry --- lemma hh {U : Type _} (A : Set U) (x : U) : --- A \ {x} ∈ +-- lemma mem_powerset' {U : Type _} {A B C : Set U} +-- (h' : B ∈ 𝒫 C) (h : A ⊆ B) : +-- A ∈ 𝒫 C := by +-- rw [mem_powerset_iff] at h' ⊢ +-- exact le_trans h h' + +-- example (A B : Set ℕ) : A = B ↔ ∀ x, x ∈ A ↔ x ∈ B := by +-- exact ext_iff -lemma diff_singleton_eq_iff {U : Type _} {A B : Set U} {x : U} : - A \ {x} = B ↔ A = B ∨ A = insert x B := by sorry -lemma x1 {U : Type _} (x : U) : insert x (∅ : Set U) = {x} := by sorry ---set_option maxHeartbeats 20000 +-- lemma NO.powerset_insert {U : Type _} (A : Set U) (x : U) : +-- 𝒫 (insert x A) = 𝒫 A ∪ ({insert x B | B ∈ 𝒫 A}) := by +-- ext y +-- rw [mem_powerset_insert_iff] +-- constructor +-- · intro h +-- rw [mem_union, mem_setOf] +-- by_cases hx : x ∈ y +-- · right +-- use y \ {x} +-- constructor +-- · assumption +-- · rw [insert_diff_singleton, insert_eq_of_mem hx] +-- · left +-- rw [diff_singleton_eq_self hx] at h +-- assumption +-- · intro h +-- rw [mem_union, mem_setOf] at h +-- rcases h with h | h +-- · apply mem_powerset' h +-- simp +-- · rcases h with ⟨B, hB⟩ +-- rw [←hB.2] +-- apply mem_powerset' hB.1 +-- simp + +-- -- lemma xxx {U : Type _} (x y : U): +-- -- ({insert x B | B ∈ {∅, }}) = {({x} : Set U), {x, y}} := by +-- -- sorry + +-- -- lemma hh {U : Type _} (A : Set U) (x : U) : +-- -- A \ {x} ∈ + +-- lemma diff_singleton_eq_iff {U : Type _} {A B : Set U} {x : U} : +-- A \ {x} = B ↔ A = B ∨ A = insert x B := by sorry +-- lemma x1 {U : Type _} (x : U) : insert x (∅ : Set U) = {x} := by sorry -example {U : Type _} {x y : U} : ({x, y} : Set U) = {y, x} := by - exact pair_comm x y +-- --set_option maxHeartbeats 20000 -example {U : Type _} {A : Set U} {x y : U} : insert x (insert y A) = insert y (insert x A) := by - exact insert_comm x y A -open Classical +-- example {U : Type _} {x y : U} : ({x, y} : Set U) = {y, x} := by +-- exact pair_comm x y -#check decide +-- example {U : Type _} {A : Set U} {x y : U} : insert x (insert y A) = insert y (insert x A) := by +-- exact insert_comm x y A -example : ({{0, 2}, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}} := by - rw [Subset.antisymm_iff] - constructor <;> - intro A hA <;> - simp_rw [mem_insert_iff, mem_singleton_iff] at * - · rw [pair_comm 2 0, insert_comm 5 3] - tauto - · rw [pair_comm 0 2, insert_comm 3 5] - tauto +-- open Classical -example (A : Set ℕ) : ({{0, 2}, A, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}, A} := by - simp only [insert_comm, ←insert_emptyc_eq] +-- #check decide +-- example : ({{0, 2}, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}} := by +-- rw [Subset.antisymm_iff] +-- constructor <;> +-- intro A hA <;> +-- simp_rw [mem_insert_iff, mem_singleton_iff] at * +-- · rw [pair_comm 2 0, insert_comm 5 3] +-- tauto +-- · rw [pair_comm 0 2, insert_comm 3 5] +-- tauto + +-- example (A : Set ℕ) : ({{0, 2}, A, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}, A} := by +-- simp only [insert_comm, ←insert_emptyc_eq] -example : ({{0, 2}, {3, 5, 6}} : Finset (Finset ℕ)) = {{2, 0}, {5, 3, 6}} := by - simp only +-- example : ({{0, 2}, {3, 5, 6}} : Finset (Finset ℕ)) = {{2, 0}, {5, 3, 6}} := by +-- simp only - -- -- This works but does not scale well - -- ext x - -- simp_rw [powerset_insert, powerset_singleton] - -- simp_rw [mem_union, mem_setOf, mem_insert_iff, mem_singleton_iff] - -- simp_rw [diff_singleton_eq_iff, x1] - -- tauto +-- -- -- This works but does not scale well +-- -- ext x +-- -- simp_rw [powerset_insert, powerset_singleton] +-- -- simp_rw [mem_union, mem_setOf, mem_insert_iff, mem_singleton_iff] +-- -- simp_rw [diff_singleton_eq_iff, x1] +-- -- tauto - -- rw [Subset.antisymm_iff] - -- constructor - -- intro A hA - -- rw [mem_powerset_iff] at hA - -- simp_rw [mem_insert_iff, mem_singleton_iff] at * +-- -- rw [Subset.antisymm_iff] +-- -- constructor +-- -- intro A hA +-- -- rw [mem_powerset_iff] at hA +-- -- simp_rw [mem_insert_iff, mem_singleton_iff] at * -example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by - intro a ha - simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at * - tauto -example : ({0} : Set ℕ) ∪ {1, 2} = {0, 2, 1} := by - rw [Subset.antisymm_iff] - intro A hA - --rw [Set.mem_insert_iff] +-- example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by +-- intro a ha +-- simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at * +-- tauto + +-- example : ({0} : Set ℕ) ∪ {1, 2} = {0, 2, 1} := by +-- rw [Subset.antisymm_iff] +-- intro A hA +-- --rw [Set.mem_insert_iff] --- Trick: --- attribute [default_instance] Set.instSingletonSet +-- -- Trick: +-- -- attribute [default_instance] Set.instSingletonSet diff --git a/server/adam/Adam/Levels/SetTheory/T04_xx.lean b/server/adam/Adam/Levels/SetTheory/T04_xx.lean index 7d0f0ad..106c3f9 100644 --- a/server/adam/Adam/Levels/SetTheory/T04_xx.lean +++ b/server/adam/Adam/Levels/SetTheory/T04_xx.lean @@ -1,96 +1,96 @@ -import Adam.Metadata +-- import Adam.Metadata -import Mathlib -import Duper.Tactic +-- import Duper.Tactic -import Mathlib.Order.Disjoint -set_option tactic.hygienic false +-- import Mathlib.Order.Disjoint -Game "Adam" -World "SetTheory" -Level 4 +-- set_option tactic.hygienic false -Title "Mengen" +-- Game "Adam" +-- World "SetTheory" +-- Level 4 -Introduction -" -`∈ ∉ ⊆ ⊂ ⋃ ⋂` -" +-- Title "Mengen" -open Set +-- Introduction +-- " +-- `∈ ∉ ⊆ ⊂ ⋃ ⋂` +-- " --- open_locale cardinal +-- open Set -variables {X : Type _} (x : X) (A B : Set X) +-- -- open_locale cardinal -#check A.Nonempty -#check Nonempty A -#check insert x A -- {x} ∪ A --- #check disjoint A B -- needs Mathlib.Order.Disjoint -#check A ∆ B -#check Nontrivial A +-- variables {X : Type _} (x : X) (A B : Set X) -#check ({2} : Set ℕ) +-- #check A.Nonempty +-- #check Nonempty A +-- #check insert x A -- {x} ∪ A +-- -- #check disjoint A B -- needs Mathlib.Order.Disjoint +-- #check A ∆ B +-- #check Nontrivial A -example : ({2} : Set ℕ) ⊆ {4, 2, 3} := by - simp only [mem_singleton_iff, mem_insert_iff, or_self, singleton_subset_iff, or_false, or_true] +-- #check ({2} : Set ℕ) -example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by - intro n hn - simp only [mem_insert_iff, mem_singleton_iff] at * - tauto +-- example : ({2} : Set ℕ) ⊆ {4, 2, 3} := by +-- simp only [mem_singleton_iff, mem_insert_iff, or_self, singleton_subset_iff, or_false, or_true] -example : {2, 3, 5} ⊆ (univ : Set ℕ) := by - tauto +-- example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by +-- intro n hn +-- simp only [mem_insert_iff, mem_singleton_iff] at * +-- tauto -example : 3 ∈ ({4, 2, 5, 7, 3} : Set ℕ) := by - tauto +-- example : {2, 3, 5} ⊆ (univ : Set ℕ) := by +-- tauto -example : ({4, 9} : Set ℕ) = Set.insert 4 {9} := by - rfl +-- example : 3 ∈ ({4, 2, 5, 7, 3} : Set ℕ) := by +-- tauto +-- example : ({4, 9} : Set ℕ) = Set.insert 4 {9} := by +-- rfl -#check Finset.card -variable (A : Finset ℕ) +-- #check Finset.card -#check A.card +-- variable (A : Finset ℕ) --- card_union_eq -example (A B : Finset ℕ) (h : Disjoint A B) : (A ∪ B).card = A.card + B.card := by - -- Not a suitable proof for the course. - rw [← Finset.disjUnion_eq_union A B h, Finset.card_disjUnion _ _ _] +-- #check A.card -example : ¬Disjoint {n : ℤ | ∃ k, n = 2 * k} {3, 5, 6, 9, 11} := by - rw [not_disjoint_iff] - use 6 - constructor - rw [mem_setOf_eq] - use 3 - tauto +-- -- card_union_eq +-- example (A B : Finset ℕ) (h : Disjoint A B) : (A ∪ B).card = A.card + B.card := by +-- -- Not a suitable proof for the course. +-- rw [← Finset.disjUnion_eq_union A B h, Finset.card_disjUnion _ _ _] -example : {n : ℕ | Even n ∨ Odd n} = univ := by - rw [setOf_or] +-- example : ¬Disjoint {n : ℤ | ∃ k, n = 2 * k} {3, 5, 6, 9, 11} := by +-- rw [not_disjoint_iff] +-- use 6 +-- constructor +-- rw [mem_setOf_eq] +-- use 3 +-- tauto +-- example : {n : ℕ | Even n ∨ Odd n} = univ := by +-- rw [setOf_or] -#check Set.eq_of_mem_singleton -#check {n : ℤ | ∃ k, n = 2 * k} -#check {n : ℤ // ∃ k, n = 2 * k} -#check ℤ -variables (C : Set ℤ) -#check {n ∈ C | ∃ (k : ℤ), n = 2 * k} -#check {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} -#check {x ∈ A | x = x} -#check {y | y ∈ A} -#check setOf_and -#check setOf_or -#check Disjoint C univ -example : {n ∈ C | ∃ (k : ℤ), n = 2 * k} = {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} := by - rfl +-- #check Set.eq_of_mem_singleton +-- #check {n : ℤ | ∃ k, n = 2 * k} +-- #check {n : ℤ // ∃ k, n = 2 * k} +-- #check ℤ +-- variables (C : Set ℤ) +-- #check {n ∈ C | ∃ (k : ℤ), n = 2 * k} +-- #check {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} +-- #check {x ∈ A | x = x} +-- #check {y | y ∈ A} +-- #check setOf_and +-- #check setOf_or +-- #check Disjoint C univ + +-- example : {n ∈ C | ∃ (k : ℤ), n = 2 * k} = {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} := by +-- rfl diff --git a/server/adam/Adam/Levels/StatementTest.lean b/server/adam/Adam/Levels/StatementTest.lean index db6bc7f..8ea9990 100644 --- a/server/adam/Adam/Levels/StatementTest.lean +++ b/server/adam/Adam/Levels/StatementTest.lean @@ -1,38 +1,38 @@ -import Adam.Metadata -import Mathlib +-- import Adam.Metadata +-- import Mathlib -Game "Adam" -World "TestWorld" -Level 1 +-- Game "Adam" +-- World "TestWorld" +-- Level 1 -Title "Annahmen" +-- Title "Annahmen" -Introduction "yadaa yadaa" +-- Introduction "yadaa yadaa" -class MyClass (n : ℕ) where +-- class MyClass (n : ℕ) where -Statement name -"Beweise dieses Lemma." -(n m : ℕ) : CommSemigroup ℕ where - mul := fun i j => 0 - mul_comm := sorry - mul_assoc := sorry +-- Statement name +-- "Beweise dieses Lemma." +-- (n m : ℕ) : CommSemigroup ℕ where +-- mul := fun i j => 0 +-- mul_comm := sorry +-- mul_assoc := sorry ---@[exercise] -instance instTest (n m : ℕ) : CommSemigroup ℕ where - mul := fun i j => 0 - mul_comm := by - sorry - mul_assoc := by - sorry +-- --@[exercise] +-- instance instTest (n m : ℕ) : CommSemigroup ℕ where +-- mul := fun i j => 0 +-- mul_comm := by +-- sorry +-- mul_assoc := by +-- sorry ---@[exercise] -lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by - rewrite [h₁] - rw [←h₂] - assumption +-- --@[exercise] +-- lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by +-- rewrite [h₁] +-- rw [←h₂] +-- assumption -Conclusion "" +-- Conclusion "" -NewTactic assumption +-- NewTactic assumption diff --git a/server/adam/Adam/Levels/Sum/L02_Sum.lean b/server/adam/Adam/Levels/Sum/L02_Sum.lean index 8c47b5e..6ec0238 100644 --- a/server/adam/Adam/Levels/Sum/L02_Sum.lean +++ b/server/adam/Adam/Levels/Sum/L02_Sum.lean @@ -1,7 +1,8 @@ import Adam.Metadata import Adam.ToBePorted -import Mathlib + +import Adam.Options.MathlibPart set_option tactic.hygienic false open Finset diff --git a/server/adam/Adam/Levels/Sum/L03_ArithSum.lean b/server/adam/Adam/Levels/Sum/L03_ArithSum.lean index ff80c3d..cd7fac1 100644 --- a/server/adam/Adam/Levels/Sum/L03_ArithSum.lean +++ b/server/adam/Adam/Levels/Sum/L03_ArithSum.lean @@ -1,7 +1,6 @@ import Adam.Metadata -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean index 17f594f..93cf12e 100644 --- a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean +++ b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean @@ -1,8 +1,7 @@ import Adam.Metadata import Adam.ToBePorted -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart Game "Adam" World "Sum" diff --git a/server/adam/Adam/Levels/Sum/L05_SumComm.lean b/server/adam/Adam/Levels/Sum/L05_SumComm.lean index bf73cf2..c6d4f2a 100644 --- a/server/adam/Adam/Levels/Sum/L05_SumComm.lean +++ b/server/adam/Adam/Levels/Sum/L05_SumComm.lean @@ -1,8 +1,7 @@ import Adam.Metadata import Adam.ToBePorted -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart import Adam.Options.ArithSum diff --git a/server/adam/Adam/Levels/Sum/L06_Summary.lean b/server/adam/Adam/Levels/Sum/L06_Summary.lean index 3e45e7b..7c68f7b 100644 --- a/server/adam/Adam/Levels/Sum/L06_Summary.lean +++ b/server/adam/Adam/Levels/Sum/L06_Summary.lean @@ -1,10 +1,8 @@ import Adam.Metadata import Adam.ToBePorted -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart -import Adam.ToBePorted import Adam.Options.ArithSum Game "Adam" diff --git a/server/adam/Adam/Levels/Sum/T01_Induction.lean b/server/adam/Adam/Levels/Sum/T01_Induction.lean index 24062ab..ec8dc5f 100644 --- a/server/adam/Adam/Levels/Sum/T01_Induction.lean +++ b/server/adam/Adam/Levels/Sum/T01_Induction.lean @@ -1,38 +1,38 @@ -import Adam.Metadata +-- import Adam.Metadata -import Adam.ToBePorted -import Mathlib.Algebra.BigOperators.Fin +-- import Adam.ToBePorted +-- import Adam.Options.MathlibPart -set_option tactic.hygienic false +-- set_option tactic.hygienic false -open Nat +-- open Nat -Game "Adam" -World "Sum" -Level 2 +-- Game "Adam" +-- World "Sum" +-- Level 2 -Title "endliche Summe" +-- Title "endliche Summe" --- TODO: Tactics `mono` and `omega` are not ported yet. +-- -- TODO: Tactics `mono` and `omega` are not ported yet. -Introduction -" -2^n > n^2 für n ≥ 5 -" +-- Introduction +-- " +-- 2^n > n^2 für n ≥ 5 +-- " -Statement -"2^n > n^2 für n ≥ 5" - (n : ℕ) : (n + 5)^2 < 2 ^ (n + 5) := by -induction' n with n ih -simp -rw [succ_eq_add_one] -simp_rw [add_pow_two] at * -ring_nf at ih ⊢ -sorry +-- Statement +-- "2^n > n^2 für n ≥ 5" +-- (n : ℕ) : (n + 5)^2 < 2 ^ (n + 5) := by +-- induction' n with n ih +-- simp +-- rw [succ_eq_add_one] +-- simp_rw [add_pow_two] at * +-- ring_nf at ih ⊢ +-- sorry -example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n -| 0 | 1 | 2 | 3 | 4 => by - sorry -| n + 5 => by sorry +-- example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n +-- | 0 | 1 | 2 | 3 | 4 => by +-- sorry +-- | n + 5 => by sorry diff --git a/server/adam/Adam/Levels/Sum/T02_Induction.lean b/server/adam/Adam/Levels/Sum/T02_Induction.lean index 09f6400..1ce9f9e 100644 --- a/server/adam/Adam/Levels/Sum/T02_Induction.lean +++ b/server/adam/Adam/Levels/Sum/T02_Induction.lean @@ -1,31 +1,31 @@ -import Adam.Metadata +-- import Adam.Metadata -import Adam.ToBePorted -import Mathlib.Algebra.BigOperators.Fin +-- import Adam.ToBePorted +-- import Adam.Options.MathlibPart -set_option tactic.hygienic false +-- set_option tactic.hygienic false -Game "Adam" -World "Sum" -Level 2 +-- Game "Adam" +-- World "Sum" +-- Level 2 -Title "endliche Summe" +-- Title "endliche Summe" -Introduction -" -n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n -" +-- Introduction +-- " +-- n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n +-- " -Statement -"n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n" - (n : ℤ) : 3 ∣ n^3 + 2*n := by - induction n - induction a - norm_cast - change 3 ∣ (Nat.succ n : ℤ) ^ 3 + 2 * (Nat.succ n : ℤ) - rw [Int.ofNat_succ] - sorry - sorry +-- Statement +-- "n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n" +-- (n : ℤ) : 3 ∣ n^3 + 2*n := by +-- induction n +-- induction a +-- norm_cast +-- change 3 ∣ (Nat.succ n : ℤ) ^ 3 + 2 * (Nat.succ n : ℤ) +-- rw [Int.ofNat_succ] +-- sorry +-- sorry -- example (n : ℕ) : (n - 1) * (n + 1) = (n ^ 2 - 1) := by -- induction' n with n hn diff --git a/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean b/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean index 0c73287..7b4bb9b 100644 --- a/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean +++ b/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean @@ -1,8 +1,7 @@ import Adam.Metadata import Adam.ToBePorted -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Tactic.Ring +import Adam.Options.MathlibPart import Adam.ToBePorted diff --git a/server/adam/Adam/Options/ArithSum.lean b/server/adam/Adam/Options/ArithSum.lean index d92a8ee..6019a33 100644 --- a/server/adam/Adam/Options/ArithSum.lean +++ b/server/adam/Adam/Options/ArithSum.lean @@ -1,5 +1,4 @@ -import Mathlib.Tactic.Ring -import Mathlib.Algebra.BigOperators.Fin +import Adam.Options.MathlibPart open BigOperators diff --git a/server/adam/Adam/Options/MathlibPart.lean b/server/adam/Adam/Options/MathlibPart.lean new file mode 100644 index 0000000..55bf1da --- /dev/null +++ b/server/adam/Adam/Options/MathlibPart.lean @@ -0,0 +1,15 @@ +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring +import Mathlib.Tactic.Linarith +import Mathlib.Data.Nat.Parity +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.LinearAlgebra.LinearIndependent +import Mathlib.Data.Real.Basic -- definiert `ℝ` +import Mathlib.LinearAlgebra.Basis +import Mathlib.Data.Real.Basic -- definiert `ℝ` +import Mathlib.Algebra.Module.Pi -- definiert `Module ℚ (fin 2 → ℚ)` +import Mathlib.Data.Fin.VecNotation +import Mathlib.Tactic.FinCases diff --git a/server/adam/Adam/Playground.lean b/server/adam/Adam/Playground.lean index 897d304..997447d 100644 --- a/server/adam/Adam/Playground.lean +++ b/server/adam/Adam/Playground.lean @@ -1,96 +1,97 @@ -import Mathlib - -open Function Set - -example {A B : Type _ } (f : A → B) : f.Injective ↔ ∃ g : B → A, g ∘ f = id := by - constructor - · intro h - -- hard. - sorry - · intro h - rcases h with ⟨g, h⟩ - unfold Injective - intro a b hab - rw [←id_eq a, ←id_eq b] - rw [← h] - rw [comp_apply] - rw [hab] - simp - - -lemma singleton_mem_powerset - {U : Type _} {M : Set U} {x : U} (h : x ∈ M) : - {x} ∈ 𝒫 M := by - rw [mem_powerset_iff, singleton_subset_iff] - assumption - -example - {U : Type _} (M : Set U) : - {A : Set U // A ∈ 𝒫 M} = {A ∈ 𝒫 M | True} := by - simp_rw [coe_setOf, and_true] - -example - {U : Type _} (M : Set U) : - {A : Set U // A ∈ 𝒫 M} = 𝒫 M := by - rfl - -example - {U : Type _} (M : Set U) : - {x : U // x ∈ M} = M := by - rfl - -example - {U : Type _} (M : Set U) : - ∃ (f : M → 𝒫 M), Injective f := by - use fun x ↦ ⟨ _, singleton_mem_powerset x.prop ⟩ - intro a b hab - simp at hab - rw [Subtype.val_inj] at hab - assumption - -instance {U : Type _} {M : Set U} : Membership ↑M ↑(𝒫 M) := -{ mem := fun x A ↦ x.1 ∈ A.1 } - -instance {U : Type _} {M : Set U} : Membership U (Set ↑M) := -{ mem := fun x A ↦ _ } - - -example - {U : Type _} {M : Set U} (h_empty : M.Nonempty) - (f : {x : U // x ∈ M} → {A : Set U // A ∈ 𝒫 M}): - ¬ Surjective f := by - unfold Surjective - push_neg - --by_contra h_sur - let B : Set M := {x : M | x ∉ (f x)} - use ⟨B, sorry⟩ - intro ⟨a, ha⟩ - sorry - -- Too hard? - -#check singleton_mem_powerset -#check Subtype.val_inj - - - --- These are fun exercises for prime. -example (x : ℕ) : 0 < x ↔ 1 ≤ x := by - rfl - -lemma le_cancel_left (n x : ℕ) (h : x ≠ 0): n ≤ n * x := by - induction n - simp - simp - rw [← zero_lt_iff] at h - assumption - - -example (n m : ℕ) (g : m ≠ 0) (h : n ∣ m) : n ≤ m := by - rcases h with ⟨x, hx⟩ - rw [hx] - apply le_cancel_left - by_contra k - rw [k] at hx - simp at hx - rw [hx] at g - contradiction +-- import Mathlib.Data.Set.Basic +-- import Mathlib + +-- open Function Set + +-- example {A B : Type _ } (f : A → B) : f.Injective ↔ ∃ g : B → A, g ∘ f = id := by +-- constructor +-- · intro h +-- -- hard. +-- sorry +-- · intro h +-- rcases h with ⟨g, h⟩ +-- unfold Injective +-- intro a b hab +-- rw [←id_eq a, ←id_eq b] +-- rw [← h] +-- rw [comp_apply] +-- rw [hab] +-- simp + + +-- lemma singleton_mem_powerset +-- {U : Type _} {M : Set U} {x : U} (h : x ∈ M) : +-- {x} ∈ 𝒫 M := by +-- rw [mem_powerset_iff, singleton_subset_iff] +-- assumption + +-- example +-- {U : Type _} (M : Set U) : +-- {A : Set U // A ∈ 𝒫 M} = {A ∈ 𝒫 M | True} := by +-- simp_rw [coe_setOf, and_true] + +-- example +-- {U : Type _} (M : Set U) : +-- {A : Set U // A ∈ 𝒫 M} = 𝒫 M := by +-- rfl + +-- example +-- {U : Type _} (M : Set U) : +-- {x : U // x ∈ M} = M := by +-- rfl + +-- example +-- {U : Type _} (M : Set U) : +-- ∃ (f : M → 𝒫 M), Injective f := by +-- use fun x ↦ ⟨ _, singleton_mem_powerset x.prop ⟩ +-- intro a b hab +-- simp at hab +-- rw [Subtype.val_inj] at hab +-- assumption + +-- instance {U : Type _} {M : Set U} : Membership ↑M ↑(𝒫 M) := +-- { mem := fun x A ↦ x.1 ∈ A.1 } + +-- instance {U : Type _} {M : Set U} : Membership U (Set ↑M) := +-- { mem := fun x A ↦ _ } + + +-- example +-- {U : Type _} {M : Set U} (h_empty : M.Nonempty) +-- (f : {x : U // x ∈ M} → {A : Set U // A ∈ 𝒫 M}): +-- ¬ Surjective f := by +-- unfold Surjective +-- push_neg +-- --by_contra h_sur +-- let B : Set M := {x : M | x ∉ (f x)} +-- use ⟨B, sorry⟩ +-- intro ⟨a, ha⟩ +-- sorry +-- -- Too hard? + +-- #check singleton_mem_powerset +-- #check Subtype.val_inj + + + +-- -- These are fun exercises for prime. +-- example (x : ℕ) : 0 < x ↔ 1 ≤ x := by +-- rfl + +-- lemma le_cancel_left (n x : ℕ) (h : x ≠ 0): n ≤ n * x := by +-- induction n +-- simp +-- simp +-- rw [← zero_lt_iff] at h +-- assumption + + +-- example (n m : ℕ) (g : m ≠ 0) (h : n ∣ m) : n ≤ m := by +-- rcases h with ⟨x, hx⟩ +-- rw [hx] +-- apply le_cancel_left +-- by_contra k +-- rw [k] at hx +-- simp at hx +-- rw [hx] at g +-- contradiction diff --git a/server/adam/Adam/StructInstWithHolesTest.lean b/server/adam/Adam/StructInstWithHolesTest.lean index 12fdc8d..743e991 100644 --- a/server/adam/Adam/StructInstWithHolesTest.lean +++ b/server/adam/Adam/StructInstWithHolesTest.lean @@ -1,117 +1,117 @@ -import Adam.StructInstWithHoles -import Mathlib - - -example : Module ℚ ℝ := by - refine { ?..! } - exact fun a r => a * r - intro b - sorry - sorry - sorry - sorry - sorry - sorry - sorry - -structure Foo where - x : Nat := 0 - y : Nat - -structure Bar extends Foo where - z : Nat := x - -example := by refine { ?.. : Foo }; case y => exact 0 -example := by refine { ?.. : Bar }; case y => exact 0 -example := by refine { ?..a : Bar }; case a.y => exact 0 -example := by refine { ?..! : Bar }; case x | y | z => exact 0; -example := by refine { ?..!a : Bar }; case a.x | a.y | a.z => exact 0; --- example := by refine' { ... : Bar }; exact 0 -example := by refine' { .. : Bar }; exact 0; exact 0; exact 0 --- example := by refine' { ..! : Bar }; exact 0; exact 0; exact 0 - -structure rflFoo where - x : Nat - y : Nat - xy : x = y := by rfl - -example := by refine { ?.. : rflFoo }; (case x | y => exact 0); case xy => rfl -example := by refine { ?..! : rflFoo }; (case x | y => exact 0); case xy => rfl - -structure autoFoo where - x : Nat := 0 - y : Nat := 0 - xy : x = y := by rfl - -example := { ?.. : autoFoo } -example := by refine { ?..! : autoFoo }; (case x | y => exact 0); case xy => rfl - -def f : Foo → Nat := fun _ => 0 -def ff : Foo → Foo → Unit := fun _ _ => () -def ffb : Foo → Bar → Unit := fun _ _ => () -def ffa : Foo → autoFoo → Unit := fun _ _ => () - -example := by refine { x := f { ?.. }, ?.. : Foo }; case y | y_1 => exact 0 -example := by refine { x := f { ?..x }, ?.. : Foo }; case x.y | y => exact 0 -example := by refine { x := f { ?.. }, ?..x : Foo }; case y | x.y => exact 0 -example := by refine { x := f { ?..x }, ?..x : Foo }; case x.y | x.y_1 => exact 0 - -example := by refine ff { ?.. } { ?.. }; case y | y_1 => exact 0 -example := by refine ff { ?..! } { ?.. }; case x | y | y_1 => exact 0 -example := by refine ffb { ?..! } { ?..! }; case x | y | x_1 | y_1 | z_1 => exact 0 -example := by refine ffa { ?..! } { ?..! }; (case x | y | x_1 | y_1 => exact 0); rfl - -structure Foo' where - x : Nat - -structure dFoo' where - x : Nat := 0 - -def ff' : Foo → Foo' → Unit := fun _ _ => () -def fdf' : Foo → dFoo' → Unit := fun _ _ => () - -example := by refine ff' { ?.. } { ?.. }; case y | x_1 => exact 0 -example := by refine fdf' { ?.. } { ?.. }; case y => exact 0 - -structure Fooα (α : Type) where - x : α - -example := by refine { ?.. : Fooα Nat}; case x => exact 0 - -structure Fooαi where - {α : Type} - x : α - -example := by refine { ?.. : Fooαi }; (case α => exact Nat); case x => exact 0 - -/- haveFieldProj tests (subject to be moved)-/ -section haveFieldProj - -structure Foo'' where - x : Bool - y : Nat - -def foo'': Foo'' := { x := true, y := 0 } - -example := by - refine { ?.. : Foo''}; - haveFieldProj; - case x => exact x.proj foo''; - case y => exact 0 -example := by - refine { ?.. : Foo''}; - haveFieldProj as a; - case x => exact a foo''; - case y => exact 0 -example := by - refine { ?.. : Foo''}; - haveFieldProj y; - case x => exact 0 == y.proj foo''; - case y => exact 0 -example := by - refine { ?.. : Foo''}; - haveFieldProj y as a; - case x => exact 0 == a foo''; - case y => exact 0 - -end haveFieldProj +-- import Adam.StructInstWithHoles +-- import Mathlib + + +-- example : Module ℚ ℝ := by +-- refine { ?..! } +-- exact fun a r => a * r +-- intro b +-- sorry +-- sorry +-- sorry +-- sorry +-- sorry +-- sorry +-- sorry + +-- structure Foo where +-- x : Nat := 0 +-- y : Nat + +-- structure Bar extends Foo where +-- z : Nat := x + +-- example := by refine { ?.. : Foo }; case y => exact 0 +-- example := by refine { ?.. : Bar }; case y => exact 0 +-- example := by refine { ?..a : Bar }; case a.y => exact 0 +-- example := by refine { ?..! : Bar }; case x | y | z => exact 0; +-- example := by refine { ?..!a : Bar }; case a.x | a.y | a.z => exact 0; +-- -- example := by refine' { ... : Bar }; exact 0 +-- example := by refine' { .. : Bar }; exact 0; exact 0; exact 0 +-- -- example := by refine' { ..! : Bar }; exact 0; exact 0; exact 0 + +-- structure rflFoo where +-- x : Nat +-- y : Nat +-- xy : x = y := by rfl + +-- example := by refine { ?.. : rflFoo }; (case x | y => exact 0); case xy => rfl +-- example := by refine { ?..! : rflFoo }; (case x | y => exact 0); case xy => rfl + +-- structure autoFoo where +-- x : Nat := 0 +-- y : Nat := 0 +-- xy : x = y := by rfl + +-- example := { ?.. : autoFoo } +-- example := by refine { ?..! : autoFoo }; (case x | y => exact 0); case xy => rfl + +-- def f : Foo → Nat := fun _ => 0 +-- def ff : Foo → Foo → Unit := fun _ _ => () +-- def ffb : Foo → Bar → Unit := fun _ _ => () +-- def ffa : Foo → autoFoo → Unit := fun _ _ => () + +-- example := by refine { x := f { ?.. }, ?.. : Foo }; case y | y_1 => exact 0 +-- example := by refine { x := f { ?..x }, ?.. : Foo }; case x.y | y => exact 0 +-- example := by refine { x := f { ?.. }, ?..x : Foo }; case y | x.y => exact 0 +-- example := by refine { x := f { ?..x }, ?..x : Foo }; case x.y | x.y_1 => exact 0 + +-- example := by refine ff { ?.. } { ?.. }; case y | y_1 => exact 0 +-- example := by refine ff { ?..! } { ?.. }; case x | y | y_1 => exact 0 +-- example := by refine ffb { ?..! } { ?..! }; case x | y | x_1 | y_1 | z_1 => exact 0 +-- example := by refine ffa { ?..! } { ?..! }; (case x | y | x_1 | y_1 => exact 0); rfl + +-- structure Foo' where +-- x : Nat + +-- structure dFoo' where +-- x : Nat := 0 + +-- def ff' : Foo → Foo' → Unit := fun _ _ => () +-- def fdf' : Foo → dFoo' → Unit := fun _ _ => () + +-- example := by refine ff' { ?.. } { ?.. }; case y | x_1 => exact 0 +-- example := by refine fdf' { ?.. } { ?.. }; case y => exact 0 + +-- structure Fooα (α : Type) where +-- x : α + +-- example := by refine { ?.. : Fooα Nat}; case x => exact 0 + +-- structure Fooαi where +-- {α : Type} +-- x : α + +-- example := by refine { ?.. : Fooαi }; (case α => exact Nat); case x => exact 0 + +-- /- haveFieldProj tests (subject to be moved)-/ +-- section haveFieldProj + +-- structure Foo'' where +-- x : Bool +-- y : Nat + +-- def foo'': Foo'' := { x := true, y := 0 } + +-- example := by +-- refine { ?.. : Foo''}; +-- haveFieldProj; +-- case x => exact x.proj foo''; +-- case y => exact 0 +-- example := by +-- refine { ?.. : Foo''}; +-- haveFieldProj as a; +-- case x => exact a foo''; +-- case y => exact 0 +-- example := by +-- refine { ?.. : Foo''}; +-- haveFieldProj y; +-- case x => exact 0 == y.proj foo''; +-- case y => exact 0 +-- example := by +-- refine { ?.. : Foo''}; +-- haveFieldProj y as a; +-- case x => exact 0 == a foo''; +-- case y => exact 0 + +-- end haveFieldProj diff --git a/server/adam/Adam/ToBePorted.lean b/server/adam/Adam/ToBePorted.lean index 7c66039..4fa6321 100644 --- a/server/adam/Adam/ToBePorted.lean +++ b/server/adam/Adam/ToBePorted.lean @@ -1,4 +1,4 @@ -import Mathlib +import Adam.Options.MathlibPart open BigOperators