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>

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.
 -/

Mathlib/GroupTheory/GroupAction/SubMulAction.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 group_theory.group_action.sub_mul_action
-! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
+! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -42,14 +42,21 @@ universe u u' u'' v
 variable {S : Type u'} {T : Type u''} {R : Type u} {M : Type v}
 
 /-- `SMulMemClass S R M` says `S` is a type of subsets `s ≤ M` that are closed under the
-scalar action of `R` on `M`. -/
+scalar action of `R` on `M`.
+
+Note that only `R` is marked as an `outParam` here, since `M` is supplied by the `SetLike`
+class instead.
+-/
 class SMulMemClass (S : Type _) (R : outParam <| Type _) (M : Type _) [SMul R M] [SetLike S M] where
   /-- Multiplication by a scalar on an element of the set remains in the set. -/
   smul_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ s
 #align smul_mem_class SMulMemClass
 
 /-- `VAddMemClass S R M` says `S` is a type of subsets `s ≤ M` that are closed under the
-additive action of `R` on `M`. -/
+additive action of `R` on `M`.
+
+Note that only `R` is marked as an `outParam` here, since `M` is supplied by the `SetLike`
+class instead. -/
 class VAddMemClass (S : Type _) (R : outParam <| Type _) (M : Type _) [VAdd R M] [SetLike S M] where
   /-- Addition by a scalar with an element of the set remains in the set. -/
   vadd_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r +ᵥ m ∈ s

Mathlib/GroupTheory/Submonoid/Basic.lean

@@ -6,7 +6,7 @@ Amelia Livingston, Yury Kudryashov
 Ported by: Anatole Dedecker
 
 ! This file was ported from Lean 3 source module group_theory.submonoid.basic
-! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
+! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Logic/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 
 ! This file was ported from Lean 3 source module logic.basic
-! leanprover-community/mathlib commit 1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e
+! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Order/InitialSeg.lean

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

Mathlib/Order/RelClasses.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module order.rel_classes
-! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
+! leanprover-community/mathlib commit bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -603,39 +603,57 @@ variable [HasSubset α] {a b c : α}
 
 lemma subset_of_eq_of_subset (hab : a = b) (hbc : b ⊆ c) : a ⊆ c := by rwa [hab]
 #align subset_of_eq_of_subset subset_of_eq_of_subset
+
 lemma subset_of_subset_of_eq (hab : a ⊆ b) (hbc : b = c) : a ⊆ c := by rwa [←hbc]
 #align subset_of_subset_of_eq subset_of_subset_of_eq
-@[refl] lemma subset_refl [IsRefl α (· ⊆ ·)] (a : α) : a ⊆ a := refl _
+
+@[refl]
+lemma subset_refl [IsRefl α (· ⊆ ·)] (a : α) : a ⊆ a := refl _
 #align subset_refl subset_refl
+
 lemma subset_rfl [IsRefl α (· ⊆ ·)] : a ⊆ a := refl _
 #align subset_rfl subset_rfl
+
 lemma subset_of_eq [IsRefl α (· ⊆ ·)] : a = b → a ⊆ b := fun h => h ▸ subset_rfl
 #align subset_of_eq subset_of_eq
+
 lemma superset_of_eq [IsRefl α (· ⊆ ·)] : a = b → b ⊆ a := fun h => h ▸ subset_rfl
 #align superset_of_eq superset_of_eq
+
 lemma ne_of_not_subset [IsRefl α (· ⊆ ·)] : ¬a ⊆ b → a ≠ b := mt subset_of_eq
 #align ne_of_not_subset ne_of_not_subset
+
 lemma ne_of_not_superset [IsRefl α (· ⊆ ·)] : ¬a ⊆ b → b ≠ a := mt superset_of_eq
 #align ne_of_not_superset ne_of_not_superset
-@[trans] lemma subset_trans [IsTrans α (· ⊆ ·)] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c := _root_.trans
+
+@[trans]
+lemma subset_trans [IsTrans α (· ⊆ ·)] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c := _root_.trans
 #align subset_trans subset_trans
+
 lemma subset_antisymm [IsAntisymm α (· ⊆ ·)] : a ⊆ b → b ⊆ a → a = b := antisymm
 #align subset_antisymm subset_antisymm
+
 lemma superset_antisymm [IsAntisymm α (· ⊆ ·)] : a ⊆ b → b ⊆ a → b = a := antisymm'
 #align superset_antisymm superset_antisymm
 
 alias subset_of_eq_of_subset ← Eq.trans_subset
 #align eq.trans_subset Eq.trans_subset
+
 alias subset_of_subset_of_eq ← HasSubset.subset.trans_eq
 #align has_subset.subset.trans_eq HasSubset.subset.trans_eq
+
 alias subset_of_eq ← Eq.subset' --TODO: Fix it and kill `Eq.subset`
 #align eq.subset' Eq.subset'
+
 alias superset_of_eq ← Eq.superset
 #align eq.superset Eq.superset
+
 alias subset_trans ← HasSubset.Subset.trans
 #align has_subset.subset.trans HasSubset.Subset.trans
+
 alias subset_antisymm ← HasSubset.Subset.antisymm
 #align has_subset.subset.antisymm HasSubset.Subset.antisymm
+
 alias superset_antisymm ← HasSubset.Subset.antisymm'
 #align has_subset.subset.antisymm' HasSubset.Subset.antisymm'
 
@@ -654,33 +672,47 @@ variable [HasSSubset α] {a b c : α}
 
 lemma ssubset_of_eq_of_ssubset (hab : a = b) (hbc : b ⊂ c) : a ⊂ c := by rwa [hab]
 #align ssubset_of_eq_of_ssubset ssubset_of_eq_of_ssubset
+
 lemma ssubset_of_ssubset_of_eq (hab : a ⊂ b) (hbc : b = c) : a ⊂ c := by rwa [←hbc]
 #align ssubset_of_ssubset_of_eq ssubset_of_ssubset_of_eq
+
 lemma ssubset_irrefl [IsIrrefl α (· ⊂ ·)] (a : α) : ¬a ⊂ a := irrefl _
 #align ssubset_irrefl ssubset_irrefl
+
 lemma ssubset_irrfl [IsIrrefl α (· ⊂ ·)] {a : α} : ¬a ⊂ a := irrefl _
 #align ssubset_irrfl ssubset_irrfl
+
 lemma ne_of_ssubset [IsIrrefl α (· ⊂ ·)] {a b : α} : a ⊂ b → a ≠ b := ne_of_irrefl
 #align ne_of_ssubset ne_of_ssubset
+
 lemma ne_of_ssuperset [IsIrrefl α (· ⊂ ·)] {a b : α} : a ⊂ b → b ≠ a := ne_of_irrefl'
 #align ne_of_ssuperset ne_of_ssuperset
-@[trans] lemma ssubset_trans [IsTrans α (· ⊂ ·)] {a b c : α} : a ⊂ b → b ⊂ c → a ⊂ c := _root_.trans
+
+@[trans]
+lemma ssubset_trans [IsTrans α (· ⊂ ·)] {a b c : α} : a ⊂ b → b ⊂ c → a ⊂ c := _root_.trans
 #align ssubset_trans ssubset_trans
+
 lemma ssubset_asymm [IsAsymm α (· ⊂ ·)] {a b : α} : a ⊂ b → ¬b ⊂ a := asymm
 #align ssubset_asymm ssubset_asymm
 
 alias ssubset_of_eq_of_ssubset ← Eq.trans_ssubset
 #align eq.trans_ssubset Eq.trans_ssubset
+
 alias ssubset_of_ssubset_of_eq ← HasSSubset.SSubset.trans_eq
 #align has_ssubset.ssubset.trans_eq HasSSubset.SSubset.trans_eq
+
 alias ssubset_irrfl ← HasSSubset.SSubset.false
 #align has_ssubset.ssubset.false HasSSubset.SSubset.false
+
 alias ne_of_ssubset ← HasSSubset.SSubset.ne
 #align has_ssubset.ssubset.ne HasSSubset.SSubset.ne
+
 alias ne_of_ssuperset ← HasSSubset.SSubset.ne'
 #align has_ssubset.ssubset.ne' HasSSubset.SSubset.ne'
+
 alias ssubset_trans ← HasSSubset.SSubset.trans
 #align has_ssubset.ssubset.trans HasSSubset.SSubset.trans
+
 alias ssubset_asymm ← HasSSubset.SSubset.asymm
 #align has_ssubset.ssubset.asymm HasSSubset.SSubset.asymm
 

Mathlib/Order/WithBot.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module order.with_bot
-! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! leanprover-community/mathlib commit 995b47e555f1b6297c7cf16855f1023e355219fb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/RingTheory/Subsemiring/Basic.lean

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