Division working in each level,need simpler proofs

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 "∣"

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 "∣"

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 "∣"

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 "∣"

Game/Levels/Division/Level_6.lean

@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 6

Game/Levels/Division/Level_7.lean

@@ -1,4 +1,5 @@
 import Game.Levels.AdvMultiplication
+import Game.MyNat.Division
 
 World "Division"
 Level 7