feat(Algebra/Group/Submonoid): type class to indicate that supremum in a SubmonoidClass agrees with supremum of submonoids

[TentativeConvert]

Add a type class SubmonoidClass.IsConcreteSSup to indicate that the canonical map .ofClass from a class S of submonoids of M to Submonoid M preserves suprema.

---

This PR implements the minimal type class assumption needed to make „pushfoward of gradings along maps of indexing sets“ – see draft PR #39356 – work in some SetLike generality.

Given {S M : Type*} [SetLike S M] [Monoid M] [SubmonoidClass S M], we have canonical maps

   S → Submonoid M → Set M

The first is Submonoid.ofClass, the second and the composition are coe maps coming from the SetLike structures. Depending on S, these maps may or may not satisfy various properties with respect the lattice structures on Submonoid M and Set M. Mathlib so far includes the type class [IsConcreteLE S M], which asserts that the composition S → Set M is order-preserving and order-reflecting. The type class defined here asserts that the first map, S → Submonoid M, preserves suprema.

In examples such as S = Subgroup M, S = Submodule R M, much more is true – in these cases, S is a complete sublattice of Submonoid M. But there are also examples where only the weaker property defined here holds, e.g. S = OpenSubgroup M for a topological group M.

Note on outParam: I did not write (M : outParam Type*) in the assumptions of SubmonoidClass.IsConcreteSSup in accordance with the DocString of Setlike. However, we do have (B : outParam Type*) in the definition of IsConcreteLE, so perhaps I'm misinterpreting the DocString.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue 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. The review dashboard has a dedicated webpage 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/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary e97fc580bf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Group.Submonoid.SSup (new file)	276

---

Declarations diff

+ AddSubmonoidClass.IsConcreteSSup
+ SubmonoidClass.IsConcreteSSup
+ iSup_toSubmonoid
+ instance (M : Type*) [Monoid M] : IsConcreteSSup (Submonoid M) M
+ mem_iSup_iff_mem_iSup_Submonoid

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.