From 1ea9de78dd0529b8efd5f025c068d2a0c2831448 Mon Sep 17 00:00:00 2001
From: Archie <94995351+archiebrowne@users.noreply.github.com>
Date: Fri, 20 Oct 2023 09:28:08 +0000
Subject: [PATCH] Division working in each level,need simpler proofs

---
 Game/Levels/Division/Level_2.lean |  2 ++
 Game/Levels/Division/Level_3.lean | 15 +++++++++------
 Game/Levels/Division/Level_4.lean |  8 ++++++--
 Game/Levels/Division/Level_5.lean |  5 ++---
 Game/Levels/Division/Level_6.lean |  1 +
 Game/Levels/Division/Level_7.lean |  1 +
 6 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/Game/Levels/Division/Level_2.lean b/Game/Levels/Division/Level_2.lean
index 4ef4524..882f119 100644
--- a/Game/Levels/Division/Level_2.lean
+++ b/Game/Levels/Division/Level_2.lean
@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 2
@@ -22,6 +23,7 @@ Statement
     (n : ℕ) : n ∣ n := by
   Hint "This is true because `n = n * 1`"
   use 1
+  rw [mul_one]
   rfl
 
 LemmaTab "∣"
diff --git a/Game/Levels/Division/Level_3.lean b/Game/Levels/Division/Level_3.lean
index b2723ae..9ce7260 100644
--- a/Game/Levels/Division/Level_3.lean
+++ b/Game/Levels/Division/Level_3.lean
@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 3
@@ -21,12 +22,14 @@ Statement
     (a b : ℕ) (h1 : a ∣ b) (h2 : b ∣ a): a = b := by
   Hint "You will need to expand what `h1` and `h2` atually mean. You may find `rcases` helpful"
   rcases h1 with ⟨c, hc⟩
-  rcases h2 with ⟨d , rfl⟩
+  rcases h2 with ⟨d, hd⟩
   -- need to cancel b's:
-  have : 1 = c * d
-  -- need the fact that if 1 = cd, c = d = 1
-  have : 1 = c
-  rw [this] at hd -- hc : a = b
-  exact hd
+  have hcd : b = b * d * c := by sorry
+  have h1dc : 1 = d * c := by sorry
+  -- need the fact that if 1 = dc, c = d = 1
+  have h1c : 1 = c := by sorry
+  rw [← h1c] at hc -- hc : a = b
+  rw [mul_one] at hc
+  exact Eq.symm hc
 
 LemmaTab "∣"
diff --git a/Game/Levels/Division/Level_4.lean b/Game/Levels/Division/Level_4.lean
index 27942b0..b2453a0 100644
--- a/Game/Levels/Division/Level_4.lean
+++ b/Game/Levels/Division/Level_4.lean
@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 4
@@ -23,12 +24,15 @@ Statement
   Hint "Here, like the last level, you may find `rcases` helpful."
   rcases hbc with ⟨m, hm⟩
   rcases hab with ⟨n, rfl⟩
-
   -- b = na, c = mb
   -- c = mna
   Hint "Now, since we are looking show `a ∣ c`, which is an existience hypothesis, a `use` tactic
   would be a good choice."
   use (m * n)
-  assumption
+  Hint "Now the goal is clear, its just a case of finding the correct rewrites."
+  rw [hm]
+  rw [mul_assoc]
+  rw [mul_comm n m]
+  rfl
 
 LemmaTab "∣"
diff --git a/Game/Levels/Division/Level_5.lean b/Game/Levels/Division/Level_5.lean
index f081cbf..f287afd 100644
--- a/Game/Levels/Division/Level_5.lean
+++ b/Game/Levels/Division/Level_5.lean
@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 5
@@ -27,9 +28,7 @@ Statement
   Hint "The goal is pretty trivial now, you just need to figure out the correct sequence of
   rewrites to finish the job."
   rw [hk]
-  rw [mul_assoc k b d]
-  rw [mul_comm b d]
-  rw [mul_assoc k d b]
+  rw [mul_assoc]
   rfl
 
 LemmaTab "∣"
diff --git a/Game/Levels/Division/Level_6.lean b/Game/Levels/Division/Level_6.lean
index f02ed48..a50dfa4 100644
--- a/Game/Levels/Division/Level_6.lean
+++ b/Game/Levels/Division/Level_6.lean
@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 6
diff --git a/Game/Levels/Division/Level_7.lean b/Game/Levels/Division/Level_7.lean
index cfceb1e..2467234 100644
--- a/Game/Levels/Division/Level_7.lean
+++ b/Game/Levels/Division/Level_7.lean
@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 7