morrison-daniel
diff --git a/‎my_project/Uniqueness.lean ‎Coverings/Uniqueness.lean b/‎my_project/Uniqueness.lean ‎Coverings/Uniqueness.lean
diff --git a/‎my_project/daniel.lean ‎Coverings/daniel.lean
+1-1 b/‎my_project/daniel.lean ‎Coverings/daniel.lean
+1-1
diff --git a/‎my_project/existance.lean ‎Coverings/existance.lean b/‎my_project/existance.lean ‎Coverings/existance.lean
diff --git a/‎my_project/lean3.lean ‎Coverings/lean3.lean b/‎my_project/lean3.lean ‎Coverings/lean3.lean
diff --git a/‎my_project/notes.lean ‎Coverings/notes.lean b/‎my_project/notes.lean ‎Coverings/notes.lean
diff --git a/‎my_project/notes.txt ‎Coverings/notes.txt b/‎my_project/notes.txt ‎Coverings/notes.txt
diff --git a/‎my_project/probs.lean ‎Coverings/probs.lean b/‎my_project/probs.lean ‎Coverings/probs.lean
diff --git a/‎my_project/tony.lean ‎Coverings/tony.lean b/‎my_project/tony.lean ‎Coverings/tony.lean
diff --git a/‎my_project/universal.lean ‎Coverings/universal.lean b/‎my_project/universal.lean ‎Coverings/universal.lean
diff --git a/‎lakefile.lean
+2-2 b/‎lakefile.lean
+2-2
@@ -3,7 +3,7 @@ import Mathlib.Topology.ContinuousOn
 import Mathlib.Topology.Covering
 import Mathlib.Topology.LocalHomeomorph
 import Mathlib.Topology.UnitInterval
-import my_project.tony
+import Coverings.tony
 open Topology Filter unitInterval Bundle
 
 /-
 
@@ -1,14 +1,14 @@
 import Lake
 open Lake DSL
 
-package «my_project» {
+package «coverings» {
   -- add any package configuration options here
 }
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
 @[default_target]
-lean_lib «my_project» {
+lean_lib «Coverings» {
   -- add any library configuration options here
 }
Original file line number	Diff line number	Diff line change
`@@ -1,14 +1,14 @@`
`1`	`1`	`import Lake`
`2`	`2`	`open Lake DSL`
`3`	`3`
`4`		`-package «my_project» {`
	`4`	`+package «coverings» {`
`5`	`5`	`-- add any package configuration options here`
`6`	`6`	`}`
`7`	`7`
`8`	`8`	`require mathlib from git`
`9`	`9`	`"https://github.com/leanprover-community/mathlib4.git"`
`10`	`10`
`11`	`11`	`@[default_target]`
`12`		`-lean_lib «my_project» {`
	`12`	`+lean_lib «Coverings» {`
`13`	`13`	`-- add any library configuration options here`
`14`	`14`	`}`