mathlib3

99608cc6 - feat(group_theory/sub{monoid,group}, linear_algebra/basic): add `supr_induction` for `submonoid`, `add_submonoid`, `subgroup`, `add_subgroup`, and `submodule` (#11556)

feat(group_theory/sub{monoid,group}, linear_algebra/basic): add `supr_induction` for `submonoid`, `add_submonoid`, `subgroup`, `add_subgroup`, and `submodule` (#11556) This also adds dependent versions, which match the style of the dependent versions of `submodule.span_induction` and `submonoid.closure_induction` in #11555. Primarily it's the group and module versions that are useful here, as they remove the inv and smul obligations that would appear if using `closure_induction` or `span_induction`.