feat(GroupTheory/Finiteness): add general IsMulFG

[tb65536]

This PR adds a general IsMulFG predicate that generalizes all four existing definitions Monoid.FG, Submonoid.FG, Group.FG and Subgroup.FG. Ultimately the plan will be to deprecate all four existing definitions in favor of IsMulFG.

---

[github-actions]

PR summary 6cedfc269b

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.Finiteness	694	703	+9 (+1.30%)

Import changes for all files

Files	Import difference
6 files Mathlib.GroupTheory.FinitelyPresentedGroup Mathlib.GroupTheory.Perm.Centralizer Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour Mathlib.GroupTheory.SpecificGroups.Alternating.Simple	1
3 files Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.IsPerfect Mathlib.GroupTheory.Nilpotent	2
31 files Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.TensorProduct Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Geometry.Convex.Cone.DualFinite Mathlib.GroupTheory.Descent Mathlib.GroupTheory.Torsion Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.DirectSum.Finite Mathlib.LinearAlgebra.PiTensorProduct.Finite Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.CoassocSimps Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MulOpposite Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional	3
Mathlib.GroupTheory.Commutator.Finite Mathlib.GroupTheory.Rank	5
4 files Mathlib.Algebra.AffineMonoid.Basic Mathlib.Algebra.AffineMonoid.Irreducible Mathlib.GroupTheory.Finiteness Mathlib.GroupTheory.MonoidLocalization.Finite	9

---

Declarations diff (regex)

+ IsAddFG
+ IsMulFG
+ IsMulFG.of_surjective
+ exists_iff_exists_finite
+ forall_iff_forall_finite
+ instance (priority := 100) [Finite M] : IsMulFG M := by
+ instance [IsMulFG G] : IsMulFG (⊤ : Subgroup G)
+ instance [IsMulFG G] : IsMulFG f.range
+ instance [IsMulFG H] : IsMulFG (H.map f)
+ instance [IsMulFG M] : IsMulFG (MonoidHom.mrange f)
+ instance [IsMulFG M] : IsMulFG (⊤ : Submonoid M)
+ instance [IsMulFG P] : IsMulFG (P.map f)
++ isMulFG_top_iff
++++ isMulFG_iff
++++ isMulFG_iff_finite

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 6cedfc2).

• +53 new declarations
• −0 removed declarations

+AddGroup.instIsAddFGSubtypeMemAddSubgroupRange
+AddGroup.isAddFG_iff
+AddGroup.isAddFG_iff_finite
+AddMonoid.instIsAddFGSubtypeMemAddSubmonoidMrangeAddMonoidHom
+AddMonoid.isAddFG_iff
+AddMonoid.isAddFG_iff_finite
+AddSubgroup.instIsAddFGSubtypeMemMap
+AddSubgroup.instIsAddFGSubtypeMemTop
+AddSubgroup.isAddFG_iff
+AddSubgroup.isAddFG_iff_finite
+AddSubgroup.isAddFG_top_iff
+AddSubmonoid.closure_eq_zero_union
+AddSubmonoid.instIsAddFGSubtypeMemMapAddMonoidHom
+AddSubmonoid.instIsAddFGSubtypeMemTop
+AddSubmonoid.isAddFG_iff
+AddSubmonoid.isAddFG_iff_finite
+AddSubmonoid.isAddFG_top_iff
+Finset.exists_iff_exists_finite
+Finset.forall_iff_forall_finite
+Group.instIsMulFGSubtypeMemSubgroupRange
+Group.isMulFG_iff
+Group.isMulFG_iff_finite
+IsAddFG
+IsAddFG.casesOn
+IsAddFG.fg_top
+IsAddFG.mk
+IsAddFG.of_surjective
+IsAddFG.rec
+IsAddFG.recOn
+IsMulFG
+IsMulFG.casesOn
+IsMulFG.fg_top
+IsMulFG.mk
+IsMulFG.of_surjective
+IsMulFG.rec
+IsMulFG.recOn
+Monoid.instIsMulFGSubtypeMemSubmonoidMrangeMonoidHom
+Monoid.isMulFG_iff
+Monoid.isMulFG_iff_finite
+Subgroup.instIsMulFGSubtypeMemMap
+Subgroup.instIsMulFGSubtypeMemTop
+Subgroup.isMulFG_iff
+Subgroup.isMulFG_iff_finite
+Subgroup.isMulFG_top_iff
+Submonoid.instIsMulFGSubtypeMemMapMonoidHom
+Submonoid.instIsMulFGSubtypeMemTop
+Submonoid.isMulFG_iff
+Submonoid.isMulFG_iff_finite
+Submonoid.isMulFG_top_iff
+instIsAddFGOfFinite
+instIsMulFGOfFinite
+isAddFG_def
+isMulFG_def

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 6cedfc269b
Reference commit 01cceef430

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Here's what I think is one more option:

structure FG {S M : Type*} [SetLike S M] [InfSet S] (s : S) : Prop where
  fg_top : ∃ fs : Finset M, sInf {s' : S | (fs : Set M) ≤ s'} = s

which then directly replaces Submonoid.FG

[tb65536]

Here's what I think is one more option:

structure FG {S M : Type*} [SetLike S M] [InfSet S] (s : S) : Prop where
  fg_top : ∃ fs : Finset M, sInf {s' : S | (fs : Set M) ≤ s'} = s

which then directly replaces Submonoid.FG

That's a nice definition! And it might even work for other algebraic structures like IntermediateField.FG.

But in the case of this PR, we definitely want some predicate IsMulFG for monoids and groups, in which case there's not much point having a separate predicate for submonoids and subgroups. If we do add FG later, then IsMulFG should be the simp-normal form (so that FG top becomes IsMulFG M).

[tb65536]

The point is, the file currently has four predicates which are all say the same thing and can be simultaneously generated to IsMulFG. I think we want this generalization independent of a general FG predicate for subojects (which only handles two of the four predicates in this file).