fixes from Kevin's review

kim-em · kim-em · commit 68f709d32346 · 2025-03-31T09:26:59.000+11:00
diff --git a/.github/workflows/nightly_bump_toolchain.yml b/.github/workflows/nightly_bump_toolchain.yml
@@ -2,7 +2,10 @@ name: Bump lean-toolchain on nightly-testing
 
 on:
   schedule:
-    - cron: '0 10/3 * * *'  # Run every three hours, starting at 11AM CET/2AM PT.
+    - cron: '0 10/3 * * *'
+    # Run every three hours, starting at 11AM CET/2AM PT.
+    # This should be 3 hours after lean4 starts building its nightly,
+    # and 15 minutes after batteries `nightly-testing` branch bumps its toolchain.
   workflow_dispatch:
 
 jobs:
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -1199,8 +1199,7 @@ theorem erase_diff_erase_sublist_of_sublist {a : α} :
     else by
       simp only [erase_cons_head, erase_cons_tail (not_beq_of_ne heq),
         diff_cons ((List.erase l₂ a)) (List.erase l₁ a) b, diff_cons l₂ l₁ b,
-        -- FIXME remove use of named argument before merging
-        erase_comm (a := a)]
+        erase_comm a]
       have h' := h.erase b
       rw [erase_cons_head] at h'
       exact @erase_diff_erase_sublist_of_sublist _ l₁ (l₂.erase b) h'
diff --git a/Mathlib/Data/Multiset/AddSub.lean b/Mathlib/Data/Multiset/AddSub.lean
@@ -126,7 +126,7 @@ protected lemma add_right_inj : s + t = s + u ↔ t = u := by classical simp [Mu
 
 @[simp]
 theorem card_add (s t : Multiset α) : card (s + t) = card s + card t :=
-  Quotient.inductionOn₂ s t fun _ _ =>length_append
+  Quotient.inductionOn₂ s t fun _ _ => length_append
 
 end add
 
