Merge branch 'master' into limsup_const_mul

Author: jvanwinden

.github/workflows/label_new_contributor.yml

@@ -106,7 +106,7 @@ jobs:
             ## Welcome new contributor!
             Thank you for contributing to Mathlib! If you haven't done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html).
 
-            We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr).
+            We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr). The review dashboard has [a dedicated webpage](https://leanprover-community.github.io/queueboard/on_the_queue.html?search=${{ github.event.pull_request.number }}) which shows whether your PR is on the review queue, and (if not), why.
 
             If you haven't already done so, please come to [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/), introduce yourself, and mention your new PR.
 

Mathlib/Data/Set/Card.lean

@@ -188,6 +188,7 @@ theorem encard_pi_eq_prod_encard [h : Fintype α] {ι : α → Type*} {s : ∀ i
 
 section Lattice
 
+@[gcongr]
 theorem encard_le_encard (h : s ⊆ t) : s.encard ≤ t.encard := by
   rw [← union_diff_cancel h, encard_union_eq disjoint_sdiff_right]; exact le_self_add
 
@@ -296,7 +297,7 @@ theorem one_le_encard_insert (s : Set α) : 1 ≤ (insert a s).encard :=
   ENat.one_le_iff_ne_zero.mpr <| encard_ne_zero_of_mem (mem_insert a s)
 
 theorem encard_singleton_inter (s : Set α) (x : α) : ({x} ∩ s).encard ≤ 1 := by
-  rw [← encard_singleton x]; exact encard_le_encard inter_subset_left
+  grw [← encard_singleton x, inter_subset_left]
 
 theorem encard_diff_singleton_add_one (h : a ∈ s) :
     (s \ {a}).encard + 1 = s.encard := by
@@ -485,9 +486,7 @@ theorem _root_.Function.Embedding.encard_le (e : s ↪ t) : s.encard ≤ t.encar
 theorem encard_image_le (f : α → β) (s : Set α) : (f '' s).encard ≤ s.encard := by
   obtain (h | h) := isEmpty_or_nonempty α
   · rw [s.eq_empty_of_isEmpty]; simp
-  rw [← (f.invFunOn_injOn_image s).encard_image]
-  apply encard_le_encard
-  exact f.invFunOn_image_image_subset s
+  grw [← (f.invFunOn_injOn_image s).encard_image, f.invFunOn_image_image_subset s]
 
 theorem Finite.injOn_of_encard_image_eq (hs : s.Finite) (h : (f '' s).encard = s.encard) :
     InjOn f s := by
@@ -506,7 +505,7 @@ lemma encard_preimage_of_bijective (hf : f.Bijective) (t : Set β) : (f ⁻¹' t
 
 theorem encard_le_encard_of_injOn (hf : MapsTo f s t) (f_inj : InjOn f s) :
     s.encard ≤ t.encard := by
-  rw [← f_inj.encard_image]; apply encard_le_encard; rintro _ ⟨x, hx, rfl⟩; exact hf hx
+  grw [← f_inj.encard_image, hf.image_subset]
 
 open Notation in
 lemma encard_preimage_val_le_encard_left (P Q : Set α) : (P ↓∩ Q).encard ≤ P.encard :=

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -941,10 +941,9 @@ theorem dvd_antisymm {a b : Ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b :
 instance antisymm : @Std.Antisymm Ordinal (· ∣ ·) :=
   ⟨@dvd_antisymm⟩
 
-/-- `a % b` is the unique ordinal `o'` satisfying
-  `a = b * o + o'` with `o' < b`. -/
-instance mod : Mod Ordinal :=
-  ⟨fun a b => a - b * (a / b)⟩
+/-- `a % b` is the unique ordinal `r` satisfying `a = b * q + r` with `r < b`. -/
+instance mod : Mod Ordinal where
+  mod a b := a - b * (a / b)
 
 theorem mod_def (a b : Ordinal) : a % b = a - b * (a / b) :=
   rfl
@@ -953,27 +952,29 @@ theorem mod_le (a b : Ordinal) : a % b ≤ a :=
   sub_le_self a _
 
 @[simp]
-theorem mod_zero (a : Ordinal) : a % 0 = a := by simp only [mod_def, div_zero, zero_mul, sub_zero]
+theorem mod_zero (a : Ordinal) : a % 0 = a := by simp [mod_def]
 
 theorem mod_eq_of_lt {a b : Ordinal} (h : a < b) : a % b = a := by
-  simp only [mod_def, div_eq_zero_of_lt h, mul_zero, sub_zero]
+  simp [mod_def, div_eq_zero_of_lt h]
 
 @[simp]
-theorem zero_mod (b : Ordinal) : 0 % b = 0 := by simp only [mod_def, zero_div, mul_zero, sub_self]
+theorem zero_mod (b : Ordinal) : 0 % b = 0 := by simp [mod_def]
 
 theorem div_add_mod (a b : Ordinal) : b * (a / b) + a % b = a :=
   Ordinal.add_sub_cancel_of_le <| mul_div_le _ _
 
-theorem mod_lt (a) {b : Ordinal} (h : b ≠ 0) : a % b < b :=
-  (add_lt_add_iff_left (b * (a / b))).1 <| by rw [div_add_mod]; exact lt_mul_div_add a h
+theorem mod_lt (a) {b : Ordinal} (h : b ≠ 0) : a % b < b := by
+  rw [← add_lt_add_iff_left, div_add_mod]
+  exact lt_mul_div_add a h
 
 @[simp]
-theorem mod_self (a : Ordinal) : a % a = 0 :=
-  if a0 : a = 0 then by simp only [a0, zero_mod]
-  else by simp only [mod_def, div_self a0, mul_one, sub_self]
+theorem mod_self (a : Ordinal) : a % a = 0 := by
+  obtain rfl | ha := eq_or_ne a 0
+  · simp
+  · simp [mod_def, ha]
 
 @[simp]
-theorem mod_one (a : Ordinal) : a % 1 = 0 := by simp only [mod_def, div_one, one_mul, sub_self]
+theorem mod_one (a : Ordinal) : a % 1 = 0 := by simp [mod_def]
 
 theorem dvd_of_mod_eq_zero {a b : Ordinal} (H : a % b = 0) : b ∣ a :=
   ⟨a / b, by simpa [H] using (div_add_mod a b).symm⟩

Mathlib/Topology/Algebra/Ring/Ideal.lean

@@ -45,6 +45,20 @@ https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.
 theorem Ideal.closure_eq_of_isClosed (I : Ideal R) (hI : IsClosed (I : Set R)) : I.closure = I :=
   SetLike.ext' hI.closure_eq
 
+variable (R)
+
+/-- The connected component of zero in a topological ring as an ideal. -/
+def Ideal.connectedComponentOfZero : Ideal R where
+  __ := AddSubgroup.connectedComponentOfZero R
+  smul_mem' c x h := IsConnected.subset_connectedComponent
+    (isConnected_connectedComponent.image _ (continuous_const_mul c).continuousOn)
+    ⟨0, mem_connectedComponent, mul_zero c⟩ ⟨x, h, rfl⟩
+
+@[simp]
+theorem Ideal.coe_connectedComponentOfZero :
+    (Ideal.connectedComponentOfZero R : Set R) = connectedComponent 0 :=
+  rfl
+
 end Ring
 
 section CommRing

scripts/autolabel.lean

@@ -166,6 +166,10 @@ structure LabelData (label : Label) where
   /-- Array of paths which should be excluded.
   Any modifications to a file in an excluded path are ignored for the purposes of labelling. -/
   exclusions : Array FilePath := #[]
+  /-- Labels which are "lower" in the Mathlib import order. These labels will not be added
+  alongside the label. For example any PR to `t-ring-theory` might modify files from `t-algebra`
+  but should only get the former label -/
+  dependencies : Array Label := #[]
   deriving BEq, Hashable
 
 /-- Mathlib labels and their corresponding folders -/
@@ -277,6 +281,18 @@ 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 -/
+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
+  labels.filter (!dependentLabels.contains ·)
+
 /-!
 Testing the functionality of the declarations defined in this script
 -/
@@ -414,8 +430,7 @@ unsafe def main (args : List String): IO UInt32 := do
   let modifiedFiles : Array FilePath := (gitDiff.splitOn "\n").toArray.map (⟨·⟩)
 
   -- find labels covering the modified files
-  let labels := getMatchingLabels modifiedFiles
-
+  let labels := dropDependentLabels <| getMatchingLabels modifiedFiles
   println s!"::notice::Applicable labels: {labels}"
 
   match labels with