chore: update SHA of already forward-ported files (#2181)

Update some SHAs of files that changed in mathlib3.

These 17 files need mainly only updated SHA as they've been only touched by backports or already have been forward-ported.

The relevant changes are:

* [Algebra.Group.Defs (#17884)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/defs?range=41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3..2e0975f6a25dd3fbfb9e41556a77f075f6269748)
  * #945
* [Algebra.Group.WithOne.Defs (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/with_one/defs?range=e574b1a4e891376b0ef974b926da39e05da12a06..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Algebra.Module.Submodule.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/algebra/module/submodule/basic?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Algebra.Order.Monoid.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/with_top?range=2258b40dacd2942571c8ce136215350c702dc78f..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Algebra.Order.Ring.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/ring/with_top?range=550b58538991c8977703fdeb7c9d51a5aa27df11..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Data.Finset.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/n_ary?range=9003f28797c0664a49e4179487267c494477d853..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Option.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/option/n_ary?range=2258b40dacd2942571c8ce136215350c702dc78f..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Set.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/set/n_ary?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.SetLike.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/data/set_like/basic?range=fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Data.Sum.Basic (#18184)](https://leanprover-community.github.io/mathlib-port-status/file/data/sum/basic?range=d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..f4ecb599422baaf39055d8278c7d9ef3b5b72b88)
  * #1583
* [GroupTheory.GroupAction.SubMulAction  (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/group_action/sub_mul_action?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [GroupTheory.Submonoid.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/basic?range=207cfac9fcd06138865b5d04f7091e46d9320432..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [ Logic.Basic (#18291): backport](https://leanprover-community.github.io/mathlib-port-status/file/logic/basic?range=1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e..feb99064803fd3108e37c18b0f77d0a8344677a3)
  * #1509
* [Order.InitialSeg (#18198): backport](https://leanprover-community.github.io/mathlib-port-status/file/order/initial_seg?range=ee0c179cd3c8a45aa5bffbf1b41d8dbede452865..7c3269ca3fa4c0c19e4d127cd7151edbdbf99ed4)
* [Order.RelClasses (#17957)](https://leanprover-community.github.io/mathlib-port-status/file/order/rel_classes?range=c4658a649d216f57e99621708b09dcb3dcccbd23..bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e)
  * #1047
* [Order.WithBot (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/order/with_bot?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [RingTheory.Subsemiring.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subsemiring/basic?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: joneugster

Mathlib/Algebra/Group/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.group.defs
-! leanprover-community/mathlib commit 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
+! leanprover-community/mathlib commit 2e0975f6a25dd3fbfb9e41556a77f075f6269748
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 
 ! This file was ported from Lean 3 source module algebra.group.with_one.defs
-! leanprover-community/mathlib commit e574b1a4e891376b0ef974b926da39e05da12a06
+! leanprover-community/mathlib commit 995b47e555f1b6297c7cf16855f1023e355219fb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -98,7 +98,7 @@ instance inhabited : Inhabited (WithOne α) :=
 instance nontrivial [Nonempty α] : Nontrivial (WithOne α) :=
   Option.nontrivial
 
--- porting note: this new declaration is here to make `((a : α): WithOne α)` have type `WithOne α` ;
+-- porting note: this new declaration is here to make `((a : α): WithOne α)` have type `WithOne α`;
 -- otherwise the coercion kicks in and it becomes `Option.some a : WithOne α` which
 -- becomes `Option.some a : Option α`.
 /-- The canonical map from `α` into `WithOne α` -/
@@ -190,11 +190,6 @@ protected theorem cases_on {P : WithOne α → Prop} : ∀ x : WithOne α, P 1 
 -- port note: I don't know if `elab_as_elim` is being added to the additivised declaration.
 attribute [elab_as_elim] WithZero.cases_on
 
--- porting note: in Lean 3 there was the following comment:
--- the `show` statements in the proofs are important, because otherwise the generated lemmas
--- `WithOne.mulOneClass._proof_{1,2}` have an ill-typed statement after `WithOne` is made
--- irreducible. Maybe one day when mathlib is ported to Lean 4 we can experiment
--- to see if these `show` comments can be removed.
 @[to_additive]
 instance mulOneClass [Mul α] : MulOneClass (WithOne α) where
   mul := (· * ·)
@@ -290,7 +285,7 @@ instance commMonoidWithZero [CommMonoid α] : CommMonoidWithZero (WithZero α) :
   { WithZero.monoidWithZero, WithZero.commSemigroup with }
 
 /-- Given an inverse operation on `α` there is an inverse operation
-  on `WithZero α` sending `0` to `0`-/
+  on `WithZero α` sending `0` to `0`. -/
 instance inv [Inv α] : Inv (WithZero α) :=
   ⟨fun a => Option.map Inv.inv a⟩
 

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.module.submodule.basic
-! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
+! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -38,7 +38,11 @@ universe u'' u' u v w
 
 variable {G : Type u''} {S : Type u'} {R : Type u} {M : Type v} {ι : Type w}
 
-/-- `SubmoduleClass S R M` says `S` is a type of submodules `s ≤ M`. -/
+/--
+`SubmoduleClass S R M` says `S` is a type of submodules `s ≤ M`.
+
+Note that only `R` is marked as `outParam` since `M` is already supplied by the `SetLike` class.
+-/
 class SubmoduleClass (S : Type _) (R : outParam <| Type _) (M : Type _) [AddZeroClass M] [SMul R M]
   [SetLike S M] [AddSubmonoidClass S M] extends SMulMemClass S R M
 #align submodule_class SubmoduleClass

Mathlib/Algebra/Order/Monoid/WithTop.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 Ported by: Jon Eugster
 
 ! This file was ported from Lean 3 source module algebra.order.monoid.with_top
-! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
+! leanprover-community/mathlib commit e7e2ba8aa216a5833b5ed85a93317263711a36b5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -3,7 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 ! This file was ported from Lean 3 source module algebra.order.ring.with_top
-! leanprover-community/mathlib commit 550b58538991c8977703fdeb7c9d51a5aa27df11
+! leanprover-community/mathlib commit e7e2ba8aa216a5833b5ed85a93317263711a36b5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -425,9 +425,9 @@ instance [MulZeroClass α] [Preorder α] [MulPosMonoRev α] : MulPosMonoRev (Wit
     exact le_of_mul_le_mul_right h x0 ⟩
 
 instance orderedCommSemiring [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
-  OrderedCommSemiring (WithBot α) :=
+    OrderedCommSemiring (WithBot α) :=
   { WithBot.zeroLEOneClass, WithBot.orderedAddCommMonoid, WithBot.commSemiring with
-    mul_le_mul_of_nonneg_left  := fun _ _ _ => mul_le_mul_of_nonneg_left,
-    mul_le_mul_of_nonneg_right := fun _ _ _ => mul_le_mul_of_nonneg_right, }
+    mul_le_mul_of_nonneg_left  := fun _ _ _ => mul_le_mul_of_nonneg_left
+    mul_le_mul_of_nonneg_right := fun _ _ _ => mul_le_mul_of_nonneg_right }
 
 end WithBot

Mathlib/Data/Finset/NAry.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.finset.n_ary
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit 995b47e555f1b6297c7cf16855f1023e355219fb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -475,4 +475,17 @@ theorem image_image₂_right_anticomm {f : α → β' → γ} {g : β → β'} {
   (image_image₂_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm
 #align finset.image_image₂_right_anticomm Finset.image_image₂_right_anticomm
 
+/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
+`Finset.image₂ f`. -/
+theorem image₂_left_identity {f : α → γ → γ} {a : α} (h : ∀ b, f a b = b) (t : Finset γ) :
+    image₂ f {a} t = t :=
+  coe_injective <| by rw [coe_image₂, coe_singleton, Set.image2_left_identity h]
+#align finset.image₂_left_identity Finset.image₂_left_identity
+
+/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
+`Finset.image₂ f`. -/
+theorem image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b = a) (s : Finset γ) :
+    image₂ f s {b} = s := by rw [image₂_singleton_right, funext h, image_id']
+#align finset.image₂_right_identity Finset.image₂_right_identity
+
 end Finset

Mathlib/Data/Option/NAry.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.option.n_ary
-! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
+! leanprover-community/mathlib commit 995b47e555f1b6297c7cf16855f1023e355219fb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Data/Set/NAry.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module data.set.n_ary
-! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
+! leanprover-community/mathlib commit 995b47e555f1b6297c7cf16855f1023e355219fb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Data/SetLike/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module data.set_like.basic
-! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
+! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Data/Sum/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module data.sum.basic
-! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
+! leanprover-community/mathlib commit f4ecb599422baaf39055d8278c7d9ef3b5b72b88
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/