diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean
index 8f5c650..b0dd582 100644
--- a/Bookshelf/Apostol/Chapter_1_11.lean
+++ b/Bookshelf/Apostol/Chapter_1_11.lean
@@ -118,7 +118,7 @@ Derive the result analytically as follows: By changing the index of summation,
 note that `Σ_{n=1}^{b-1} ⌊na / b⌋ = Σ_{n=1}^{b-1} ⌊a(b - n) / b⌋`. Now apply
 Exercises 4(a) and (b) to the bracket on the right.
 -/
-theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.coprime a b)
+theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.Coprime a b)
   : ∑ n in (Finset.range b).filter (· > 0), ⌊n * ((a : ℕ) : ℝ) / b⌋ =
       ((a - 1) * (b - 1)) / 2 := by
   sorry
diff --git a/Bookshelf/Enderton/Logic/Chapter_1.lean b/Bookshelf/Enderton/Logic/Chapter_1.lean
index 15210fd..561b3de 100644
--- a/Bookshelf/Enderton/Logic/Chapter_1.lean
+++ b/Bookshelf/Enderton/Logic/Chapter_1.lean
@@ -475,7 +475,7 @@ theorem exercise_1_2_2b_iii {k : ℕ} (h : Odd k)
       have ⟨r, hr⟩ := h
       refine ⟨r, hr, ?_⟩
       by_contra nr
-      have : r = 0 := Nat.eq_zero_of_nonpos r nr
+      have : r = 0 := Nat.eq_zero_of_not_pos nr
       rw [this] at hr
       simp only [mul_zero, zero_add] at hr
       exact absurd hr hk
diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean
index 945345a..b70306e 100644
--- a/Bookshelf/Enderton/Set/Chapter_2.lean
+++ b/Bookshelf/Enderton/Set/Chapter_2.lean
@@ -171,8 +171,7 @@ theorem emptyset_identity_ii (A : Set α)
   : A ∩ ∅ = ∅ := calc A ∩ ∅
   _ = { x | x ∈ A ∧ x ∈ ∅ } := rfl
   _ = { x | x ∈ A ∧ False } := rfl
-  _ = { x | False } := by simp
-  _ = ∅ := rfl
+  _ = ∅ := by simp
 
 #check Set.inter_empty
 
@@ -181,8 +180,7 @@ theorem emptyset_identity_iii (A C : Set α)
   _ = { x | x ∈ A ∧ x ∈ C \ A } := rfl
   _ = { x | x ∈ A ∧ (x ∈ C ∧ x ∉ A) } := rfl
   _ = { x | x ∈ C ∧ False } := by simp
-  _ = { x | False } := by simp
-  _ = ∅ := rfl
+  _ = ∅ := by simp
 
 #check Set.inter_diff_self
 
@@ -636,7 +634,7 @@ lemma left_diff_eq_singleton_one : (A \ B) \ C = {1} := by
     have ⟨⟨ha, hb⟩, hc⟩ := hx
     rw [not_or_de_morgan] at hb hc
     apply Or.elim ha
-    · simp 
+    · simp
     · intro hy
       apply Or.elim hy
       · intro hz
@@ -792,11 +790,11 @@ theorem exercise_2_17_ii {A B : Set α} (h : A \ B = ∅)
 
 theorem exercise_2_17_iii {A B : Set α} (h : A ∪ B = B)
   : A ∩ B = A := by
-  suffices A ⊆ B from Set.inter_eq_left_iff_subset.mpr this
-  exact Set.union_eq_right_iff_subset.mp h
+  suffices A ⊆ B from Set.inter_eq_left.mpr this
+  exact Set.union_eq_right.mp h
 
 theorem exercise_2_17_iv {A B : Set α} (h : A ∩ B = A)
-  : A ⊆ B := Set.inter_eq_left_iff_subset.mp h
+  : A ⊆ B := Set.inter_eq_left.mp h
 
 /-- #### Exercise 2.19
 
@@ -954,7 +952,7 @@ theorem exercise_2_24b {𝓐 : Set (Set α)}
 /-- #### Exercise 2.25
 
 Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under
-what conditions does equality hold? 
+what conditions does equality hold?
 -/
 theorem exercise_2_25 {A : Set α} (𝓑 : Set (Set α))
   : (A ∪ (⋃₀ 𝓑) = ⋃₀ { A ∪ X | X ∈ 𝓑 }) ↔ (A = ∅ ∨ Set.Nonempty 𝓑) := by
@@ -995,4 +993,4 @@ theorem exercise_2_25 {A : Set α} (𝓑 : Set (Set α))
         _ = { x | ∃ t, t ∈ { y | ∃ X, X ∈ 𝓑 ∧ A ∪ X = y } ∧ x ∈ t } := by simp
         _ = ⋃₀ { A ∪ X | X ∈ 𝓑 } := rfl
 
-end Enderton.Set.Chapter_2
\ No newline at end of file
+end Enderton.Set.Chapter_2
diff --git a/Common/Logic/Basic.lean b/Common/Logic/Basic.lean
index a9bf1e5..ba0c170 100644
--- a/Common/Logic/Basic.lean
+++ b/Common/Logic/Basic.lean
@@ -1,4 +1,5 @@
 import Mathlib.Logic.Basic
+import Mathlib.Data.Set.Basic
 import Mathlib.Tactic.Tauto
 
 /-! # Common.Logic.Basic
@@ -39,4 +40,4 @@ theorem forall_mem_comm {X : Set α} {Y : Set β} (p : α → β → Prop)
   · intro h v hv u hu
     exact h u hu v hv
   · intro h u hu v hv
-    exact h v hv u hu
\ No newline at end of file
+    exact h v hv u hu
diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean
index da74efb..f3f1910 100644
--- a/DocGen4/Process/Analyze.lean
+++ b/DocGen4/Process/Analyze.lean
@@ -84,10 +84,10 @@ def shouldRender : ModuleMember → Bool
 end ModuleMember
 
 inductive AnalyzeTask where
-| loadAll (load : List Name) : AnalyzeTask
-| loadAllLimitAnalysis (analyze : List Name) : AnalyzeTask
+| loadAll (load : Array Name) : AnalyzeTask
+| loadAllLimitAnalysis (analyze : Array Name) : AnalyzeTask
 
-def AnalyzeTask.getLoad : AnalyzeTask → List Name
+def AnalyzeTask.getLoad : AnalyzeTask → Array Name
 | loadAll load => load
 | loadAllLimitAnalysis load => load