diff --git a/Compfiles/Imo1965P1.lean b/Compfiles/Imo1965P1.lean
index caa2ced..7d3c44c 100644
--- a/Compfiles/Imo1965P1.lean
+++ b/Compfiles/Imo1965P1.lean
@@ -41,8 +41,9 @@ problem imo1965_p1 :
     simp [←pow_two, h0]
   simp only [Set.mem_Icc]
   simp_rw [this, and_true]
-  symm; ext x; constructor; dsimp
-  . rw [the_answer]; rintro ⟨h1, h2⟩
+  symm; ext x; constructor
+  · dsimp
+    rw [the_answer]; rintro ⟨h1, h2⟩
     constructor
     . constructor <;> linarith
     have : x ∈ Ico (π/4) (π / 2) ∪ Icc (π/2) (3*π/2) ∪ Ioc (3*π/2) (7*π/4) := by
@@ -57,7 +58,8 @@ problem imo1965_p1 :
       have cosx2_nonneg : 0 ≤ 2 * cos x := by linarith
       rw [←abs_of_nonneg cosx2_nonneg, ←sq_le_sq, h0, abs_of_nonpos cos2x_nonpos, cos_two_mul]
       linarith
-    . trans 0; swap; simp
+    . trans 0; swap;
+      · simp
       suffices cos x ≤ 0 by linarith
       apply cos_nonpos_of_pi_div_two_le_of_le h3
       linarith
@@ -90,7 +92,8 @@ problem imo1965_p1 :
     rw [cos_pi_div_four, div_pow] at this; norm_num at this
     linarith
   rw [sq_lt_sq, abs_of_nonneg cosx_nonneg, abs_of_nonneg]
-  swap; simp [cos_pi_div_four]; positivity
+  swap
+  · simp [cos_pi_div_four]; positivity
   rcases h4 with h5 | h5
   . apply cos_lt_cos_of_nonneg_of_le_pi_div_two h1 (by linarith) h5
   rw [←cos_neg x, ←cos_add_two_pi (-x)]
diff --git a/Compfiles/Imo1970P4.lean b/Compfiles/Imo1970P4.lean
index 2049f39..9d97d47 100644
--- a/Compfiles/Imo1970P4.lean
+++ b/Compfiles/Imo1970P4.lean
@@ -174,30 +174,28 @@ lemma odd_props (n : ℕ) (odd_s : Finset ℕ) (s_odd_eq : odd_s = (Finset.Icc n
     ext x
     simp_all only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_filter, Finset.mem_Icc]
     apply Iff.intro
-    intro H
-    constructor
-    · omega
-    · cases H
-      case inl h3 =>
-        simp_all only
-      case inr h4 =>
-        cases h4
-        case inl h5 =>
-          simp_all only
-          dsimp[Odd]
-          dsimp[Odd] at h
-          obtain ⟨k, h6⟩ := h
-          use k + 1
-          rw[h6]
-          ring_nf
-        case inr h6 =>
+    · intro H
+      constructor
+      · omega
+      · cases H
+        case inl h3 =>
           simp_all only
-          dsimp[Odd]
-          dsimp[Odd] at h
-          obtain ⟨k, h6⟩ := h
-          use k + 2
-          rw[h6]
-          ring_nf
+        case inr h4 =>
+          cases h4
+          case inl h5 =>
+            simp_all only
+            dsimp[Odd] at h ⊢
+            obtain ⟨k, h6⟩ := h
+            use k + 1
+            rw[h6]
+            ring_nf
+          case inr h6 =>
+            simp_all only
+            dsimp[Odd] at h ⊢
+            obtain ⟨k, h6⟩ := h
+            use k + 2
+            rw[h6]
+            ring_nf
     intro H
     obtain ⟨a, Hh⟩ := H
     have h3 := Odd.not_two_dvd_nat Hh
diff --git a/Compfiles/Usa1996P1.lean b/Compfiles/Usa1996P1.lean
index 600fec9..9a981ae 100644
--- a/Compfiles/Usa1996P1.lean
+++ b/Compfiles/Usa1996P1.lean
@@ -113,9 +113,9 @@ problem usa1996_p1 :
       ring
     · rw [mul_comm]
       rw [Finset.sum_eq_zero]
-      simp only [zero_sub]
-      rw [←neg_mul, ←Real.cos_sub_pi]
-      congr; ring
+      · simp only [zero_sub]
+        rw [←neg_mul, ←Real.cos_sub_pi]
+        congr; ring
       intro n _
       rw [cos_add]
       ring
diff --git a/Compfiles/Usa2001P3.lean b/Compfiles/Usa2001P3.lean
index ba7b784..75e74f8 100644
--- a/Compfiles/Usa2001P3.lean
+++ b/Compfiles/Usa2001P3.lean
@@ -63,11 +63,11 @@ problem usa2001_p3 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c)
   rw [←geq]
   wlog ha1 : a≤1 generalizing a b c with Ha
   · by_cases hb1 : b ≤ 1
-    rw [(by ring_nf : g a b c = g b a c)]
-    exact Ha b a c hb ha hc (by rw [←h]; unfold f; ring_nf) hb1
+    · rw [(by ring_nf : g a b c = g b a c)]
+      exact Ha b a c hb ha hc (by rw [←h]; unfold f; ring_nf) hb1
     by_cases hc1 : c ≤ 1
-    rw [(by ring_nf : g a b c = g c b a)]
-    exact Ha c b a hc hb ha (by rw [←h]; unfold f; ring_nf) hc1
+    · rw [(by ring_nf : g a b c = g c b a)]
+      exact Ha c b a hc hb ha (by rw [←h]; unfold f; ring_nf) hc1
     apply False.elim (ne_of_not_le _ h)
     unfold f
     rw [not_le]
diff --git a/Compfiles/Usa2015P1.lean b/Compfiles/Usa2015P1.lean
index 116d6e8..99d5d33 100644
--- a/Compfiles/Usa2015P1.lean
+++ b/Compfiles/Usa2015P1.lean
@@ -47,7 +47,7 @@ problem usa2015_p1 (x y : ℤ) :
     all_goals obtain ⟨h, hx, hy⟩ := h; rw [hx, hy]; ring_nf; use (h + h ^ 2); ring_nf
   · intro h; apply_fun (· * 3 ^ 3) at h; rw [←mul_pow, (add_mul _ 1)] at h; simp at h
     norm_num at h; norm_cast at h
-    suffices : (x + y) % 3 = 0; rw [←dvd_def]; exact Int.dvd_of_emod_eq_zero this
+    suffices (x + y) % 3 = 0 by rw [←dvd_def]; exact Int.dvd_of_emod_eq_zero this
     have h1 : (x ^ (2 : ℕ) + x * y + y ^ (2 : ℕ)) * (27 : ℤ) % 3 =
               (x + y + (3 : ℤ)) ^ (3 : ℕ) % 3 := by rw [h]
     clear h
diff --git a/lakefile.lean b/lakefile.lean
index 6fa4bd6..e6d5f8f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,13 +2,17 @@ import Lake
 
 open Lake DSL
 
-package compfiles where
-  leanOptions := #[
+abbrev leanOptions : Array LeanOption := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
     ⟨`autoImplicit, false⟩,
     ⟨`relaxedAutoImplicit, false⟩
+--    ⟨`weak.linter.style.multiGoal, true⟩
   ]
 
+package compfiles where
+  leanOptions := leanOptions
+  moreServerOptions := leanOptions
+
 @[default_target]
 lean_lib ProblemExtraction