poistettu mathlib

alma-n · Oct 5, 2024 · 25116a7 · 25116a7
1 parent e41f339
commit 25116a7
Show file tree

Hide file tree

Showing 5 changed files with 29 additions and 53 deletions.
diff --git a/Game/Levels/Disjunktio/L01.lean b/Game/Levels/Disjunktio/L01.lean
@@ -1,5 +1,4 @@
 import Game.Metadata
-import Mathlib
 
 World "Disjunktio"
 Level 2
@@ -9,9 +8,9 @@ Title "Disjunktio 1"
 Statement : A ∨ A ↔ A := by
   constructor
   intro h
-  cases' h with a a
-  exact a
-  exact a
+  cases h
+  exact h_1
+  exact h_1
   intro a
   left
   exact a

diff --git a/Game/Levels/Disjunktio/L02.lean b/Game/Levels/Disjunktio/L02.lean
@@ -1,5 +1,4 @@
 import Game.Metadata
-import Mathlib
 
 World "Disjunktio"
 Level 3
@@ -9,14 +8,14 @@ Title "Disjunktio 2"
 Statement : A ∨ B ↔ B ∨ A := by
   constructor
   intro h
-  cases' h with a b
+  cases h
   right
-  exact a
+  exact h_1
   left
-  exact b
+  exact h_1
   intro h
-  cases' h with b a
+  cases h
   right
-  exact b
+  exact h_1
   left
-  exact a
+  exact h_1
diff --git a/Game/Levels/Disjunktio/L03.lean b/Game/Levels/Disjunktio/L03.lean
@@ -1,5 +1,4 @@
 import Game.Metadata
-import Mathlib
 
 World "Disjunktio"
 Level 4
@@ -9,24 +8,24 @@ Title "Disjunktio 3"
 Statement : (A ∨ B) ∨ C ↔ A ∨ (B ∨ C) := by
   constructor
   intro h
-  cases' h with ab c
-  cases' ab with a b
+  cases h
+  cases h_1
   left
-  exact a
+  exact h
   right
   left
-  exact b
+  exact h
   right
   right
-  exact c
+  exact h_1
   intro h
-  cases' h with a bc
+  cases h
   left
   left
-  exact a
-  cases' bc with b c
+  exact h_1
+  cases h_1
   left
   right
-  exact b
+  exact h
   right
-  exact c
+  exact h
diff --git a/Game/Levels/DisjunktioJaKonjunktio/L01.lean b/Game/Levels/DisjunktioJaKonjunktio/L01.lean
@@ -1,5 +1,5 @@
 import Game.Metadata
-import Mathlib
+
 
 World "DisjunktioJaKonjunktio"
 Level 2
@@ -9,19 +9,19 @@ Title "Disjunktio ∧ konjunktio"
 Statement : A ∧ (B ∨ C) ↔ (A ∧ B) ∨ (A ∧ C) := by
   constructor
   intro h
-  cases' h with a bc
-  cases' bc with b c
+  cases h
+  cases right
   left
-  exact And.intro a b
+  exact And.intro left h
   right
-  exact And.intro a c
+  exact And.intro left h
   intro h
-  cases' h with ab ac
+  cases h
   constructor
-  exact ab.1
+  exact h_1.1
   left
-  exact ab.2
+  exact h_1.2
   constructor
-  exact ac.1
+  exact h_1.1
   right
-  exact ac.2
+  exact h_1.2
diff --git a/Game/Levels/Kertolasku/L00.sync-conflict-20241004-142651-WVUKI75.lean b/Game/Levels/Kertolasku/L00.sync-conflict-20241004-142651-WVUKI75.lean