feat(scripts/autolabel): collect label dependencies transitively (leanprover-community#36242)

Collect label dependencies transitively. if `t-algebraic-geometry -> t-ring-theory` and `t-ring-theory -> t-algebra` are two dependencies where the latter label is dropped from the list of applicable labels, then `t-algebraic-geometry -> t-algebra` is also dropped.

Author: joneugster

scripts/autolabel.lean

@@ -294,16 +294,15 @@ def getMatchingLabels (files : Array FilePath) : Array Label :=
   -- return sorted list of labels
   applicable |>.qsort (·.toString < ·.toString)
 
-/-- Helper function: union of all labels an all their dependent labels -/
+/-- Helper function: union of all labels and all their dependent labels -/
 partial def collectLabelsAndDependentLabels (labels: Array Label) : Array Label :=
   labels.flatMap fun label ↦
     (collectLabelsAndDependentLabels (mathlibLabelData label).dependencies).push label
 
 /-- Reduce a list of labels to not include any which are dependencies of other
 labels in the list -/
 def dropDependentLabels (labels: Array Label) : Array Label :=
-  let dependentLabels := labels.flatMap fun label ↦
-    (mathlibLabelData label).dependencies
+  let dependentLabels := collectLabelsAndDependentLabels labels
   labels.filter (!dependentLabels.contains ·)
 
 /-!