Trigger CI for leanprover-community/batteries#1007

Author: leanprover-community-mathlib4-bot

.github/build.in.yml

@@ -356,7 +356,7 @@ jobs:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@3.0.0
+        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/bors.yml

@@ -366,7 +366,7 @@ jobs:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@3.0.0
+        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/build.yml

@@ -373,7 +373,7 @@ jobs:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@3.0.0
+        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/build_fork.yml

@@ -370,7 +370,7 @@ jobs:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@3.0.0
+        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

.github/workflows/update_dependencies.yml

@@ -31,7 +31,7 @@ jobs:
       - name: Get PR and labels
         if: ${{ steps.sha.outputs.sha }}
         id: PR # all the steps below are skipped if 'ready-to-merge' is in the list of labels found here
-        uses: 8BitJonny/gh-get-current-pr@3.0.0
+        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:

Mathlib.lean

@@ -431,6 +431,7 @@ import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Conj
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.GroupWithZero.Divisibility
+import Mathlib.Algebra.GroupWithZero.Equiv
 import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.GroupWithZero.Idempotent
 import Mathlib.Algebra.GroupWithZero.Indicator
@@ -942,6 +943,7 @@ import Mathlib.Algebra.Polynomial.Splits
 import Mathlib.Algebra.Polynomial.SumIteratedDerivative
 import Mathlib.Algebra.Polynomial.Taylor
 import Mathlib.Algebra.Polynomial.UnitTrinomial
+import Mathlib.Algebra.Polynomial.ofFn
 import Mathlib.Algebra.PresentedMonoid.Basic
 import Mathlib.Algebra.Prime.Defs
 import Mathlib.Algebra.Prime.Lemmas
@@ -2994,6 +2996,7 @@ import Mathlib.Data.Matroid.IndepAxioms
 import Mathlib.Data.Matroid.Init
 import Mathlib.Data.Matroid.Loop
 import Mathlib.Data.Matroid.Map
+import Mathlib.Data.Matroid.Minor.Basic
 import Mathlib.Data.Matroid.Rank.Cardinal
 import Mathlib.Data.Matroid.Rank.Finite
 import Mathlib.Data.Matroid.Restrict
@@ -4535,10 +4538,12 @@ import Mathlib.Order.Heyting.Hom
 import Mathlib.Order.Heyting.Regular
 import Mathlib.Order.Hom.Basic
 import Mathlib.Order.Hom.Bounded
+import Mathlib.Order.Hom.BoundedLattice
 import Mathlib.Order.Hom.CompleteLattice
 import Mathlib.Order.Hom.Lattice
 import Mathlib.Order.Hom.Order
 import Mathlib.Order.Hom.Set
+import Mathlib.Order.Hom.WithTopBot
 import Mathlib.Order.Ideal
 import Mathlib.Order.InitialSeg
 import Mathlib.Order.Interval.Basic
@@ -4732,6 +4737,7 @@ import Mathlib.Probability.Process.Filtration
 import Mathlib.Probability.Process.HittingTime
 import Mathlib.Probability.Process.PartitionFiltration
 import Mathlib.Probability.Process.Stopping
+import Mathlib.Probability.ProductMeasure
 import Mathlib.Probability.StrongLaw
 import Mathlib.Probability.UniformOn
 import Mathlib.Probability.Variance
@@ -6051,6 +6057,7 @@ import Mathlib.Topology.UniformSpace.CompleteSeparated
 import Mathlib.Topology.UniformSpace.Completion
 import Mathlib.Topology.UniformSpace.Defs
 import Mathlib.Topology.UniformSpace.Dini
+import Mathlib.Topology.UniformSpace.DiscreteUniformity
 import Mathlib.Topology.UniformSpace.Equicontinuity
 import Mathlib.Topology.UniformSpace.Equiv
 import Mathlib.Topology.UniformSpace.HeineCantor

Mathlib/Algebra/Field/Equiv.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
 import Mathlib.Algebra.Field.IsField
-import Mathlib.Algebra.GroupWithZero.Hom
+import Mathlib.Algebra.GroupWithZero.Equiv
 
 /-!
 # If a semiring is a field, any isomorphic semiring is also a field.

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -401,9 +401,17 @@ instance (priority := 100) normal_in_normalizer : (H.subgroupOf H.normalizer).No
   (normal_subgroupOf_iff_le_normalizer H.le_normalizer).mpr le_rfl
 
 @[to_additive]
-theorem le_normalizer_of_normal [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer :=
+theorem le_normalizer_of_normal_subgroupOf [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) :
+    K ≤ H.normalizer :=
   (normal_subgroupOf_iff_le_normalizer HK).mp hK
 
+@[to_additive]
+theorem subset_normalizer_of_normal {S : Set G} [hH : H.Normal] : S ⊆ H.normalizer :=
+  (@normalizer_eq_top _ _ H hH) ▸ le_top
+
+@[to_additive]
+theorem le_normalizer_of_normal [H.Normal] : K ≤ H.normalizer := subset_normalizer_of_normal
+
 @[to_additive]
 theorem inf_normalizer_le_normalizer_inf : H.normalizer ⊓ K.normalizer ≤ (H ⊓ K).normalizer :=
   fun _ h g ↦ and_congr (h.1 g) (h.2 g)
@@ -897,6 +905,18 @@ theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Nor
     apply H₂.mul_mem _ (H₂.inv_mem hy)
     apply hH₂.conj_mem _ hy
 
+@[to_additive]
+theorem normal_subgroupOf_of_le_normalizer {H N : Subgroup G}
+    (hLE : H ≤ N.normalizer) : (N.subgroupOf H).Normal := by
+  rw [normal_subgroupOf_iff_le_normalizer_inf]
+  exact (le_inf hLE H.le_normalizer).trans inf_normalizer_le_normalizer_inf
+
+@[to_additive]
+theorem normal_subgroupOf_sup_of_le_normalizer {H N : Subgroup G}
+    (hLE : H ≤ N.normalizer) : (N.subgroupOf (H ⊔ N)).Normal := by
+  rw [normal_subgroupOf_iff_le_normalizer le_sup_right]
+  exact sup_le hLE le_normalizer
+
 end SubgroupNormal
 
 end Subgroup

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -227,15 +227,23 @@ theorem sup_eq_closure_mul (H K : Subgroup G) : H ⊔ K = closure ((H : Set G) *
     ((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])
 
 @[to_additive]
-theorem set_mul_normal_comm (s : Set G) (N : Subgroup G) [hN : N.Normal] :
-    s * (N : Set G) = (N : Set G) * s := by
+theorem set_mul_normalizer_comm (S : Set G) (N : Subgroup G) (hLE : S ⊆ N.normalizer) :
+    S * N = N * S := by
   rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]
-  simp only [image_mul_left, image_mul_right, Set.preimage, SetLike.mem_coe, hN.mem_comm_iff]
+  simp only [image_mul_left, image_mul_right, Set.preimage]
+  congr! 5 with s hs x
+  exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm
 
-/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product) when `N` is normal. -/
+@[to_additive]
+theorem set_mul_normal_comm (S : Set G) (N : Subgroup G) [hN : N.Normal] :
+    S * (N : Set G) = (N : Set G) * S := set_mul_normalizer_comm S N subset_normalizer_of_normal
+
+/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product)
+when `H` is a subgroup of the normalizer of `N` in `G`. -/
 @[to_additive "The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
-when `N` is normal."]
-theorem mul_normal (H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) = H * N := by
+when `H` is a subgroup of the normalizer of `N` in `G`."]
+theorem coe_mul_of_left_le_normalizer_right (H N : Subgroup G) (hLE : H ≤ N.normalizer) :
+    (↑(H ⊔ N) : Set G) = H * N := by
   rw [sup_eq_closure_mul]
   refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
   induction hx using closure_induction'' with
@@ -244,19 +252,33 @@ theorem mul_normal (H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) =
   | inv_mem x hx =>
     obtain ⟨x, hx, y, hy, rfl⟩ := hx
     simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
-      using mul_mem_mul (inv_mem hx) (hN.conj_mem _ (inv_mem hy) x)
+      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))
   | mul x' x' _ _ hx hx' =>
     obtain ⟨x, hx, y, hy, rfl⟩ := hx
     obtain ⟨x', hx', y', hy', rfl⟩ := hx'
     refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
-    · simpa using hN.conj_mem _ hy x'⁻¹
+    · exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
     · simp only [mul_assoc, mul_inv_cancel_left]
 
+/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when
+`H` is a subgroup of the normalizer of `N` in `G`. -/
+@[to_additive "The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
+when `H` is a subgroup of the normalizer of `N` in `G`."]
+theorem coe_mul_of_right_le_normalizer_left (N H : Subgroup G) (hLE : H ≤ N.normalizer) :
+    (↑(N ⊔ H) : Set G) = N * H := by
+  rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]
+
+/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product) when `N` is normal. -/
+@[to_additive "The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
+when `N` is normal."]
+theorem mul_normal (H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) = H * N :=
+  coe_mul_of_left_le_normalizer_right H N le_normalizer_of_normal
+
 /-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when `N` is normal. -/
 @[to_additive "The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
 when `N` is normal."]
-theorem normal_mul (N H : Subgroup G) [N.Normal] : (↑(N ⊔ H) : Set G) = N * H := by
-  rw [← set_mul_normal_comm, sup_comm, mul_normal]
+theorem normal_mul (N H : Subgroup G) [N.Normal] : (↑(N ⊔ H) : Set G) = N * H :=
+  coe_mul_of_right_le_normalizer_left N H le_normalizer_of_normal
 
 @[to_additive]
 theorem mul_inf_assoc (A B C : Subgroup G) (h : A ≤ C) :

Mathlib/Algebra/GroupWithZero/Equiv.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.Group.Equiv.Defs
+import Mathlib.Algebra.GroupWithZero.Hom
+
+/-! # Isomorphisms of monoids with zero -/
+
+namespace MulEquivClass
+variable {F α β : Type*} [EquivLike F α β]
+
+-- See note [lower instance priority]
+instance (priority := 100) toZeroHomClass [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] :
+    ZeroHomClass F α β where
+  map_zero f :=
+    calc
+      f 0 = f 0 * f (EquivLike.inv f 0) := by rw [← map_mul, zero_mul]
+        _ = 0 := by simp
+
+-- See note [lower instance priority]
+instance (priority := 100) toMonoidWithZeroHomClass
+    [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
+    MonoidWithZeroHomClass F α β :=
+  { MulEquivClass.instMonoidHomClass F, MulEquivClass.toZeroHomClass with }
+
+end MulEquivClass