diff --git a/.github/workflows/add_label_from_comment.yml b/.github/workflows/add_label_from_comment.yml
deleted file mode 100644
index 30a161785134f..0000000000000
--- a/.github/workflows/add_label_from_comment.yml
+++ /dev/null
@@ -1,60 +0,0 @@
-name: Add "ready-to-merge" and "delegated" label from comment
-
-on:
-  issue_comment:
-    types: [created]
-
-jobs:
-  add_ready_to_merge_label:
-    name: Add ready-to-merge label
-    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
-    runs-on: ubuntu-latest
-    steps:
-      - id: user_permission
-        uses: actions-cool/check-user-permission@v2
-        with:
-          require: 'admin'
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
-        uses: octokit/request-action@v2.x
-        id: add_label
-        name: Add label
-        with:
-          route: POST /repos/:repository/issues/:issue_number/labels
-          repository: ${{ github.repository }}
-          issue_number: ${{ github.event.issue.number }}
-          labels: '["ready-to-merge"]'
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
-        id: remove_labels
-        name: Remove "awaiting-author"
-        # we use curl rather than octokit/request-action so that the job won't fail
-        # (and send an annoying email) if the labels don't exist
-        run: |
-          curl --request DELETE \
-            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-author \
-            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
-
-  add_delegated_label:
-    name: Add delegated label
-    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
-    runs-on: ubuntu-latest
-    steps:
-      - id: user_permission
-        uses: actions-cool/check-user-permission@v2
-        with:
-          require: 'admin'
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
-        uses: octokit/request-action@v2.x
-        id: add_label
-        name: Add label
-        with:
-          route: POST /repos/:repository/issues/:issue_number/labels
-          repository: ${{ github.repository }}
-          issue_number: ${{ github.event.issue.number }}
-          labels: '["delegated"]'
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.github/workflows/add_label_from_review.yml b/.github/workflows/add_label_from_review.yml
deleted file mode 100644
index 9406866ff214e..0000000000000
--- a/.github/workflows/add_label_from_review.yml
+++ /dev/null
@@ -1,62 +0,0 @@
-name: Add "ready-to-merge" and "delegated" label from PR review
-
-on:
-  pull_request_review:
-    types: [submitted]
-
-jobs:
-  add_ready_to_merge_label:
-    name: Add ready-to-merge label
-    if: (startsWith(github.event.review.body, 'bors r+') || contains(toJSON(github.event.review.body), '\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\nbors merge'))
-    runs-on: ubuntu-latest
-    steps:
-      - id: user_permission
-        uses: actions-cool/check-user-permission@v2
-        with:
-          require: 'write'
-          token: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
-        uses: octokit/request-action@v2.x
-        id: add_label
-        name: Add label
-        with:
-          route: POST /repos/:repository/issues/:issue_number/labels
-          repository: ${{ github.repository }}
-          issue_number: ${{ github.event.pull_request.number }}
-          labels: '["ready-to-merge"]'
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
-        id: remove_labels
-        name: Remove "awaiting-author"
-        # we use curl rather than octokit/request-action so that the job won't fail
-        # (and send an annoying email) if the labels don't exist
-        run: |
-          curl --request DELETE \
-            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-author \
-            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
-
-  add_delegated_label:
-    name: Add delegated label
-    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\nbors d'))
-    runs-on: ubuntu-latest
-    steps:
-      - id: user_permission
-        uses: actions-cool/check-user-permission@v2
-        with:
-          require: 'write'
-          token: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
-        uses: octokit/request-action@v2.x
-        id: add_label
-        name: Add label
-        with:
-          route: POST /repos/:repository/issues/:issue_number/labels
-          repository: ${{ github.repository }}
-          issue_number: ${{ github.event.pull_request.number }}
-          labels: '["delegated"]'
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
diff --git a/.github/workflows/add_label_from_review_comment.yml b/.github/workflows/add_label_from_review_comment.yml
deleted file mode 100644
index da8b643fb0ee4..0000000000000
--- a/.github/workflows/add_label_from_review_comment.yml
+++ /dev/null
@@ -1,62 +0,0 @@
-name: Add "ready-to-merge" and "delegated" label from PR review comment
-
-on:
-  pull_request_review_comment:
-    types: [created]
-
-jobs:
-  add_ready_to_merge_label:
-    name: Add ready-to-merge label
-    if: (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
-    runs-on: ubuntu-latest
-    steps:
-      - id: user_permission
-        uses: actions-cool/check-user-permission@v2
-        with:
-          require: 'write'
-          token: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
-        uses: octokit/request-action@v2.x
-        id: add_label
-        name: Add label
-        with:
-          route: POST /repos/:repository/issues/:issue_number/labels
-          repository: ${{ github.repository }}
-          issue_number: ${{ github.event.pull_request.number }}
-          labels: '["ready-to-merge"]'
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
-        id: remove_labels
-        name: Remove "awaiting-author"
-        # we use curl rather than octokit/request-action so that the job won't fail
-        # (and send an annoying email) if the labels don't exist
-        run: |
-          curl --request DELETE \
-            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-author \
-            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
-
-  add_delegated_label:
-    name: Add delegated label
-    if: (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
-    runs-on: ubuntu-latest
-    steps:
-      - id: user_permission
-        uses: actions-cool/check-user-permission@v2
-        with:
-          require: 'write'
-          token: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
-        uses: octokit/request-action@v2.x
-        id: add_label
-        name: Add label
-        with:
-          route: POST /repos/:repository/issues/:issue_number/labels
-          repository: ${{ github.repository }}
-          issue_number: ${{ github.event.pull_request.number }}
-          labels: '["delegated"]'
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
diff --git a/.github/workflows/discover-lean-pr-testing.yml b/.github/workflows/discover-lean-pr-testing.yml
index 3c414d9e99689..69e46265bbbc0 100644
--- a/.github/workflows/discover-lean-pr-testing.yml
+++ b/.github/workflows/discover-lean-pr-testing.yml
@@ -24,6 +24,23 @@ jobs:
         git config --global user.name "github-actions"
         git config --global user.email "github-actions@github.com"
 
+    - name: Determine old and new lean-toolchain
+      id: determine-toolchains
+      run: |
+        # `lean-toolchain` contains a string of the form "leanprover/lean4:nightly-2024-11-20"
+        # We grab the part after the ":"
+        NEW=$(cut -f2 -d: lean-toolchain)
+
+        # Find the commit hash of the previous change to `lean-toolchain`
+        PREV_COMMIT=$(git log -2 --format=format:%H -- lean-toolchain | tail -1)
+
+        # Get the contents of `lean-toolchain` from the previous commit
+        # The "./" in front of the path is important for `git show`
+        OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)
+
+        echo "new=$NEW" >> "$GITHUB_OUTPUT"
+        echo "old=$OLD" >> "$GITHUB_OUTPUT"
+
     - name: Clone lean4 repository and get PRs
       id: get-prs
       run: |
@@ -38,14 +55,15 @@ jobs:
         # Navigate to the cloned repository
         cd lean4-nightly || exit 1
 
-        # Shallow fetch of the last two tags
-        LAST_TWO_TAGS=$(git ls-remote --tags | grep nightly | tail -2 | cut -f2)
-        OLD=$(echo "$LAST_TWO_TAGS" | head -1)
-        NEW=$(echo "$LAST_TWO_TAGS" | tail -1)
+        # Use the OLD and NEW toolchains determined in the previous step
+        OLD="${{ steps.determine-toolchains.outputs.old }}"
+        NEW="${{ steps.determine-toolchains.outputs.new }}"
+
+        # Fetch the $OLD tag
         git fetch --depth=1 origin tag "$OLD" --no-tags
-        # Fetch the latest 100 commits prior to the $NEW tag.
-        # This should cover the terrain between $OLD and $NEW while still being a speedy download.
-        git fetch --depth=100 origin tag "$NEW" --no-tags
+        # Fetch the $NEW tag.
+        # This will only fetch commits newer than previously fetched commits (ie $OLD)
+        git fetch origin tag "$NEW" --no-tags
 
         PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/')
         
diff --git a/.github/workflows/maintainer_bors.yml b/.github/workflows/maintainer_bors.yml
index 073477b4fa324..8b06a44a1b926 100644
--- a/.github/workflows/maintainer_bors.yml
+++ b/.github/workflows/maintainer_bors.yml
@@ -19,13 +19,8 @@ jobs:
     # both set simultaneously: depending on the event that triggers the PR, usually only one is set
     env:
       AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
-      PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
       COMMENT_EVENT: ${{ github.event.comment.body }}
       COMMENT_REVIEW: ${{ github.event.review.body }}
-      PR_TITLE_ISSUE: ${{ github.event.issue.title }}
-      PR_TITLE_PR: ${{ github.event.pull_request.title }}
-      PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
-      EVENT_NAME: ${{ github.event_name }}
     name: Add ready-to-merge or delegated label
     runs-on: ubuntu-latest
     steps:
@@ -43,8 +38,7 @@ jobs:
 
           printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
           printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
-          printf $'PR_NUMBER: \'%s\'\n' "${PR_NUMBER}"
-          printf $'OTHER_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
+          printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
           printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
 
           printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
@@ -64,9 +58,6 @@ jobs:
         uses: actions-cool/check-user-permission@v2
         with:
           require: 'admin'
-          # review(_comment) use
-          # require: 'write'
-          # token: ${{ secrets.TRIAGE_TOKEN }}
 
       - name: Add ready-to-merge or delegated label
         id: add_label
@@ -75,13 +66,12 @@ jobs:
             steps.merge_or_delegate.outputs.bot == 'true' ) }}
         uses: octokit/request-action@v2.x
         with:
-          # check is this ok? was /repos/:repository/issues/:issue_number/labels
           route: POST /repos/:repository/issues/:issue_number/labels
           repository: ${{ github.repository }}
           issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
           labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }} # comment uses ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
 
       - if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
@@ -92,6 +82,6 @@ jobs:
         # (and send an annoying email) if the labels don't exist
         run: |
           curl --request DELETE \
-            --url "https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels/awaiting-author" \
+            --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
             --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
             # comment uses ${{ secrets.GITHUB_TOKEN }}
diff --git a/Archive/Imo/Imo2008Q2.lean b/Archive/Imo/Imo2008Q2.lean
index 0340c3f70479b..41687a4a977a0 100644
--- a/Archive/Imo/Imo2008Q2.lean
+++ b/Archive/Imo/Imo2008Q2.lean
@@ -106,12 +106,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
             exact ⟨rfl, rfl, rfl⟩
         · have hg : -z = g (x, y, z) := rfl
           rw [hg, hz_def]; ring
-      have h₂ : q < t * (t + 1) := by
-        calc
-          q < q + 1 := by linarith
-          _ ≤ t := le_max_left (q + 1) 1
-          _ ≤ t + t ^ 2 := by linarith [sq_nonneg t]
-          _ = t * (t + 1) := by ring
+      have h₂ : q < t * (t + 1) := by linarith [sq_nonneg t, le_max_left (q + 1) 1]
       exact ⟨h₁, h₂⟩
     have hK_inf : Set.Infinite K := by intro h; apply hK_not_bdd; exact Set.Finite.bddAbove h
     exact hK_inf.of_image g
diff --git a/Archive/Imo/Imo2013Q5.lean b/Archive/Imo/Imo2013Q5.lean
index 225e64ae35b02..eb996b73633a4 100644
--- a/Archive/Imo/Imo2013Q5.lean
+++ b/Archive/Imo/Imo2013Q5.lean
@@ -65,15 +65,9 @@ theorem le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
   refine le_of_all_pow_lt_succ hx ?_ h
   by_contra! hy'' : y ≤ 1
   -- Then there exists y' such that 0 < y ≤ 1 < y' < x.
-  let y' := (x + 1) / 2
-  have h_y'_lt_x : y' < x :=
-    calc
-      (x + 1) / 2 < x * 2 / 2 := by linarith
-      _ = x := by field_simp
-  have h1_lt_y' : 1 < y' :=
-    calc
-      1 = 1 * 2 / 2 := by field_simp
-      _ < (x + 1) / 2 := by linarith
+  have h_y'_lt_x : (x + 1) / 2 < x := by linarith
+  have h1_lt_y' : 1 < (x + 1) / 2 := by linarith
+  set y' := (x + 1) / 2
   have h_y_lt_y' : y < y' := by linarith
   have hh : ∀ n, 0 < n → x ^ n - 1 < y' ^ n := by
     intro n hn
diff --git a/Mathlib.lean b/Mathlib.lean
index 5922aa04576e9..139b1e81351a5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -298,6 +298,9 @@ import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Group.Subgroup.Finite
+import Mathlib.Algebra.Group.Subgroup.Ker
+import Mathlib.Algebra.Group.Subgroup.Lattice
+import Mathlib.Algebra.Group.Subgroup.Map
 import Mathlib.Algebra.Group.Subgroup.MulOpposite
 import Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
 import Mathlib.Algebra.Group.Subgroup.Order
diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
index 7dc43d9c08e9a..b8a261ee2098e 100644
--- a/Mathlib/Algebra/AddConstMap/Basic.lean
+++ b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -28,6 +28,8 @@ We use parameters `a` and `b` instead of `1` to accommodate for two use cases:
   including orientation-reversing maps.
 -/
 
+assert_not_exists Finset
+
 open Function Set
 
 /-- A bundled map `f : G → H` such that `f (x + a) = f x + b` for all `x`.
diff --git a/Mathlib/Algebra/AddConstMap/Equiv.lean b/Mathlib/Algebra/AddConstMap/Equiv.lean
index ee4c37b716812..28779a4f482cc 100644
--- a/Mathlib/Algebra/AddConstMap/Equiv.lean
+++ b/Mathlib/Algebra/AddConstMap/Equiv.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.AddConstMap.Basic
 import Mathlib.GroupTheory.Perm.Basic
+
 /-!
 # Equivalences conjugating `(· + a)` to `(· + b)`
 
@@ -14,6 +15,8 @@ to be the type of equivalences such that `∀ x, f (x + a) = f x + b`.
 We also define the corresponding typeclass and prove some basic properties.
 -/
 
+assert_not_exists Finset
+
 open Function
 open scoped AddConstMap
 
diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean b/Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean
index 44e1c3d71de18..f269dd69e8670 100644
--- a/Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean
+++ b/Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean
@@ -58,6 +58,7 @@ with a head term (`seq1`) is then transformed to a generalized continued fractio
 numerics, number theory, approximations, fractions
 -/
 
+assert_not_exists Finset
 
 namespace GenContFract
 
diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
index d732ff25b6a7a..0b971d4795163 100644
--- a/Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
+++ b/Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
@@ -37,6 +37,7 @@ of three sections:
   parts.
 -/
 
+assert_not_exists Finset
 
 namespace GenContFract
 
diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index 6fc988e05de4b..c6b11e2b701e3 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -5,20 +5,13 @@ Authors: Kexing Ying
 -/
 import Mathlib.Algebra.Group.Conj
 import Mathlib.Algebra.Group.Pi.Lemmas
-import Mathlib.Algebra.Group.Submonoid.Operations
-import Mathlib.Algebra.Group.Subgroup.Defs
-import Mathlib.Data.Set.Image
-import Mathlib.Tactic.ApplyFun
+import Mathlib.Algebra.Group.Subgroup.Ker
 
 /-!
-# Subgroups
+# Basic results on subgroups
 
-We prove subgroups of a group form a complete lattice, and results about images and preimages of
-subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.
-
-There are also theorems about the subgroups generated by an element or a subset of a group,
-defined both inductively and as the infimum of the set of subgroups containing a given
-element/subset.
+We prove basic results on the definitions of subgroups. The bundled subgroups use bundled monoid
+homomorphisms.
 
 Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
 
@@ -40,31 +33,9 @@ Notation used here:
 
 Definitions in the file:
 
-* `CompleteLattice (Subgroup G)` : the subgroups of `G` form a complete lattice
-
-* `Subgroup.closure k` : the minimal subgroup that includes the set `k`
-
-* `Subgroup.subtype` : the natural group homomorphism from a subgroup of group `G` to `G`
-
-* `Subgroup.gi` : `closure` forms a Galois insertion with the coercion to set
-
-* `Subgroup.comap H f` : the preimage of a subgroup `H` along the group homomorphism `f` is also a
-  subgroup
-
-* `Subgroup.map f H` : the image of a subgroup `H` along the group homomorphism `f` is also a
-  subgroup
-
 * `Subgroup.prod H K` : the product of subgroups `H`, `K` of groups `G`, `N` respectively, `H × K`
   is a subgroup of `G × N`
 
-* `MonoidHom.range f` : the range of the group homomorphism `f` is a subgroup
-
-* `MonoidHom.ker f` : the kernel of a group homomorphism `f` is the subgroup of elements `x : G`
-  such that `f x = 1`
-
-* `MonoidHom.eqLocus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
-  `f x = g x` form a subgroup of `G`
-
 ## Implementation notes
 
 Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
@@ -96,43 +67,6 @@ theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
 
 end SubgroupClass
 
-/-!
-### Conversion to/from `Additive`/`Multiplicative`
--/
-
-
-section mul_add
-
-/-- Subgroups of a group `G` are isomorphic to additive subgroups of `Additive G`. -/
-@[simps!]
-def Subgroup.toAddSubgroup : Subgroup G ≃o AddSubgroup (Additive G) where
-  toFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
-  invFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
-  left_inv x := by cases x; rfl
-  right_inv x := by cases x; rfl
-  map_rel_iff' := Iff.rfl
-
-/-- Additive subgroup of an additive group `Additive G` are isomorphic to subgroup of `G`. -/
-abbrev AddSubgroup.toSubgroup' : AddSubgroup (Additive G) ≃o Subgroup G :=
-  Subgroup.toAddSubgroup.symm
-
-/-- Additive subgroups of an additive group `A` are isomorphic to subgroups of `Multiplicative A`.
--/
-@[simps!]
-def AddSubgroup.toSubgroup : AddSubgroup A ≃o Subgroup (Multiplicative A) where
-  toFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
-  invFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
-  left_inv x := by cases x; rfl
-  right_inv x := by cases x; rfl
-  map_rel_iff' := Iff.rfl
-
-/-- Subgroups of an additive group `Multiplicative A` are isomorphic to additive subgroups of `A`.
--/
-abbrev Subgroup.toAddSubgroup' : Subgroup (Multiplicative A) ≃o AddSubgroup A :=
-  AddSubgroup.toSubgroup.symm
-
-end mul_add
-
 namespace Subgroup
 
 variable (H K : Subgroup G)
@@ -141,691 +75,11 @@ variable (H K : Subgroup G)
 protected theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
   div_mem_comm_iff
 
-/-- The subgroup `G` of the group `G`. -/
-@[to_additive "The `AddSubgroup G` of the `AddGroup G`."]
-instance : Top (Subgroup G) :=
-  ⟨{ (⊤ : Submonoid G) with inv_mem' := fun _ => Set.mem_univ _ }⟩
-
-/-- The top subgroup is isomorphic to the group.
-
-This is the group version of `Submonoid.topEquiv`. -/
-@[to_additive (attr := simps!)
-      "The top additive subgroup is isomorphic to the additive group.
-
-      This is the additive group version of `AddSubmonoid.topEquiv`."]
-def topEquiv : (⊤ : Subgroup G) ≃* G :=
-  Submonoid.topEquiv
-
-/-- The trivial subgroup `{1}` of a group `G`. -/
-@[to_additive "The trivial `AddSubgroup` `{0}` of an `AddGroup` `G`."]
-instance : Bot (Subgroup G) :=
-  ⟨{ (⊥ : Submonoid G) with inv_mem' := by simp}⟩
-
-@[to_additive]
-instance : Inhabited (Subgroup G) :=
-  ⟨⊥⟩
-
-@[to_additive (attr := simp)]
-theorem mem_bot {x : G} : x ∈ (⊥ : Subgroup G) ↔ x = 1 :=
-  Iff.rfl
-
-@[to_additive (attr := simp)]
-theorem mem_top (x : G) : x ∈ (⊤ : Subgroup G) :=
-  Set.mem_univ x
-
-@[to_additive (attr := simp)]
-theorem coe_top : ((⊤ : Subgroup G) : Set G) = Set.univ :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem coe_bot : ((⊥ : Subgroup G) : Set G) = {1} :=
-  rfl
-
-@[to_additive]
-instance : Unique (⊥ : Subgroup G) :=
-  ⟨⟨1⟩, fun g => Subtype.ext g.2⟩
-
-@[to_additive (attr := simp)]
-theorem top_toSubmonoid : (⊤ : Subgroup G).toSubmonoid = ⊤ :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem bot_toSubmonoid : (⊥ : Subgroup G).toSubmonoid = ⊥ :=
-  rfl
-
-@[to_additive]
-theorem eq_bot_iff_forall : H = ⊥ ↔ ∀ x ∈ H, x = (1 : G) :=
-  toSubmonoid_injective.eq_iff.symm.trans <| Submonoid.eq_bot_iff_forall _
-
-@[to_additive]
-theorem eq_bot_of_subsingleton [Subsingleton H] : H = ⊥ := by
-  rw [Subgroup.eq_bot_iff_forall]
-  intro y hy
-  rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_eq_univ {H : Subgroup G} : (H : Set G) = Set.univ ↔ H = ⊤ :=
-  (SetLike.ext'_iff.trans (by rfl)).symm
-
-@[to_additive]
-theorem coe_eq_singleton {H : Subgroup G} : (∃ g : G, (H : Set G) = {g}) ↔ H = ⊥ :=
-  ⟨fun ⟨g, hg⟩ =>
-    haveI : Subsingleton (H : Set G) := by
-      rw [hg]
-      infer_instance
-    H.eq_bot_of_subsingleton,
-    fun h => ⟨1, SetLike.ext'_iff.mp h⟩⟩
-
-@[to_additive]
-theorem nontrivial_iff_exists_ne_one (H : Subgroup G) : Nontrivial H ↔ ∃ x ∈ H, x ≠ (1 : G) := by
-  rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
-  simp
-
-@[to_additive]
-theorem exists_ne_one_of_nontrivial (H : Subgroup G) [Nontrivial H] :
-    ∃ x ∈ H, x ≠ 1 := by
-  rwa [← Subgroup.nontrivial_iff_exists_ne_one]
-
-@[to_additive]
-theorem nontrivial_iff_ne_bot (H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥ := by
-  rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
-  simp only [ne_eq, not_forall, exists_prop]
-
-/-- A subgroup is either the trivial subgroup or nontrivial. -/
-@[to_additive "A subgroup is either the trivial subgroup or nontrivial."]
-theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H := by
-  have := nontrivial_iff_ne_bot H
-  tauto
-
-/-- A subgroup is either the trivial subgroup or contains a non-identity element. -/
-@[to_additive "A subgroup is either the trivial subgroup or contains a nonzero element."]
-theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1 : G) := by
-  convert H.bot_or_nontrivial
-  rw [nontrivial_iff_exists_ne_one]
-
-@[to_additive]
-lemma ne_bot_iff_exists_ne_one {H : Subgroup G} : H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1 := by
-  rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
-  simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]
-
-/-- The inf of two subgroups is their intersection. -/
-@[to_additive "The inf of two `AddSubgroup`s is their intersection."]
-instance : Min (Subgroup G) :=
-  ⟨fun H₁ H₂ =>
-    { H₁.toSubmonoid ⊓ H₂.toSubmonoid with
-      inv_mem' := fun ⟨hx, hx'⟩ => ⟨H₁.inv_mem hx, H₂.inv_mem hx'⟩ }⟩
-
-@[to_additive (attr := simp)]
-theorem coe_inf (p p' : Subgroup G) : ((p ⊓ p' : Subgroup G) : Set G) = (p : Set G) ∩ p' :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mem_inf {p p' : Subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
-  Iff.rfl
-
-@[to_additive]
-instance : InfSet (Subgroup G) :=
-  ⟨fun s =>
-    { (⨅ S ∈ s, Subgroup.toSubmonoid S).copy (⋂ S ∈ s, ↑S) (by simp) with
-      inv_mem' := fun {x} hx =>
-        Set.mem_biInter fun i h => i.inv_mem (by apply Set.mem_iInter₂.1 hx i h) }⟩
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_sInf (H : Set (Subgroup G)) : ((sInf H : Subgroup G) : Set G) = ⋂ s ∈ H, ↑s :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mem_sInf {S : Set (Subgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
-  Set.mem_iInter₂
-
-@[to_additive]
-theorem mem_iInf {ι : Sort*} {S : ι → Subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
-  simp only [iInf, mem_sInf, Set.forall_mem_range]
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_iInf {ι : Sort*} {S : ι → Subgroup G} : (↑(⨅ i, S i) : Set G) = ⋂ i, S i := by
-  simp only [iInf, coe_sInf, Set.biInter_range]
-
-/-- Subgroups of a group form a complete lattice. -/
-@[to_additive "The `AddSubgroup`s of an `AddGroup` form a complete lattice."]
-instance : CompleteLattice (Subgroup G) :=
-  { completeLatticeOfInf (Subgroup G) fun _s =>
-      IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
-    bot := ⊥
-    bot_le := fun S _x hx => (mem_bot.1 hx).symm ▸ S.one_mem
-    top := ⊤
-    le_top := fun _S x _hx => mem_top x
-    inf := (· ⊓ ·)
-    le_inf := fun _a _b _c ha hb _x hx => ⟨ha hx, hb hx⟩
-    inf_le_left := fun _a _b _x => And.left
-    inf_le_right := fun _a _b _x => And.right }
-
-@[to_additive]
-theorem mem_sup_left {S T : Subgroup G} : ∀ {x : G}, x ∈ S → x ∈ S ⊔ T :=
-  have : S ≤ S ⊔ T := le_sup_left; fun h ↦ this h
-
-@[to_additive]
-theorem mem_sup_right {S T : Subgroup G} : ∀ {x : G}, x ∈ T → x ∈ S ⊔ T :=
-  have : T ≤ S ⊔ T := le_sup_right; fun h ↦ this h
-
-@[to_additive]
-theorem mul_mem_sup {S T : Subgroup G} {x y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
-  (S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)
-
-@[to_additive]
-theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Subgroup G} (i : ι) :
-    ∀ {x : G}, x ∈ S i → x ∈ iSup S :=
-  have : S i ≤ iSup S := le_iSup _ _; fun h ↦ this h
-
-@[to_additive]
-theorem mem_sSup_of_mem {S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) :
-    ∀ {x : G}, x ∈ s → x ∈ sSup S :=
-  have : s ≤ sSup S := le_sSup hs; fun h ↦ this h
-
-@[to_additive (attr := simp)]
-theorem subsingleton_iff : Subsingleton (Subgroup G) ↔ Subsingleton G :=
-  ⟨fun _ =>
-    ⟨fun x y =>
-      have : ∀ i : G, i = 1 := fun i =>
-        mem_bot.mp <| Subsingleton.elim (⊤ : Subgroup G) ⊥ ▸ mem_top i
-      (this x).trans (this y).symm⟩,
-    fun _ => ⟨fun x y => Subgroup.ext fun i => Subsingleton.elim 1 i ▸ by simp [Subgroup.one_mem]⟩⟩
-
-@[to_additive (attr := simp)]
-theorem nontrivial_iff : Nontrivial (Subgroup G) ↔ Nontrivial G :=
-  not_iff_not.mp
-    ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans
-      not_nontrivial_iff_subsingleton.symm)
-
-@[to_additive]
-instance [Subsingleton G] : Unique (Subgroup G) :=
-  ⟨⟨⊥⟩, fun a => @Subsingleton.elim _ (subsingleton_iff.mpr ‹_›) a _⟩
-
-@[to_additive]
-instance [Nontrivial G] : Nontrivial (Subgroup G) :=
-  nontrivial_iff.mpr ‹_›
-
-@[to_additive]
-theorem eq_top_iff' : H = ⊤ ↔ ∀ x : G, x ∈ H :=
-  eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩
-
-/-- The `Subgroup` generated by a set. -/
-@[to_additive "The `AddSubgroup` generated by a set"]
-def closure (k : Set G) : Subgroup G :=
-  sInf { K | k ⊆ K }
-
 variable {k : Set G}
 
-@[to_additive]
-theorem mem_closure {x : G} : x ∈ closure k ↔ ∀ K : Subgroup G, k ⊆ K → x ∈ K :=
-  mem_sInf
-
-/-- The subgroup generated by a set includes the set. -/
-@[to_additive (attr := simp, aesop safe 20 apply (rule_sets := [SetLike]))
-  "The `AddSubgroup` generated by a set includes the set."]
-theorem subset_closure : k ⊆ closure k := fun _ hx => mem_closure.2 fun _ hK => hK hx
-
-@[to_additive]
-theorem not_mem_of_not_mem_closure {P : G} (hP : P ∉ closure k) : P ∉ k := fun h =>
-  hP (subset_closure h)
-
 open Set
 
-/-- A subgroup `K` includes `closure k` if and only if it includes `k`. -/
-@[to_additive (attr := simp)
-  "An additive subgroup `K` includes `closure k` if and only if it includes `k`"]
-theorem closure_le : closure k ≤ K ↔ k ⊆ K :=
-  ⟨Subset.trans subset_closure, fun h => sInf_le h⟩
-
-@[to_additive]
-theorem closure_eq_of_le (h₁ : k ⊆ K) (h₂ : K ≤ closure k) : closure k = K :=
-  le_antisymm ((closure_le <| K).2 h₁) h₂
-
-/-- An induction principle for closure membership. If `p` holds for `1` and all elements of `k`, and
-is preserved under multiplication and inverse, then `p` holds for all elements of the closure
-of `k`.
-
-See also `Subgroup.closure_induction_left` and `Subgroup.closure_induction_right` for versions that
-only require showing `p` is preserved by multiplication by elements in `k`. -/
-@[to_additive (attr := elab_as_elim)
-      "An induction principle for additive closure membership. If `p`
-      holds for `0` and all elements of `k`, and is preserved under addition and inverses, then `p`
-      holds for all elements of the additive closure of `k`.
-
-      See also `AddSubgroup.closure_induction_left` and `AddSubgroup.closure_induction_left` for
-      versions that only require showing `p` is preserved by addition by elements in `k`."]
-theorem closure_induction {p : (g : G) → g ∈ closure k → Prop}
-    (mem : ∀ x (hx : x ∈ k), p x (subset_closure hx)) (one : p 1 (one_mem _))
-    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
-    (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx :=
-  let K : Subgroup G :=
-    { carrier := { x | ∃ hx, p x hx }
-      mul_mem' := fun ⟨_, ha⟩ ⟨_, hb⟩ ↦ ⟨_, mul _ _ _ _ ha hb⟩
-      one_mem' := ⟨_, one⟩
-      inv_mem' := fun ⟨_, hb⟩ ↦ ⟨_, inv _ _ hb⟩ }
-  closure_le (K := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
-
-@[deprecated closure_induction (since := "2024-10-10")]
-alias closure_induction' := closure_induction
-
-/-- An induction principle for closure membership for predicates with two arguments. -/
-@[to_additive (attr := elab_as_elim)
-      "An induction principle for additive closure membership, for
-      predicates with two arguments."]
-theorem closure_induction₂ {p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop}
-    (mem : ∀ (x) (y) (hx : x ∈ k) (hy : y ∈ k), p x y (subset_closure hx) (subset_closure hy))
-    (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
-    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
-    (mul_right : ∀ y z x hy hz hx, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
-    (inv_left : ∀ x y hx hy, p x y hx hy → p x⁻¹ y (inv_mem hx) hy)
-    (inv_right : ∀ x y hx hy, p x y hx hy → p x y⁻¹ hx (inv_mem hy))
-    {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy := by
-  induction hy using closure_induction with
-  | mem z hz => induction hx using closure_induction with
-    | mem _ h => exact mem _ _ h hz
-    | one => exact one_left _ (subset_closure hz)
-    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
-    | inv _ _ h => exact inv_left _ _ _ _ h
-  | one => exact one_right x hx
-  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
-  | inv _ _ h => exact inv_right _ _ _ _ h
-
-@[to_additive (attr := simp)]
-theorem closure_closure_coe_preimage {k : Set G} : closure (((↑) : closure k → G) ⁻¹' k) = ⊤ :=
-  eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
-    closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem)
-      (fun _ _ ↦ inv_mem) hx'
-
-variable (G)
-
-/-- `closure` forms a Galois insertion with the coercion to set. -/
-@[to_additive "`closure` forms a Galois insertion with the coercion to set."]
-protected def gi : GaloisInsertion (@closure G _) (↑) where
-  choice s _ := closure s
-  gc s t := @closure_le _ _ t s
-  le_l_u _s := subset_closure
-  choice_eq _s _h := rfl
-
-variable {G}
-
-/-- Subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
-then `closure h ≤ closure k`. -/
-@[to_additive
-      "Additive subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
-      then `closure h ≤ closure k`"]
-theorem closure_mono ⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k :=
-  (Subgroup.gi G).gc.monotone_l h'
-
-/-- Closure of a subgroup `K` equals `K`. -/
-@[to_additive (attr := simp) "Additive closure of an additive subgroup `K` equals `K`"]
-theorem closure_eq : closure (K : Set G) = K :=
-  (Subgroup.gi G).l_u_eq K
-
-@[to_additive (attr := simp)]
-theorem closure_empty : closure (∅ : Set G) = ⊥ :=
-  (Subgroup.gi G).gc.l_bot
-
-@[to_additive (attr := simp)]
-theorem closure_univ : closure (univ : Set G) = ⊤ :=
-  @coe_top G _ ▸ closure_eq ⊤
-
-@[to_additive]
-theorem closure_union (s t : Set G) : closure (s ∪ t) = closure s ⊔ closure t :=
-  (Subgroup.gi G).gc.l_sup
-
-@[to_additive]
-theorem sup_eq_closure (H H' : Subgroup G) : H ⊔ H' = closure ((H : Set G) ∪ (H' : Set G)) := by
-  simp_rw [closure_union, closure_eq]
-
-@[to_additive]
-theorem closure_iUnion {ι} (s : ι → Set G) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
-  (Subgroup.gi G).gc.l_iSup
-
-@[to_additive (attr := simp)]
-theorem closure_eq_bot_iff : closure k = ⊥ ↔ k ⊆ {1} := le_bot_iff.symm.trans <| closure_le _
-
-@[to_additive]
-theorem iSup_eq_closure {ι : Sort*} (p : ι → Subgroup G) :
-    ⨆ i, p i = closure (⋃ i, (p i : Set G)) := by simp_rw [closure_iUnion, closure_eq]
-
-/-- The subgroup generated by an element of a group equals the set of integer number powers of
-    the element. -/
-@[to_additive
-      "The `AddSubgroup` generated by an element of an `AddGroup` equals the set of
-      natural number multiples of the element."]
-theorem mem_closure_singleton {x y : G} : y ∈ closure ({x} : Set G) ↔ ∃ n : ℤ, x ^ n = y := by
-  refine
-    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
-      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
-  · intro y hy
-    rw [eq_of_mem_singleton hy]
-    exact ⟨1, zpow_one x⟩
-  · exact ⟨0, zpow_zero x⟩
-  · rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
-    exact ⟨n + m, zpow_add x n m⟩
-  rintro _ _ ⟨n, rfl⟩
-  exact ⟨-n, zpow_neg x n⟩
-
-@[to_additive]
-theorem closure_singleton_one : closure ({1} : Set G) = ⊥ := by
-  simp [eq_bot_iff_forall, mem_closure_singleton]
-
-@[to_additive (attr := simp)]
-lemma mem_closure_singleton_self (x : G) : x ∈ closure ({x} : Set G) := by
-  simpa [-subset_closure] using subset_closure (k := {x})
-
-@[to_additive]
-theorem le_closure_toSubmonoid (S : Set G) : Submonoid.closure S ≤ (closure S).toSubmonoid :=
-  Submonoid.closure_le.2 subset_closure
-
-@[to_additive]
-theorem closure_eq_top_of_mclosure_eq_top {S : Set G} (h : Submonoid.closure S = ⊤) :
-    closure S = ⊤ :=
-  (eq_top_iff' _).2 fun _ => le_closure_toSubmonoid _ <| h.symm ▸ trivial
-
-@[to_additive]
-theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (· ≤ ·) K)
-    {x : G} : x ∈ (iSup K : Subgroup G) ↔ ∃ i, x ∈ K i := by
-  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup K i hi⟩
-  suffices x ∈ closure (⋃ i, (K i : Set G)) → ∃ i, x ∈ K i by
-    simpa only [closure_iUnion, closure_eq (K _)] using this
-  refine fun hx ↦ closure_induction (fun _ ↦ mem_iUnion.1) ?_ ?_ ?_ hx
-  · exact hι.elim fun i ↦ ⟨i, (K i).one_mem⟩
-  · rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩
-    rcases hK i j with ⟨k, hki, hkj⟩
-    exact ⟨k, mul_mem (hki hi) (hkj hj)⟩
-  · rintro _ _ ⟨i, hi⟩
-    exact ⟨i, inv_mem hi⟩
-
-@[to_additive]
-theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (· ≤ ·) S) :
-    ((⨆ i, S i : Subgroup G) : Set G) = ⋃ i, S i :=
-  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]
-
-@[to_additive]
-theorem mem_sSup_of_directedOn {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (· ≤ ·) K)
-    {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s := by
-  haveI : Nonempty K := Kne.to_subtype
-  simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, Subtype.coe_mk,
-    exists_prop]
-
-variable {N : Type*} [Group N] {P : Type*} [Group P]
-
-/-- The preimage of a subgroup along a monoid homomorphism is a subgroup. -/
-@[to_additive
-      "The preimage of an `AddSubgroup` along an `AddMonoid` homomorphism
-      is an `AddSubgroup`."]
-def comap {N : Type*} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G :=
-  { H.toSubmonoid.comap f with
-    carrier := f ⁻¹' H
-    inv_mem' := fun {a} ha => show f a⁻¹ ∈ H by rw [f.map_inv]; exact H.inv_mem ha }
-
-@[to_additive (attr := simp)]
-theorem coe_comap (K : Subgroup N) (f : G →* N) : (K.comap f : Set G) = f ⁻¹' K :=
-  rfl
-
-@[simp]
-theorem toAddSubgroup_comap {G₂ : Type*} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
-    s.toAddSubgroup.comap (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.comap f) := rfl
-
-@[simp]
-theorem _root_.AddSubgroup.toSubgroup_comap {A A₂ : Type*} [AddGroup A] [AddGroup A₂]
-    (f : A →+ A₂) (s : AddSubgroup A₂) :
-    s.toSubgroup.comap (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.comap f) := rfl
-
-@[to_additive (attr := simp)]
-theorem mem_comap {K : Subgroup N} {f : G →* N} {x : G} : x ∈ K.comap f ↔ f x ∈ K :=
-  Iff.rfl
-
-@[to_additive]
-theorem comap_mono {f : G →* N} {K K' : Subgroup N} : K ≤ K' → comap f K ≤ comap f K' :=
-  preimage_mono
-
-@[to_additive]
-theorem comap_comap (K : Subgroup P) (g : N →* P) (f : G →* N) :
-    (K.comap g).comap f = K.comap (g.comp f) :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem comap_id (K : Subgroup N) : K.comap (MonoidHom.id _) = K := by
-  ext
-  rfl
-
-/-- The image of a subgroup along a monoid homomorphism is a subgroup. -/
-@[to_additive
-      "The image of an `AddSubgroup` along an `AddMonoid` homomorphism
-      is an `AddSubgroup`."]
-def map (f : G →* N) (H : Subgroup G) : Subgroup N :=
-  { H.toSubmonoid.map f with
-    carrier := f '' H
-    inv_mem' := by
-      rintro _ ⟨x, hx, rfl⟩
-      exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩ }
-
-@[to_additive (attr := simp)]
-theorem coe_map (f : G →* N) (K : Subgroup G) : (K.map f : Set N) = f '' K :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mem_map {f : G →* N} {K : Subgroup G} {y : N} : y ∈ K.map f ↔ ∃ x ∈ K, f x = y := Iff.rfl
-
-@[to_additive]
-theorem mem_map_of_mem (f : G →* N) {K : Subgroup G} {x : G} (hx : x ∈ K) : f x ∈ K.map f :=
-  mem_image_of_mem f hx
-
-@[to_additive]
-theorem apply_coe_mem_map (f : G →* N) (K : Subgroup G) (x : K) : f x ∈ K.map f :=
-  mem_map_of_mem f x.prop
-
-@[to_additive]
-theorem map_mono {f : G →* N} {K K' : Subgroup G} : K ≤ K' → map f K ≤ map f K' :=
-  image_subset _
-
-@[to_additive (attr := simp)]
-theorem map_id : K.map (MonoidHom.id G) = K :=
-  SetLike.coe_injective <| image_id _
-
-@[to_additive]
-theorem map_map (g : N →* P) (f : G →* N) : (K.map f).map g = K.map (g.comp f) :=
-  SetLike.coe_injective <| image_image _ _ _
-
-@[to_additive (attr := simp)]
-theorem map_one_eq_bot : K.map (1 : G →* N) = ⊥ :=
-  eq_bot_iff.mpr <| by
-    rintro x ⟨y, _, rfl⟩
-    simp
-
-@[to_additive]
-theorem mem_map_equiv {f : G ≃* N} {K : Subgroup G} {x : N} :
-    x ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K := by
-  erw [@Set.mem_image_equiv _ _ (↑K) f.toEquiv x]; rfl
-
--- The simpNF linter says that the LHS can be simplified via `Subgroup.mem_map`.
--- However this is a higher priority lemma.
--- https://github.com/leanprover/std4/issues/207
-@[to_additive (attr := simp 1100, nolint simpNF)]
-theorem mem_map_iff_mem {f : G →* N} (hf : Function.Injective f) {K : Subgroup G} {x : G} :
-    f x ∈ K.map f ↔ x ∈ K :=
-  hf.mem_set_image
-
-@[to_additive]
-theorem map_equiv_eq_comap_symm' (f : G ≃* N) (K : Subgroup G) :
-    K.map f.toMonoidHom = K.comap f.symm.toMonoidHom :=
-  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)
-
-@[to_additive]
-theorem map_equiv_eq_comap_symm (f : G ≃* N) (K : Subgroup G) :
-    K.map f = K.comap (G := N) f.symm :=
-  map_equiv_eq_comap_symm' _ _
-
-@[to_additive]
-theorem comap_equiv_eq_map_symm (f : N ≃* G) (K : Subgroup G) :
-    K.comap (G := N) f = K.map f.symm :=
-  (map_equiv_eq_comap_symm f.symm K).symm
-
-@[to_additive]
-theorem comap_equiv_eq_map_symm' (f : N ≃* G) (K : Subgroup G) :
-    K.comap f.toMonoidHom = K.map f.symm.toMonoidHom :=
-  (map_equiv_eq_comap_symm f.symm K).symm
-
-@[to_additive]
-theorem map_symm_eq_iff_map_eq {H : Subgroup N} {e : G ≃* N} :
-    H.map ↑e.symm = K ↔ K.map ↑e = H := by
-  constructor <;> rintro rfl
-  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
-      MulEquiv.coe_monoidHom_refl, map_id]
-  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
-      MulEquiv.coe_monoidHom_refl, map_id]
-
-@[to_additive]
-theorem map_le_iff_le_comap {f : G →* N} {K : Subgroup G} {H : Subgroup N} :
-    K.map f ≤ H ↔ K ≤ H.comap f :=
-  image_subset_iff
-
-@[to_additive]
-theorem gc_map_comap (f : G →* N) : GaloisConnection (map f) (comap f) := fun _ _ =>
-  map_le_iff_le_comap
-
-@[to_additive]
-theorem map_sup (H K : Subgroup G) (f : G →* N) : (H ⊔ K).map f = H.map f ⊔ K.map f :=
-  (gc_map_comap f).l_sup
-
-@[to_additive]
-theorem map_iSup {ι : Sort*} (f : G →* N) (s : ι → Subgroup G) :
-    (iSup s).map f = ⨆ i, (s i).map f :=
-  (gc_map_comap f).l_iSup
-
-@[to_additive]
-theorem map_inf (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
-    (H ⊓ K).map f = H.map f ⊓ K.map f := SetLike.coe_injective (Set.image_inter hf)
-
-@[to_additive]
-theorem map_iInf {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f)
-    (s : ι → Subgroup G) : (iInf s).map f = ⨅ i, (s i).map f := by
-  apply SetLike.coe_injective
-  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)
-
-@[to_additive]
-theorem comap_sup_comap_le (H K : Subgroup N) (f : G →* N) :
-    comap f H ⊔ comap f K ≤ comap f (H ⊔ K) :=
-  Monotone.le_map_sup (fun _ _ => comap_mono) H K
-
-@[to_additive]
-theorem iSup_comap_le {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) :
-    ⨆ i, (s i).comap f ≤ (iSup s).comap f :=
-  Monotone.le_map_iSup fun _ _ => comap_mono
-
-@[to_additive]
-theorem comap_inf (H K : Subgroup N) (f : G →* N) : (H ⊓ K).comap f = H.comap f ⊓ K.comap f :=
-  (gc_map_comap f).u_inf
-
-@[to_additive]
-theorem comap_iInf {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) :
-    (iInf s).comap f = ⨅ i, (s i).comap f :=
-  (gc_map_comap f).u_iInf
-
-@[to_additive]
-theorem map_inf_le (H K : Subgroup G) (f : G →* N) : map f (H ⊓ K) ≤ map f H ⊓ map f K :=
-  le_inf (map_mono inf_le_left) (map_mono inf_le_right)
-
-@[to_additive]
-theorem map_inf_eq (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
-    map f (H ⊓ K) = map f H ⊓ map f K := by
-  rw [← SetLike.coe_set_eq]
-  simp [Set.image_inter hf]
-
-@[to_additive (attr := simp)]
-theorem map_bot (f : G →* N) : (⊥ : Subgroup G).map f = ⊥ :=
-  (gc_map_comap f).l_bot
-
-@[to_additive (attr := simp)]
-theorem map_top_of_surjective (f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤ := by
-  rw [eq_top_iff]
-  intro x _
-  obtain ⟨y, hy⟩ := h x
-  exact ⟨y, trivial, hy⟩
-
-@[to_additive (attr := simp)]
-theorem comap_top (f : G →* N) : (⊤ : Subgroup N).comap f = ⊤ :=
-  (gc_map_comap f).u_top
-
-/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`. -/
-@[to_additive "For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`."]
-def subgroupOf (H K : Subgroup G) : Subgroup K :=
-  H.comap K.subtype
-
-/-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`. -/
-@[to_additive (attr := simps) "If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`."]
-def subgroupOfEquivOfLe {G : Type*} [Group G] {H K : Subgroup G} (h : H ≤ K) :
-    H.subgroupOf K ≃* H where
-  toFun g := ⟨g.1, g.2⟩
-  invFun g := ⟨⟨g.1, h g.2⟩, g.2⟩
-  left_inv _g := Subtype.ext (Subtype.ext rfl)
-  right_inv _g := Subtype.ext rfl
-  map_mul' _g _h := rfl
-
-@[to_additive (attr := simp)]
-theorem comap_subtype (H K : Subgroup G) : H.comap K.subtype = H.subgroupOf K :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem comap_inclusion_subgroupOf {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) :
-    (H.subgroupOf K₂).comap (inclusion h) = H.subgroupOf K₁ :=
-  rfl
-
-@[to_additive]
-theorem coe_subgroupOf (H K : Subgroup G) : (H.subgroupOf K : Set K) = K.subtype ⁻¹' H :=
-  rfl
-
-@[to_additive]
-theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h : G) ∈ H :=
-  Iff.rfl
-
--- TODO(kmill): use `K ⊓ H` order for RHS to match `Subtype.image_preimage_coe`
-@[to_additive (attr := simp)]
-theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K :=
-  SetLike.ext' <| by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm
-
-@[to_additive (attr := simp)]
-theorem bot_subgroupOf : (⊥ : Subgroup G).subgroupOf H = ⊥ :=
-  Eq.symm (Subgroup.ext fun _g => Subtype.ext_iff)
-
-@[to_additive (attr := simp)]
-theorem top_subgroupOf : (⊤ : Subgroup G).subgroupOf H = ⊤ :=
-  rfl
-
-@[to_additive]
-theorem subgroupOf_bot_eq_bot : H.subgroupOf ⊥ = ⊥ :=
-  Subsingleton.elim _ _
-
-@[to_additive]
-theorem subgroupOf_bot_eq_top : H.subgroupOf ⊥ = ⊤ :=
-  Subsingleton.elim _ _
-
-@[to_additive (attr := simp)]
-theorem subgroupOf_self : H.subgroupOf H = ⊤ :=
-  top_unique fun g _hg => g.2
-
-@[to_additive (attr := simp)]
-theorem subgroupOf_inj {H₁ H₂ K : Subgroup G} :
-    H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K := by
-  simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall
-
-@[to_additive (attr := simp)]
-theorem inf_subgroupOf_right (H K : Subgroup G) : (H ⊓ K).subgroupOf K = H.subgroupOf K :=
-  subgroupOf_inj.2 (inf_right_idem _ _)
-
-@[to_additive (attr := simp)]
-theorem inf_subgroupOf_left (H K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K := by
-  rw [inf_comm, inf_subgroupOf_right]
-
-@[to_additive (attr := simp)]
-theorem subgroupOf_eq_bot {H K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K := by
-  rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]
-
-@[to_additive (attr := simp)]
-theorem subgroupOf_eq_top {H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H := by
-  rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]
+variable {N : Type*} [Group N] {P : Type*} [Group P]
 
 /-- Given `Subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`. -/
 @[to_additive prod
@@ -1143,66 +397,8 @@ variable (H)
 
 end Normalizer
 
-@[to_additive]
-instance map_isCommutative (f : G →* G') [H.IsCommutative] : (H.map f).IsCommutative :=
-  ⟨⟨by
-      rintro ⟨-, a, ha, rfl⟩ ⟨-, b, hb, rfl⟩
-      rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← map_mul, ← map_mul]
-      exact congr_arg f (Subtype.ext_iff.mp (mul_comm (⟨a, ha⟩ : H) ⟨b, hb⟩))⟩⟩
-
-@[to_additive]
-theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCommutative] :
-    (H.comap f).IsCommutative :=
-  ⟨⟨fun a b =>
-      Subtype.ext
-        (by
-          have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)
-          rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul,
-            hf.eq_iff] at this)⟩⟩
-
-@[to_additive]
-instance subgroupOf_isCommutative [H.IsCommutative] : (H.subgroupOf K).IsCommutative :=
-  H.comap_injective_isCommutative Subtype.coe_injective
-
 end Subgroup
 
-namespace MulEquiv
-variable {H : Type*} [Group H]
-
-/--
-An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
-defined by sending subgroups to their inverse images.
-
-See also `MulEquiv.mapSubgroup` which maps subgroups to their forward images.
--/
-@[simps]
-def comapSubgroup (f : G ≃* H) : Subgroup H ≃o Subgroup G where
-  toFun := Subgroup.comap f
-  invFun := Subgroup.comap f.symm
-  left_inv sg := by simp [Subgroup.comap_comap]
-  right_inv sh := by simp [Subgroup.comap_comap]
-  map_rel_iff' {sg1 sg2} :=
-    ⟨fun h => by simpa [Subgroup.comap_comap] using
-      Subgroup.comap_mono (f := (f.symm : H →* G)) h, Subgroup.comap_mono⟩
-
-/--
-An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
-defined by sending subgroups to their forward images.
-
-See also `MulEquiv.comapSubgroup` which maps subgroups to their inverse images.
--/
-@[simps]
-def mapSubgroup {H : Type*} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup H where
-  toFun := Subgroup.map f
-  invFun := Subgroup.map f.symm
-  left_inv sg := by simp [Subgroup.map_map]
-  right_inv sh := by simp [Subgroup.map_map]
-  map_rel_iff' {sg1 sg2} :=
-    ⟨fun h => by simpa [Subgroup.map_map] using
-      Subgroup.map_mono (f := (f.symm : H →* G)) h, Subgroup.map_mono⟩
-
-end MulEquiv
-
 namespace Group
 
 variable {s : Set G}
@@ -1352,243 +548,10 @@ variable {N : Type*} {P : Type*} [Group N] [Group P] (K : Subgroup G)
 
 open Subgroup
 
-/-- The range of a monoid homomorphism from a group is a subgroup. -/
-@[to_additive "The range of an `AddMonoidHom` from an `AddGroup` is an `AddSubgroup`."]
-def range (f : G →* N) : Subgroup N :=
-  Subgroup.copy ((⊤ : Subgroup G).map f) (Set.range f) (by simp [Set.ext_iff])
-
-@[to_additive (attr := simp)]
-theorem coe_range (f : G →* N) : (f.range : Set N) = Set.range f :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mem_range {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y :=
-  Iff.rfl
-
-@[to_additive]
-theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp
-
-@[to_additive]
-instance range_isCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) :
-    f.range.IsCommutative :=
-  range_eq_map f ▸ Subgroup.map_isCommutative ⊤ f
-
-@[to_additive (attr := simp)]
-theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
-  simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
-    exists_prop, forall_const]
-
-/-- The canonical surjective group homomorphism `G →* f(G)` induced by a group
-homomorphism `G →* N`. -/
-@[to_additive
-      "The canonical surjective `AddGroup` homomorphism `G →+ f(G)` induced by a group
-      homomorphism `G →+ N`."]
-def rangeRestrict (f : G →* N) : G →* f.range :=
-  codRestrict f _ fun x => ⟨x, rfl⟩
-
-@[to_additive (attr := simp)]
-theorem coe_rangeRestrict (f : G →* N) (g : G) : (f.rangeRestrict g : N) = f g :=
-  rfl
-
-@[to_additive]
-theorem coe_comp_rangeRestrict (f : G →* N) :
-    ((↑) : f.range → N) ∘ (⇑f.rangeRestrict : G → f.range) = f :=
-  rfl
-
-@[to_additive]
-theorem subtype_comp_rangeRestrict (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f :=
-  ext <| f.coe_rangeRestrict
-
-@[to_additive]
-theorem rangeRestrict_surjective (f : G →* N) : Function.Surjective f.rangeRestrict :=
-  fun ⟨_, g, rfl⟩ => ⟨g, rfl⟩
-
-@[to_additive (attr := simp)]
-lemma rangeRestrict_injective_iff {f : G →* N} : Injective f.rangeRestrict ↔ Injective f := by
-  convert Set.injective_codRestrict _
-
-@[to_additive]
-theorem map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range := by
-  rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f
-
-@[to_additive]
-theorem range_eq_top {N} [Group N] {f : G →* N} :
-    f.range = (⊤ : Subgroup N) ↔ Function.Surjective f :=
-  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ
-
-@[deprecated (since := "2024-11-11")] alias range_top_iff_surjective := range_eq_top
-
-/-- The range of a surjective monoid homomorphism is the whole of the codomain. -/
-@[to_additive (attr := simp)
-  "The range of a surjective `AddMonoid` homomorphism is the whole of the codomain."]
-theorem range_eq_top_of_surjective {N} [Group N] (f : G →* N) (hf : Function.Surjective f) :
-    f.range = (⊤ : Subgroup N) :=
-  range_eq_top.2 hf
-
-@[deprecated (since := "2024-11-11")] alias range_top_of_surjective := range_eq_top_of_surjective
-
-@[to_additive (attr := simp)]
-theorem range_one : (1 : G →* N).range = ⊥ :=
-  SetLike.ext fun x => by simpa using @comm _ (· = ·) _ 1 x
-
-@[to_additive (attr := simp)]
-theorem _root_.Subgroup.subtype_range (H : Subgroup G) : H.subtype.range = H := by
-  rw [range_eq_map, ← SetLike.coe_set_eq, coe_map, Subgroup.coeSubtype]
-  ext
-  simp
-
-@[to_additive (attr := simp)]
-theorem _root_.Subgroup.inclusion_range {H K : Subgroup G} (h_le : H ≤ K) :
-    (inclusion h_le).range = H.subgroupOf K :=
-  Subgroup.ext fun g => Set.ext_iff.mp (Set.range_inclusion h_le) g
-
-@[to_additive]
-theorem subgroupOf_range_eq_of_le {G₁ G₂ : Type*} [Group G₁] [Group G₂] {K : Subgroup G₂}
-    (f : G₁ →* G₂) (h : f.range ≤ K) :
-    f.range.subgroupOf K = (f.codRestrict K fun x => h ⟨x, rfl⟩).range := by
-  ext k
-  refine exists_congr ?_
-  simp [Subtype.ext_iff]
-
-@[simp]
-theorem coe_toAdditive_range (f : G →* G') :
-    (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range := rfl
-
-@[simp]
-theorem coe_toMultiplicative_range {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
-    (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range := rfl
-
-/-- Computable alternative to `MonoidHom.ofInjective`. -/
-@[to_additive "Computable alternative to `AddMonoidHom.ofInjective`."]
-def ofLeftInverse {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) : G ≃* f.range :=
-  { f.rangeRestrict with
-    toFun := f.rangeRestrict
-    invFun := g ∘ f.range.subtype
-    left_inv := h
-    right_inv := by
-      rintro ⟨x, y, rfl⟩
-      apply Subtype.ext
-      rw [coe_rangeRestrict, Function.comp_apply, Subgroup.coeSubtype, Subtype.coe_mk, h] }
-
-@[to_additive (attr := simp)]
-theorem ofLeftInverse_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : G) :
-    ↑(ofLeftInverse h x) = f x :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem ofLeftInverse_symm_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f)
-    (x : f.range) : (ofLeftInverse h).symm x = g x :=
-  rfl
-
-/-- The range of an injective group homomorphism is isomorphic to its domain. -/
-@[to_additive "The range of an injective additive group homomorphism is isomorphic to its
-domain."]
-noncomputable def ofInjective {f : G →* N} (hf : Function.Injective f) : G ≃* f.range :=
-  MulEquiv.ofBijective (f.codRestrict f.range fun x => ⟨x, rfl⟩)
-    ⟨fun _ _ h => hf (Subtype.ext_iff.mp h), by
-      rintro ⟨x, y, rfl⟩
-      exact ⟨y, rfl⟩⟩
-
-@[to_additive]
-theorem ofInjective_apply {f : G →* N} (hf : Function.Injective f) {x : G} :
-    ↑(ofInjective hf x) = f x :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem apply_ofInjective_symm {f : G →* N} (hf : Function.Injective f) (x : f.range) :
-    f ((ofInjective hf).symm x) = x :=
-  Subtype.ext_iff.1 <| (ofInjective hf).apply_symm_apply x
-
 section Ker
 
 variable {M : Type*} [MulOneClass M]
 
-/-- The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
-`f x = 1` -/
-@[to_additive
-      "The additive kernel of an `AddMonoid` homomorphism is the `AddSubgroup` of elements
-      such that `f x = 0`"]
-def ker (f : G →* M) : Subgroup G :=
-  { MonoidHom.mker f with
-    inv_mem' := fun {x} (hx : f x = 1) =>
-      calc
-        f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
-        _ = 1 := by rw [← map_mul, mul_inv_cancel, map_one] }
-
-@[to_additive (attr := simp)]
-theorem mem_ker {f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1 :=
-  Iff.rfl
-
-@[to_additive]
-theorem div_mem_ker_iff (f : G →* N) {x y : G} : x / y ∈ ker f ↔ f x = f y := by
-  rw [mem_ker, map_div, div_eq_one]
-
-@[to_additive]
-theorem coe_ker (f : G →* M) : (f.ker : Set G) = (f : G → M) ⁻¹' {1} :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem ker_toHomUnits {M} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker := by
-  ext x
-  simp [mem_ker, Units.ext_iff]
-
-@[to_additive]
-theorem eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker := by
-  constructor <;> intro h
-  · rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]
-
-@[to_additive]
-instance decidableMemKer [DecidableEq M] (f : G →* M) : DecidablePred (· ∈ f.ker) := fun x =>
-  decidable_of_iff (f x = 1) f.mem_ker
-
-@[to_additive]
-theorem comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem comap_bot (f : G →* N) : (⊥ : Subgroup N).comap f = f.ker :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem ker_restrict (f : G →* N) : (f.restrict K).ker = f.ker.subgroupOf K :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem ker_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S)
-    (h : ∀ x, f x ∈ s) : (f.codRestrict s h).ker = f.ker :=
-  SetLike.ext fun _x => Subtype.ext_iff
-
-@[to_additive (attr := simp)]
-theorem ker_rangeRestrict (f : G →* N) : ker (rangeRestrict f) = ker f :=
-  ker_codRestrict _ _ _
-
-@[to_additive (attr := simp)]
-theorem ker_one : (1 : G →* M).ker = ⊤ :=
-  SetLike.ext fun _x => eq_self_iff_true _
-
-@[to_additive (attr := simp)]
-theorem ker_id : (MonoidHom.id G).ker = ⊥ :=
-  rfl
-
-@[to_additive]
-theorem ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ Function.Injective f :=
-  ⟨fun h x y hxy => by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy, fun h =>
-    bot_unique fun _ hx => h (hx.trans f.map_one.symm)⟩
-
-@[to_additive (attr := simp)]
-theorem _root_.Subgroup.ker_subtype (H : Subgroup G) : H.subtype.ker = ⊥ :=
-  H.subtype.ker_eq_bot_iff.mpr Subtype.coe_injective
-
-@[to_additive (attr := simp)]
-theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥ :=
-  (inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)
-
-@[to_additive]
-theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
-    (f.prod g).ker = f.ker ⊓ g.ker :=
-  SetLike.ext fun _ => Prod.mk_eq_one
-
 @[to_additive]
 theorem prodMap_comap_prod {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N)
     (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') :
@@ -1600,74 +563,14 @@ theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →*
     (prodMap f g).ker = f.ker.prod g.ker := by
   rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
 
-@[to_additive]
-theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
-  ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y⟩
-
-@[to_additive]
-instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
-  ⟨fun x hx y => by
-    rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩
-
 @[to_additive (attr := simp)]
 lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
 
 @[to_additive (attr := simp)]
 lemma ker_snd : ker (snd G G') = .prod ⊤ ⊥ := SetLike.ext fun _ => (iff_of_eq (true_and _)).symm
 
-@[simp]
-theorem coe_toAdditive_ker (f : G →* G') :
-    (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker := rfl
-
-@[simp]
-theorem coe_toMultiplicative_ker {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
-    (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker := rfl
-
 end Ker
 
-section EqLocus
-
-variable {M : Type*} [Monoid M]
-
-/-- The subgroup of elements `x : G` such that `f x = g x` -/
-@[to_additive "The additive subgroup of elements `x : G` such that `f x = g x`"]
-def eqLocus (f g : G →* M) : Subgroup G :=
-  { eqLocusM f g with inv_mem' := eq_on_inv f g }
-
-@[to_additive (attr := simp)]
-theorem eqLocus_same (f : G →* N) : f.eqLocus f = ⊤ :=
-  SetLike.ext fun _ => eq_self_iff_true _
-
-/-- If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure. -/
-@[to_additive
-      "If two monoid homomorphisms are equal on a set, then they are equal on its subgroup
-      closure."]
-theorem eqOn_closure {f g : G →* M} {s : Set G} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
-  show closure s ≤ f.eqLocus g from (closure_le _).2 h
-
-@[to_additive]
-theorem eq_of_eqOn_top {f g : G →* M} (h : Set.EqOn f g (⊤ : Subgroup G)) : f = g :=
-  ext fun _x => h trivial
-
-@[to_additive]
-theorem eq_of_eqOn_dense {s : Set G} (hs : closure s = ⊤) {f g : G →* M} (h : s.EqOn f g) : f = g :=
-  eq_of_eqOn_top <| hs ▸ eqOn_closure h
-
-end EqLocus
-
-@[to_additive]
-theorem closure_preimage_le (f : G →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
-  (closure_le _).2 fun x hx => by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx
-
-/-- The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup
-generated by the image of the set. -/
-@[to_additive
-      "The image under an `AddMonoid` hom of the `AddSubgroup` generated by a set equals
-      the `AddSubgroup` generated by the image of the set."]
-theorem map_closure (f : G →* N) (s : Set G) : (closure s).map f = closure (f '' s) :=
-  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subgroup.gi N).gc (Subgroup.gi G).gc
-    fun _ ↦ rfl
-
 end MonoidHom
 
 namespace Subgroup
@@ -1681,14 +584,6 @@ theorem Normal.map {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function
     normalizer_eq_top.2 h]
   exact le_normalizer_map _
 
-@[to_additive]
-theorem map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
-  (gc_map_comap f).l_eq_bot
-
-@[to_additive]
-theorem map_eq_bot_iff_of_injective {f : G →* N} (hf : Function.Injective f) :
-    H.map f = ⊥ ↔ H = ⊥ := by rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]
-
 end Subgroup
 
 namespace Subgroup
@@ -1697,166 +592,6 @@ open MonoidHom
 
 variable {N : Type*} [Group N] (f : G →* N)
 
-@[to_additive]
-theorem map_le_range (H : Subgroup G) : map f H ≤ f.range :=
-  (range_eq_map f).symm ▸ map_mono le_top
-
-@[to_additive]
-theorem map_subtype_le {H : Subgroup G} (K : Subgroup H) : K.map H.subtype ≤ H :=
-  (K.map_le_range H.subtype).trans (le_of_eq H.subtype_range)
-
-@[to_additive]
-theorem ker_le_comap (H : Subgroup N) : f.ker ≤ comap f H :=
-  comap_bot f ▸ comap_mono bot_le
-
-@[to_additive]
-theorem map_comap_le (H : Subgroup N) : map f (comap f H) ≤ H :=
-  (gc_map_comap f).l_u_le _
-
-@[to_additive]
-theorem le_comap_map (H : Subgroup G) : H ≤ comap f (map f H) :=
-  (gc_map_comap f).le_u_l _
-
-@[to_additive]
-theorem map_comap_eq (H : Subgroup N) : map f (comap f H) = f.range ⊓ H :=
-  SetLike.ext' <| by
-    rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-
-@[to_additive]
-theorem comap_map_eq (H : Subgroup G) : comap f (map f H) = H ⊔ f.ker := by
-  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
-  intro x hx; simp only [exists_prop, mem_map, mem_comap] at hx
-  rcases hx with ⟨y, hy, hy'⟩
-  rw [← mul_inv_cancel_left y x]
-  exact mul_mem_sup hy (by simp [mem_ker, hy'])
-
-@[to_additive]
-theorem map_comap_eq_self {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) :
-    map f (comap f H) = H := by
-  rwa [map_comap_eq, inf_eq_right]
-
-@[to_additive]
-theorem map_comap_eq_self_of_surjective {f : G →* N} (h : Function.Surjective f) (H : Subgroup N) :
-    map f (comap f H) = H :=
-  map_comap_eq_self (range_eq_top.2 h ▸ le_top)
-
-@[to_additive]
-theorem comap_le_comap_of_le_range {f : G →* N} {K L : Subgroup N} (hf : K ≤ f.range) :
-    K.comap f ≤ L.comap f ↔ K ≤ L :=
-  ⟨(map_comap_eq_self hf).ge.trans ∘ map_le_iff_le_comap.mpr, comap_mono⟩
-
-@[to_additive]
-theorem comap_le_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
-    K.comap f ≤ L.comap f ↔ K ≤ L :=
-  comap_le_comap_of_le_range (range_eq_top.2 hf ▸ le_top)
-
-@[to_additive]
-theorem comap_lt_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
-    K.comap f < L.comap f ↔ K < L := by simp_rw [lt_iff_le_not_le, comap_le_comap_of_surjective hf]
-
-@[to_additive]
-theorem comap_injective {f : G →* N} (h : Function.Surjective f) : Function.Injective (comap f) :=
-  fun K L => by simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]
-
-@[to_additive]
-theorem comap_map_eq_self {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) :
-    comap f (map f H) = H := by
-  rwa [comap_map_eq, sup_eq_left]
-
-@[to_additive]
-theorem comap_map_eq_self_of_injective {f : G →* N} (h : Function.Injective f) (H : Subgroup G) :
-    comap f (map f H) = H :=
-  comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le)
-
-@[to_additive]
-theorem map_le_map_iff {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K ⊔ f.ker := by
-  rw [map_le_iff_le_comap, comap_map_eq]
-
-@[to_additive]
-theorem map_le_map_iff' {f : G →* N} {H K : Subgroup G} :
-    H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker := by
-  simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]
-
-@[to_additive]
-theorem map_eq_map_iff {f : G →* N} {H K : Subgroup G} :
-    H.map f = K.map f ↔ H ⊔ f.ker = K ⊔ f.ker := by simp only [le_antisymm_iff, map_le_map_iff']
-
-@[to_additive]
-theorem map_eq_range_iff {f : G →* N} {H : Subgroup G} :
-    H.map f = f.range ↔ Codisjoint H f.ker := by
-  rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]
-
-@[to_additive]
-theorem map_le_map_iff_of_injective {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} :
-    H.map f ≤ K.map f ↔ H ≤ K := by rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]
-
-@[to_additive (attr := simp)]
-theorem map_subtype_le_map_subtype {G' : Subgroup G} {H K : Subgroup G'} :
-    H.map G'.subtype ≤ K.map G'.subtype ↔ H ≤ K :=
-  map_le_map_iff_of_injective <| by apply Subtype.coe_injective
-
-@[to_additive]
-theorem map_injective {f : G →* N} (h : Function.Injective f) : Function.Injective (map f) :=
-  Function.LeftInverse.injective <| comap_map_eq_self_of_injective h
-
-@[to_additive]
-theorem map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f)
-    (hr : Function.RightInverse g f) (H : Subgroup G) : map f H = comap g H :=
-  SetLike.ext' <| by rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]
-
-/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`. -/
-@[to_additive "Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`."]
-theorem map_injective_of_ker_le {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K)
-    (hf : map f H = map f K) : H = K := by
-  apply_fun comap f at hf
-  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf
-
-@[to_additive]
-theorem closure_preimage_eq_top (s : Set G) : closure ((closure s).subtype ⁻¹' s) = ⊤ := by
-  apply map_injective (closure s).subtype_injective
-  rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, subtype_range,
-    Set.image_preimage_eq_of_subset]
-  rw [coeSubtype, Subtype.range_coe_subtype]
-  exact subset_closure
-
-@[to_additive]
-theorem comap_sup_eq_of_le_range {H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) :
-    comap f H ⊔ comap f K = comap f (H ⊔ K) :=
-  map_injective_of_ker_le f ((ker_le_comap f H).trans le_sup_left) (ker_le_comap f (H ⊔ K))
-    (by
-      rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
-        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)])
-
-@[to_additive]
-theorem comap_sup_eq (H K : Subgroup N) (hf : Function.Surjective f) :
-    comap f H ⊔ comap f K = comap f (H ⊔ K) :=
-  comap_sup_eq_of_le_range f (range_eq_top.2 hf ▸ le_top) (range_eq_top.2 hf ▸ le_top)
-
-@[to_additive]
-theorem sup_subgroupOf_eq {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) :
-    H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L :=
-  comap_sup_eq_of_le_range L.subtype (hH.trans L.subtype_range.ge) (hK.trans L.subtype_range.ge)
-
-@[to_additive]
-theorem codisjoint_subgroupOf_sup (H K : Subgroup G) :
-    Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)) := by
-  rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self]
-  exacts [le_sup_left, le_sup_right]
-
-/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
-use `MulEquiv.subgroupMap` for better definitional equalities. -/
-@[to_additive
-      "An additive subgroup is isomorphic to its image under an injective function. If you
-      have an isomorphism, use `AddEquiv.addSubgroupMap` for better definitional equalities."]
-noncomputable def equivMapOfInjective (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
-    H ≃* H.map f :=
-  { Equiv.Set.image f H hf with map_mul' := fun _ _ => Subtype.ext (f.map_mul _ _) }
-
-@[to_additive (attr := simp)]
-theorem coe_equivMapOfInjective_apply (H : Subgroup G) (f : G →* N) (hf : Function.Injective f)
-    (h : H) : (equivMapOfInjective H f hf h : N) = f h :=
-  rfl
-
 /-- The preimage of the normalizer is equal to the normalizer of the preimage of a surjective
   function. -/
 @[to_additive
@@ -2064,103 +799,6 @@ theorem Normal.of_map_subtype {K : Subgroup G} {L : Subgroup K}
 
 end Subgroup
 
-namespace MonoidHom
-
-/-- The `MonoidHom` from the preimage of a subgroup to itself. -/
-@[to_additive (attr := simps!) "the `AddMonoidHom` from the preimage of an
-additive subgroup to itself."]
-def subgroupComap (f : G →* G') (H' : Subgroup G') : H'.comap f →* H' :=
-  f.submonoidComap H'.toSubmonoid
-
-/-- The `MonoidHom` from a subgroup to its image. -/
-@[to_additive (attr := simps!) "the `AddMonoidHom` from an additive subgroup to its image"]
-def subgroupMap (f : G →* G') (H : Subgroup G) : H →* H.map f :=
-  f.submonoidMap H.toSubmonoid
-
-@[to_additive]
-theorem subgroupMap_surjective (f : G →* G') (H : Subgroup G) :
-    Function.Surjective (f.subgroupMap H) :=
-  f.submonoidMap_surjective H.toSubmonoid
-
-end MonoidHom
-
-namespace MulEquiv
-
-variable {H K : Subgroup G}
-
-/-- Makes the identity isomorphism from a proof two subgroups of a multiplicative
-    group are equal. -/
-@[to_additive
-      "Makes the identity additive isomorphism from a proof
-      two subgroups of an additive group are equal."]
-def subgroupCongr (h : H = K) : H ≃* K :=
-  { Equiv.setCongr <| congr_arg _ h with map_mul' := fun _ _ => rfl }
-
-@[to_additive (attr := simp)]
-lemma subgroupCongr_apply (h : H = K) (x) :
-    (MulEquiv.subgroupCongr h x : G) = x := rfl
-
-@[to_additive (attr := simp)]
-lemma subgroupCongr_symm_apply (h : H = K) (x) :
-    ((MulEquiv.subgroupCongr h).symm x : G) = x := rfl
-
-/-- A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
-use `Subgroup.equiv_map_of_injective`. -/
-@[to_additive
-      "An additive subgroup is isomorphic to its image under an isomorphism. If you only
-      have an injective map, use `AddSubgroup.equiv_map_of_injective`."]
-def subgroupMap (e : G ≃* G') (H : Subgroup G) : H ≃* H.map (e : G →* G') :=
-  MulEquiv.submonoidMap (e : G ≃* G') H.toSubmonoid
-
-@[to_additive (attr := simp)]
-theorem coe_subgroupMap_apply (e : G ≃* G') (H : Subgroup G) (g : H) :
-    ((subgroupMap e H g : H.map (e : G →* G')) : G') = e g :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem subgroupMap_symm_apply (e : G ≃* G') (H : Subgroup G) (g : H.map (e : G →* G')) :
-    (e.subgroupMap H).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩ :=
-  rfl
-
-end MulEquiv
-
-namespace Subgroup
-
-@[to_additive (attr := simp)]
-theorem equivMapOfInjective_coe_mulEquiv (H : Subgroup G) (e : G ≃* G') :
-    H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H := by
-  ext
-  rfl
-
-variable {C : Type*} [CommGroup C] {s t : Subgroup C} {x : C}
-
-@[to_additive]
-theorem mem_sup : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x :=
-  ⟨fun h => by
-    rw [sup_eq_closure] at h
-    refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
-    · rintro y (h | h)
-      · exact ⟨y, h, 1, t.one_mem, by simp⟩
-      · exact ⟨1, s.one_mem, y, h, by simp⟩
-    · exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
-    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
-      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
-    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
-      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩, by
-    rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz⟩
-
-@[to_additive]
-theorem mem_sup' : x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y : C) * z = x :=
-  mem_sup.trans <| by simp only [SetLike.exists, coe_mk, exists_prop]
-
-@[to_additive]
-theorem mem_closure_pair {x y z : C} :
-    z ∈ closure ({x, y} : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z := by
-  rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
-  simp_rw [mem_closure_singleton, exists_exists_eq_and]
-
-end Subgroup
-
 namespace Subgroup
 
 section SubgroupNormal
@@ -2208,15 +846,6 @@ theorem inf_subgroupOf_inf_normal_of_left {A' A : Subgroup G} (B : Subgroup G) (
 instance normal_inf_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal :=
   ⟨fun n hmem g => ⟨hH.conj_mem n hmem.1 g, hK.conj_mem n hmem.2 g⟩⟩
 
-@[to_additive]
-theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
-    (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B := by
-  refine
-    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
-      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
-  simp only [subgroupOf, map_comap_eq, map_sup, subtype_range]
-  rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
-
 @[to_additive]
 theorem SubgroupNormal.mem_comm {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal]
     {a b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H := by
@@ -2243,33 +872,6 @@ theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Nor
 
 end SubgroupNormal
 
-@[to_additive]
-theorem disjoint_def {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1 :=
-  disjoint_iff_inf_le.trans <| by simp only [Disjoint, SetLike.le_def, mem_inf, mem_bot, and_imp]
-
-@[to_additive]
-theorem disjoint_def' {H₁ H₂ : Subgroup G} :
-    Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1 :=
-  disjoint_def.trans ⟨fun h _x _y hx hy hxy ↦ h hx <| hxy.symm ▸ hy, fun h _x hx hx' ↦ h hx hx' rfl⟩
-
-@[to_additive]
-theorem disjoint_iff_mul_eq_one {H₁ H₂ : Subgroup G} :
-    Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1 :=
-  disjoint_def'.trans
-    ⟨fun h x y hx hy hxy =>
-      let hx1 : x = 1 := h hx (H₂.inv_mem hy) (eq_inv_iff_mul_eq_one.mpr hxy)
-      ⟨hx1, by simpa [hx1] using hxy⟩,
-      fun h _ _ hx hy hxy => (h hx (H₂.inv_mem hy) (mul_inv_eq_one.mpr hxy)).1⟩
-
-@[to_additive]
-theorem mul_injective_of_disjoint {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
-    Function.Injective (fun g => g.1 * g.2 : H₁ × H₂ → G) := by
-  intro x y hxy
-  rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
-  replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
-  rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
-    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
-
 end Subgroup
 
 namespace IsConj
@@ -2310,5 +912,3 @@ def noncenter (G : Type*) [Monoid G] : Set (ConjClasses G) :=
   g ∈ noncenter G ↔ g.carrier.Nontrivial := Iff.rfl
 
 end ConjClasses
-
-set_option linter.style.longFile 2500
diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean
new file mode 100644
index 0000000000000..8b9be58076933
--- /dev/null
+++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean
@@ -0,0 +1,507 @@
+/-
+Copyright (c) 2020 Kexing Ying. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kexing Ying
+-/
+import Mathlib.Algebra.Group.Subgroup.Map
+import Mathlib.Tactic.ApplyFun
+
+/-!
+# Kernel and range of group homomorphisms
+
+We define and prove results about the kernel and range of group homomorphisms.
+
+Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
+
+## Main definitions
+
+Notation used here:
+
+- `G N` are `Group`s
+
+- `x` is an element of type `G`
+
+- `f g : N →* G` are group homomorphisms
+
+Definitions in the file:
+
+* `MonoidHom.range f` : the range of the group homomorphism `f` is a subgroup
+
+* `MonoidHom.ker f` : the kernel of a group homomorphism `f` is the subgroup of elements `x : G`
+  such that `f x = 1`
+
+* `MonoidHom.eqLocus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
+  `f x = g x` form a subgroup of `G`
+
+## Implementation notes
+
+Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
+membership of a subgroup's underlying set.
+
+## Tags
+subgroup, subgroups
+-/
+
+assert_not_exists OrderedAddCommMonoid
+assert_not_exists Multiset
+assert_not_exists Ring
+
+open Function
+open scoped Int
+
+variable {G G' G'' : Type*} [Group G] [Group G'] [Group G'']
+variable {A : Type*} [AddGroup A]
+
+namespace MonoidHom
+
+variable {N : Type*} {P : Type*} [Group N] [Group P] (K : Subgroup G)
+
+open Subgroup
+
+/-- The range of a monoid homomorphism from a group is a subgroup. -/
+@[to_additive "The range of an `AddMonoidHom` from an `AddGroup` is an `AddSubgroup`."]
+def range (f : G →* N) : Subgroup N :=
+  Subgroup.copy ((⊤ : Subgroup G).map f) (Set.range f) (by simp [Set.ext_iff])
+
+@[to_additive (attr := simp)]
+theorem coe_range (f : G →* N) : (f.range : Set N) = Set.range f :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_range {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y :=
+  Iff.rfl
+
+@[to_additive]
+theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp
+
+@[to_additive]
+instance range_isCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) :
+    f.range.IsCommutative :=
+  range_eq_map f ▸ Subgroup.map_isCommutative ⊤ f
+
+@[to_additive (attr := simp)]
+theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
+  simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
+    exists_prop, forall_const]
+
+/-- The canonical surjective group homomorphism `G →* f(G)` induced by a group
+homomorphism `G →* N`. -/
+@[to_additive
+      "The canonical surjective `AddGroup` homomorphism `G →+ f(G)` induced by a group
+      homomorphism `G →+ N`."]
+def rangeRestrict (f : G →* N) : G →* f.range :=
+  codRestrict f _ fun x => ⟨x, rfl⟩
+
+@[to_additive (attr := simp)]
+theorem coe_rangeRestrict (f : G →* N) (g : G) : (f.rangeRestrict g : N) = f g :=
+  rfl
+
+@[to_additive]
+theorem coe_comp_rangeRestrict (f : G →* N) :
+    ((↑) : f.range → N) ∘ (⇑f.rangeRestrict : G → f.range) = f :=
+  rfl
+
+@[to_additive]
+theorem subtype_comp_rangeRestrict (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f :=
+  ext <| f.coe_rangeRestrict
+
+@[to_additive]
+theorem rangeRestrict_surjective (f : G →* N) : Function.Surjective f.rangeRestrict :=
+  fun ⟨_, g, rfl⟩ => ⟨g, rfl⟩
+
+@[to_additive (attr := simp)]
+lemma rangeRestrict_injective_iff {f : G →* N} : Injective f.rangeRestrict ↔ Injective f := by
+  convert Set.injective_codRestrict _
+
+@[to_additive]
+theorem map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range := by
+  rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f
+
+@[to_additive]
+theorem range_eq_top {N} [Group N] {f : G →* N} :
+    f.range = (⊤ : Subgroup N) ↔ Function.Surjective f :=
+  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ
+
+@[deprecated (since := "2024-11-11")] alias range_top_iff_surjective := range_eq_top
+
+/-- The range of a surjective monoid homomorphism is the whole of the codomain. -/
+@[to_additive (attr := simp)
+  "The range of a surjective `AddMonoid` homomorphism is the whole of the codomain."]
+theorem range_eq_top_of_surjective {N} [Group N] (f : G →* N) (hf : Function.Surjective f) :
+    f.range = (⊤ : Subgroup N) :=
+  range_eq_top.2 hf
+
+@[deprecated (since := "2024-11-11")] alias range_top_of_surjective := range_eq_top_of_surjective
+
+@[to_additive (attr := simp)]
+theorem range_one : (1 : G →* N).range = ⊥ :=
+  SetLike.ext fun x => by simpa using @comm _ (· = ·) _ 1 x
+
+@[to_additive (attr := simp)]
+theorem _root_.Subgroup.subtype_range (H : Subgroup G) : H.subtype.range = H := by
+  rw [range_eq_map, ← SetLike.coe_set_eq, coe_map, Subgroup.coeSubtype]
+  ext
+  simp
+
+@[to_additive (attr := simp)]
+theorem _root_.Subgroup.inclusion_range {H K : Subgroup G} (h_le : H ≤ K) :
+    (inclusion h_le).range = H.subgroupOf K :=
+  Subgroup.ext fun g => Set.ext_iff.mp (Set.range_inclusion h_le) g
+
+@[to_additive]
+theorem subgroupOf_range_eq_of_le {G₁ G₂ : Type*} [Group G₁] [Group G₂] {K : Subgroup G₂}
+    (f : G₁ →* G₂) (h : f.range ≤ K) :
+    f.range.subgroupOf K = (f.codRestrict K fun x => h ⟨x, rfl⟩).range := by
+  ext k
+  refine exists_congr ?_
+  simp [Subtype.ext_iff]
+
+/-- Computable alternative to `MonoidHom.ofInjective`. -/
+@[to_additive "Computable alternative to `AddMonoidHom.ofInjective`."]
+def ofLeftInverse {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) : G ≃* f.range :=
+  { f.rangeRestrict with
+    toFun := f.rangeRestrict
+    invFun := g ∘ f.range.subtype
+    left_inv := h
+    right_inv := by
+      rintro ⟨x, y, rfl⟩
+      apply Subtype.ext
+      rw [coe_rangeRestrict, Function.comp_apply, Subgroup.coeSubtype, Subtype.coe_mk, h] }
+
+@[to_additive (attr := simp)]
+theorem ofLeftInverse_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : G) :
+    ↑(ofLeftInverse h x) = f x :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem ofLeftInverse_symm_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f)
+    (x : f.range) : (ofLeftInverse h).symm x = g x :=
+  rfl
+
+/-- The range of an injective group homomorphism is isomorphic to its domain. -/
+@[to_additive "The range of an injective additive group homomorphism is isomorphic to its
+domain."]
+noncomputable def ofInjective {f : G →* N} (hf : Function.Injective f) : G ≃* f.range :=
+  MulEquiv.ofBijective (f.codRestrict f.range fun x => ⟨x, rfl⟩)
+    ⟨fun _ _ h => hf (Subtype.ext_iff.mp h), by
+      rintro ⟨x, y, rfl⟩
+      exact ⟨y, rfl⟩⟩
+
+@[to_additive]
+theorem ofInjective_apply {f : G →* N} (hf : Function.Injective f) {x : G} :
+    ↑(ofInjective hf x) = f x :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem apply_ofInjective_symm {f : G →* N} (hf : Function.Injective f) (x : f.range) :
+    f ((ofInjective hf).symm x) = x :=
+  Subtype.ext_iff.1 <| (ofInjective hf).apply_symm_apply x
+
+@[simp]
+theorem coe_toAdditive_range (f : G →* G') :
+    (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range := rfl
+
+@[simp]
+theorem coe_toMultiplicative_range {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
+    (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range := rfl
+
+section Ker
+
+variable {M : Type*} [MulOneClass M]
+
+/-- The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
+`f x = 1` -/
+@[to_additive
+      "The additive kernel of an `AddMonoid` homomorphism is the `AddSubgroup` of elements
+      such that `f x = 0`"]
+def ker (f : G →* M) : Subgroup G :=
+  { MonoidHom.mker f with
+    inv_mem' := fun {x} (hx : f x = 1) =>
+      calc
+        f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
+        _ = 1 := by rw [← map_mul, mul_inv_cancel, map_one] }
+
+@[to_additive (attr := simp)]
+theorem mem_ker {f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1 :=
+  Iff.rfl
+
+@[to_additive]
+theorem div_mem_ker_iff (f : G →* N) {x y : G} : x / y ∈ ker f ↔ f x = f y := by
+  rw [mem_ker, map_div, div_eq_one]
+
+@[to_additive]
+theorem coe_ker (f : G →* M) : (f.ker : Set G) = (f : G → M) ⁻¹' {1} :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem ker_toHomUnits {M} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker := by
+  ext x
+  simp [mem_ker, Units.ext_iff]
+
+@[to_additive]
+theorem eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker := by
+  constructor <;> intro h
+  · rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
+  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]
+
+@[to_additive]
+instance decidableMemKer [DecidableEq M] (f : G →* M) : DecidablePred (· ∈ f.ker) := fun x =>
+  decidable_of_iff (f x = 1) f.mem_ker
+
+@[to_additive]
+theorem comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem comap_bot (f : G →* N) : (⊥ : Subgroup N).comap f = f.ker :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem ker_restrict (f : G →* N) : (f.restrict K).ker = f.ker.subgroupOf K :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem ker_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S)
+    (h : ∀ x, f x ∈ s) : (f.codRestrict s h).ker = f.ker :=
+  SetLike.ext fun _x => Subtype.ext_iff
+
+@[to_additive (attr := simp)]
+theorem ker_rangeRestrict (f : G →* N) : ker (rangeRestrict f) = ker f :=
+  ker_codRestrict _ _ _
+
+@[to_additive (attr := simp)]
+theorem ker_one : (1 : G →* M).ker = ⊤ :=
+  SetLike.ext fun _x => eq_self_iff_true _
+
+@[to_additive (attr := simp)]
+theorem ker_id : (MonoidHom.id G).ker = ⊥ :=
+  rfl
+
+@[to_additive]
+theorem ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ Function.Injective f :=
+  ⟨fun h x y hxy => by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy, fun h =>
+    bot_unique fun _ hx => h (hx.trans f.map_one.symm)⟩
+
+@[to_additive (attr := simp)]
+theorem _root_.Subgroup.ker_subtype (H : Subgroup G) : H.subtype.ker = ⊥ :=
+  H.subtype.ker_eq_bot_iff.mpr Subtype.coe_injective
+
+@[to_additive (attr := simp)]
+theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥ :=
+  (inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)
+
+@[to_additive]
+theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
+    (f.prod g).ker = f.ker ⊓ g.ker :=
+  SetLike.ext fun _ => Prod.mk_eq_one
+
+@[to_additive]
+theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
+  ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y⟩
+
+@[to_additive]
+instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
+  ⟨fun x hx y => by
+    rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩
+
+@[simp]
+theorem coe_toAdditive_ker (f : G →* G') :
+    (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker := rfl
+
+@[simp]
+theorem coe_toMultiplicative_ker {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
+    (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker := rfl
+
+end Ker
+
+section EqLocus
+
+variable {M : Type*} [Monoid M]
+
+/-- The subgroup of elements `x : G` such that `f x = g x` -/
+@[to_additive "The additive subgroup of elements `x : G` such that `f x = g x`"]
+def eqLocus (f g : G →* M) : Subgroup G :=
+  { eqLocusM f g with inv_mem' := eq_on_inv f g }
+
+@[to_additive (attr := simp)]
+theorem eqLocus_same (f : G →* N) : f.eqLocus f = ⊤ :=
+  SetLike.ext fun _ => eq_self_iff_true _
+
+/-- If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure. -/
+@[to_additive
+      "If two monoid homomorphisms are equal on a set, then they are equal on its subgroup
+      closure."]
+theorem eqOn_closure {f g : G →* M} {s : Set G} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
+  show closure s ≤ f.eqLocus g from (closure_le _).2 h
+
+@[to_additive]
+theorem eq_of_eqOn_top {f g : G →* M} (h : Set.EqOn f g (⊤ : Subgroup G)) : f = g :=
+  ext fun _x => h trivial
+
+@[to_additive]
+theorem eq_of_eqOn_dense {s : Set G} (hs : closure s = ⊤) {f g : G →* M} (h : s.EqOn f g) : f = g :=
+  eq_of_eqOn_top <| hs ▸ eqOn_closure h
+
+end EqLocus
+
+end MonoidHom
+
+namespace Subgroup
+
+variable {N : Type*} [Group N] (H : Subgroup G)
+
+@[to_additive]
+theorem map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
+  (gc_map_comap f).l_eq_bot
+
+@[to_additive]
+theorem map_eq_bot_iff_of_injective {f : G →* N} (hf : Function.Injective f) :
+    H.map f = ⊥ ↔ H = ⊥ := by rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]
+
+open MonoidHom
+
+variable (f : G →* N)
+
+@[to_additive]
+theorem map_le_range (H : Subgroup G) : map f H ≤ f.range :=
+  (range_eq_map f).symm ▸ map_mono le_top
+
+@[to_additive]
+theorem map_subtype_le {H : Subgroup G} (K : Subgroup H) : K.map H.subtype ≤ H :=
+  (K.map_le_range H.subtype).trans (le_of_eq H.subtype_range)
+
+@[to_additive]
+theorem ker_le_comap (H : Subgroup N) : f.ker ≤ comap f H :=
+  comap_bot f ▸ comap_mono bot_le
+
+@[to_additive]
+theorem map_comap_eq (H : Subgroup N) : map f (comap f H) = f.range ⊓ H :=
+  SetLike.ext' <| by
+    rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
+
+@[to_additive]
+theorem comap_map_eq (H : Subgroup G) : comap f (map f H) = H ⊔ f.ker := by
+  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
+  intro x hx; simp only [exists_prop, mem_map, mem_comap] at hx
+  rcases hx with ⟨y, hy, hy'⟩
+  rw [← mul_inv_cancel_left y x]
+  exact mul_mem_sup hy (by simp [mem_ker, hy'])
+
+@[to_additive]
+theorem map_comap_eq_self {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) :
+    map f (comap f H) = H := by
+  rwa [map_comap_eq, inf_eq_right]
+
+@[to_additive]
+theorem map_comap_eq_self_of_surjective {f : G →* N} (h : Function.Surjective f) (H : Subgroup N) :
+    map f (comap f H) = H :=
+  map_comap_eq_self (range_eq_top.2 h ▸ le_top)
+
+@[to_additive]
+theorem comap_le_comap_of_le_range {f : G →* N} {K L : Subgroup N} (hf : K ≤ f.range) :
+    K.comap f ≤ L.comap f ↔ K ≤ L :=
+  ⟨(map_comap_eq_self hf).ge.trans ∘ map_le_iff_le_comap.mpr, comap_mono⟩
+
+@[to_additive]
+theorem comap_le_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
+    K.comap f ≤ L.comap f ↔ K ≤ L :=
+  comap_le_comap_of_le_range (range_eq_top.2 hf ▸ le_top)
+
+@[to_additive]
+theorem comap_lt_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
+    K.comap f < L.comap f ↔ K < L := by simp_rw [lt_iff_le_not_le, comap_le_comap_of_surjective hf]
+
+@[to_additive]
+theorem comap_injective {f : G →* N} (h : Function.Surjective f) : Function.Injective (comap f) :=
+  fun K L => by simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]
+
+@[to_additive]
+theorem comap_map_eq_self {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) :
+    comap f (map f H) = H := by
+  rwa [comap_map_eq, sup_eq_left]
+
+@[to_additive]
+theorem comap_map_eq_self_of_injective {f : G →* N} (h : Function.Injective f) (H : Subgroup G) :
+    comap f (map f H) = H :=
+  comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le)
+
+@[to_additive]
+theorem map_le_map_iff {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K ⊔ f.ker := by
+  rw [map_le_iff_le_comap, comap_map_eq]
+
+@[to_additive]
+theorem map_le_map_iff' {f : G →* N} {H K : Subgroup G} :
+    H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker := by
+  simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]
+
+@[to_additive]
+theorem map_eq_map_iff {f : G →* N} {H K : Subgroup G} :
+    H.map f = K.map f ↔ H ⊔ f.ker = K ⊔ f.ker := by simp only [le_antisymm_iff, map_le_map_iff']
+
+@[to_additive]
+theorem map_eq_range_iff {f : G →* N} {H : Subgroup G} :
+    H.map f = f.range ↔ Codisjoint H f.ker := by
+  rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]
+
+@[to_additive]
+theorem map_le_map_iff_of_injective {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} :
+    H.map f ≤ K.map f ↔ H ≤ K := by rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]
+
+@[to_additive (attr := simp)]
+theorem map_subtype_le_map_subtype {G' : Subgroup G} {H K : Subgroup G'} :
+    H.map G'.subtype ≤ K.map G'.subtype ↔ H ≤ K :=
+  map_le_map_iff_of_injective <| by apply Subtype.coe_injective
+
+@[to_additive]
+theorem map_injective {f : G →* N} (h : Function.Injective f) : Function.Injective (map f) :=
+  Function.LeftInverse.injective <| comap_map_eq_self_of_injective h
+
+/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`. -/
+@[to_additive "Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`."]
+theorem map_injective_of_ker_le {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K)
+    (hf : map f H = map f K) : H = K := by
+  apply_fun comap f at hf
+  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf
+
+@[to_additive]
+theorem closure_preimage_eq_top (s : Set G) : closure ((closure s).subtype ⁻¹' s) = ⊤ := by
+  apply map_injective (closure s).subtype_injective
+  rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, subtype_range,
+    Set.image_preimage_eq_of_subset]
+  rw [coeSubtype, Subtype.range_coe_subtype]
+  exact subset_closure
+
+@[to_additive]
+theorem comap_sup_eq_of_le_range {H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) :
+    comap f H ⊔ comap f K = comap f (H ⊔ K) :=
+  map_injective_of_ker_le f ((ker_le_comap f H).trans le_sup_left) (ker_le_comap f (H ⊔ K))
+    (by
+      rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
+        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)])
+
+@[to_additive]
+theorem comap_sup_eq (H K : Subgroup N) (hf : Function.Surjective f) :
+    comap f H ⊔ comap f K = comap f (H ⊔ K) :=
+  comap_sup_eq_of_le_range f (range_eq_top.2 hf ▸ le_top) (range_eq_top.2 hf ▸ le_top)
+
+@[to_additive]
+theorem sup_subgroupOf_eq {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) :
+    H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L :=
+  comap_sup_eq_of_le_range L.subtype (hH.trans L.subtype_range.ge) (hK.trans L.subtype_range.ge)
+
+@[to_additive]
+theorem codisjoint_subgroupOf_sup (H K : Subgroup G) :
+    Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)) := by
+  rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self]
+  exacts [le_sup_left, le_sup_right]
+
+@[to_additive]
+theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
+    (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B := by
+  refine
+    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
+      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
+  simp only [subgroupOf, map_comap_eq, map_sup, subtype_range]
+  rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
+
+end Subgroup
diff --git a/Mathlib/Algebra/Group/Subgroup/Lattice.lean b/Mathlib/Algebra/Group/Subgroup/Lattice.lean
new file mode 100644
index 0000000000000..ea029ac82db4b
--- /dev/null
+++ b/Mathlib/Algebra/Group/Subgroup/Lattice.lean
@@ -0,0 +1,558 @@
+/-
+Copyright (c) 2020 Kexing Ying. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kexing Ying
+-/
+import Mathlib.Algebra.Group.Submonoid.Operations
+import Mathlib.Algebra.Group.Subgroup.Defs
+
+/-!
+# Lattice structure of subgroups
+
+We prove subgroups of a group form a complete lattice.
+
+There are also theorems about the subgroups generated by an element or a subset of a group,
+defined both inductively and as the infimum of the set of subgroups containing a given
+element/subset.
+
+Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
+
+## Main definitions
+
+Notation used here:
+
+- `G` is a `Group`
+
+- `k` is a set of elements of type `G`
+
+Definitions in the file:
+
+* `CompleteLattice (Subgroup G)` : the subgroups of `G` form a complete lattice
+
+* `Subgroup.closure k` : the minimal subgroup that includes the set `k`
+
+* `Subgroup.gi` : `closure` forms a Galois insertion with the coercion to set
+
+## Implementation notes
+
+Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
+membership of a subgroup's underlying set.
+
+## Tags
+subgroup, subgroups
+-/
+
+assert_not_exists OrderedAddCommMonoid
+assert_not_exists Multiset
+assert_not_exists Ring
+
+open Function
+open scoped Int
+
+variable {G : Type*} [Group G]
+
+/-!
+### Conversion to/from `Additive`/`Multiplicative`
+-/
+
+section mul_add
+
+variable {A : Type*} [AddGroup A]
+
+/-- Subgroups of a group `G` are isomorphic to additive subgroups of `Additive G`. -/
+@[simps!]
+def Subgroup.toAddSubgroup : Subgroup G ≃o AddSubgroup (Additive G) where
+  toFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
+  invFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
+  left_inv x := by cases x; rfl
+  right_inv x := by cases x; rfl
+  map_rel_iff' := Iff.rfl
+
+/-- Additive subgroup of an additive group `Additive G` are isomorphic to subgroup of `G`. -/
+abbrev AddSubgroup.toSubgroup' : AddSubgroup (Additive G) ≃o Subgroup G :=
+  Subgroup.toAddSubgroup.symm
+
+/-- Additive subgroups of an additive group `A` are isomorphic to subgroups of `Multiplicative A`.
+-/
+@[simps!]
+def AddSubgroup.toSubgroup : AddSubgroup A ≃o Subgroup (Multiplicative A) where
+  toFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
+  invFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
+  left_inv x := by cases x; rfl
+  right_inv x := by cases x; rfl
+  map_rel_iff' := Iff.rfl
+
+/-- Subgroups of an additive group `Multiplicative A` are isomorphic to additive subgroups of `A`.
+-/
+abbrev Subgroup.toAddSubgroup' : Subgroup (Multiplicative A) ≃o AddSubgroup A :=
+  AddSubgroup.toSubgroup.symm
+
+end mul_add
+
+namespace Subgroup
+
+variable (H K : Subgroup G)
+
+/-- The subgroup `G` of the group `G`. -/
+@[to_additive "The `AddSubgroup G` of the `AddGroup G`."]
+instance : Top (Subgroup G) :=
+  ⟨{ (⊤ : Submonoid G) with inv_mem' := fun _ => Set.mem_univ _ }⟩
+
+/-- The top subgroup is isomorphic to the group.
+
+This is the group version of `Submonoid.topEquiv`. -/
+@[to_additive (attr := simps!)
+      "The top additive subgroup is isomorphic to the additive group.
+
+      This is the additive group version of `AddSubmonoid.topEquiv`."]
+def topEquiv : (⊤ : Subgroup G) ≃* G :=
+  Submonoid.topEquiv
+
+/-- The trivial subgroup `{1}` of a group `G`. -/
+@[to_additive "The trivial `AddSubgroup` `{0}` of an `AddGroup` `G`."]
+instance : Bot (Subgroup G) :=
+  ⟨{ (⊥ : Submonoid G) with inv_mem' := by simp}⟩
+
+@[to_additive]
+instance : Inhabited (Subgroup G) :=
+  ⟨⊥⟩
+
+@[to_additive (attr := simp)]
+theorem mem_bot {x : G} : x ∈ (⊥ : Subgroup G) ↔ x = 1 :=
+  Iff.rfl
+
+@[to_additive (attr := simp)]
+theorem mem_top (x : G) : x ∈ (⊤ : Subgroup G) :=
+  Set.mem_univ x
+
+@[to_additive (attr := simp)]
+theorem coe_top : ((⊤ : Subgroup G) : Set G) = Set.univ :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem coe_bot : ((⊥ : Subgroup G) : Set G) = {1} :=
+  rfl
+
+@[to_additive]
+instance : Unique (⊥ : Subgroup G) :=
+  ⟨⟨1⟩, fun g => Subtype.ext g.2⟩
+
+@[to_additive (attr := simp)]
+theorem top_toSubmonoid : (⊤ : Subgroup G).toSubmonoid = ⊤ :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem bot_toSubmonoid : (⊥ : Subgroup G).toSubmonoid = ⊥ :=
+  rfl
+
+@[to_additive]
+theorem eq_bot_iff_forall : H = ⊥ ↔ ∀ x ∈ H, x = (1 : G) :=
+  toSubmonoid_injective.eq_iff.symm.trans <| Submonoid.eq_bot_iff_forall _
+
+@[to_additive]
+theorem eq_bot_of_subsingleton [Subsingleton H] : H = ⊥ := by
+  rw [Subgroup.eq_bot_iff_forall]
+  intro y hy
+  rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_eq_univ {H : Subgroup G} : (H : Set G) = Set.univ ↔ H = ⊤ :=
+  (SetLike.ext'_iff.trans (by rfl)).symm
+
+@[to_additive]
+theorem coe_eq_singleton {H : Subgroup G} : (∃ g : G, (H : Set G) = {g}) ↔ H = ⊥ :=
+  ⟨fun ⟨g, hg⟩ =>
+    haveI : Subsingleton (H : Set G) := by
+      rw [hg]
+      infer_instance
+    H.eq_bot_of_subsingleton,
+    fun h => ⟨1, SetLike.ext'_iff.mp h⟩⟩
+
+@[to_additive]
+theorem nontrivial_iff_exists_ne_one (H : Subgroup G) : Nontrivial H ↔ ∃ x ∈ H, x ≠ (1 : G) := by
+  rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
+  simp
+
+@[to_additive]
+theorem exists_ne_one_of_nontrivial (H : Subgroup G) [Nontrivial H] :
+    ∃ x ∈ H, x ≠ 1 := by
+  rwa [← Subgroup.nontrivial_iff_exists_ne_one]
+
+@[to_additive]
+theorem nontrivial_iff_ne_bot (H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥ := by
+  rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
+  simp only [ne_eq, not_forall, exists_prop]
+
+/-- A subgroup is either the trivial subgroup or nontrivial. -/
+@[to_additive "A subgroup is either the trivial subgroup or nontrivial."]
+theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H := by
+  have := nontrivial_iff_ne_bot H
+  tauto
+
+/-- A subgroup is either the trivial subgroup or contains a non-identity element. -/
+@[to_additive "A subgroup is either the trivial subgroup or contains a nonzero element."]
+theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1 : G) := by
+  convert H.bot_or_nontrivial
+  rw [nontrivial_iff_exists_ne_one]
+
+@[to_additive]
+lemma ne_bot_iff_exists_ne_one {H : Subgroup G} : H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1 := by
+  rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
+  simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]
+
+/-- The inf of two subgroups is their intersection. -/
+@[to_additive "The inf of two `AddSubgroup`s is their intersection."]
+instance : Min (Subgroup G) :=
+  ⟨fun H₁ H₂ =>
+    { H₁.toSubmonoid ⊓ H₂.toSubmonoid with
+      inv_mem' := fun ⟨hx, hx'⟩ => ⟨H₁.inv_mem hx, H₂.inv_mem hx'⟩ }⟩
+
+@[to_additive (attr := simp)]
+theorem coe_inf (p p' : Subgroup G) : ((p ⊓ p' : Subgroup G) : Set G) = (p : Set G) ∩ p' :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_inf {p p' : Subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
+  Iff.rfl
+
+@[to_additive]
+instance : InfSet (Subgroup G) :=
+  ⟨fun s =>
+    { (⨅ S ∈ s, Subgroup.toSubmonoid S).copy (⋂ S ∈ s, ↑S) (by simp) with
+      inv_mem' := fun {x} hx =>
+        Set.mem_biInter fun i h => i.inv_mem (by apply Set.mem_iInter₂.1 hx i h) }⟩
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_sInf (H : Set (Subgroup G)) : ((sInf H : Subgroup G) : Set G) = ⋂ s ∈ H, ↑s :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_sInf {S : Set (Subgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
+  Set.mem_iInter₂
+
+@[to_additive]
+theorem mem_iInf {ι : Sort*} {S : ι → Subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
+  simp only [iInf, mem_sInf, Set.forall_mem_range]
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_iInf {ι : Sort*} {S : ι → Subgroup G} : (↑(⨅ i, S i) : Set G) = ⋂ i, S i := by
+  simp only [iInf, coe_sInf, Set.biInter_range]
+
+/-- Subgroups of a group form a complete lattice. -/
+@[to_additive "The `AddSubgroup`s of an `AddGroup` form a complete lattice."]
+instance : CompleteLattice (Subgroup G) :=
+  { completeLatticeOfInf (Subgroup G) fun _s =>
+      IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
+    bot := ⊥
+    bot_le := fun S _x hx => (mem_bot.1 hx).symm ▸ S.one_mem
+    top := ⊤
+    le_top := fun _S x _hx => mem_top x
+    inf := (· ⊓ ·)
+    le_inf := fun _a _b _c ha hb _x hx => ⟨ha hx, hb hx⟩
+    inf_le_left := fun _a _b _x => And.left
+    inf_le_right := fun _a _b _x => And.right }
+
+@[to_additive]
+theorem mem_sup_left {S T : Subgroup G} : ∀ {x : G}, x ∈ S → x ∈ S ⊔ T :=
+  have : S ≤ S ⊔ T := le_sup_left; fun h ↦ this h
+
+@[to_additive]
+theorem mem_sup_right {S T : Subgroup G} : ∀ {x : G}, x ∈ T → x ∈ S ⊔ T :=
+  have : T ≤ S ⊔ T := le_sup_right; fun h ↦ this h
+
+@[to_additive]
+theorem mul_mem_sup {S T : Subgroup G} {x y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
+  (S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)
+
+@[to_additive]
+theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Subgroup G} (i : ι) :
+    ∀ {x : G}, x ∈ S i → x ∈ iSup S :=
+  have : S i ≤ iSup S := le_iSup _ _; fun h ↦ this h
+
+@[to_additive]
+theorem mem_sSup_of_mem {S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) :
+    ∀ {x : G}, x ∈ s → x ∈ sSup S :=
+  have : s ≤ sSup S := le_sSup hs; fun h ↦ this h
+
+@[to_additive (attr := simp)]
+theorem subsingleton_iff : Subsingleton (Subgroup G) ↔ Subsingleton G :=
+  ⟨fun _ =>
+    ⟨fun x y =>
+      have : ∀ i : G, i = 1 := fun i =>
+        mem_bot.mp <| Subsingleton.elim (⊤ : Subgroup G) ⊥ ▸ mem_top i
+      (this x).trans (this y).symm⟩,
+    fun _ => ⟨fun x y => Subgroup.ext fun i => Subsingleton.elim 1 i ▸ by simp [Subgroup.one_mem]⟩⟩
+
+@[to_additive (attr := simp)]
+theorem nontrivial_iff : Nontrivial (Subgroup G) ↔ Nontrivial G :=
+  not_iff_not.mp
+    ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans
+      not_nontrivial_iff_subsingleton.symm)
+
+@[to_additive]
+instance [Subsingleton G] : Unique (Subgroup G) :=
+  ⟨⟨⊥⟩, fun a => @Subsingleton.elim _ (subsingleton_iff.mpr ‹_›) a _⟩
+
+@[to_additive]
+instance [Nontrivial G] : Nontrivial (Subgroup G) :=
+  nontrivial_iff.mpr ‹_›
+
+@[to_additive]
+theorem eq_top_iff' : H = ⊤ ↔ ∀ x : G, x ∈ H :=
+  eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩
+
+/-- The `Subgroup` generated by a set. -/
+@[to_additive "The `AddSubgroup` generated by a set"]
+def closure (k : Set G) : Subgroup G :=
+  sInf { K | k ⊆ K }
+
+variable {k : Set G}
+
+@[to_additive]
+theorem mem_closure {x : G} : x ∈ closure k ↔ ∀ K : Subgroup G, k ⊆ K → x ∈ K :=
+  mem_sInf
+
+/-- The subgroup generated by a set includes the set. -/
+@[to_additive (attr := simp, aesop safe 20 apply (rule_sets := [SetLike]))
+  "The `AddSubgroup` generated by a set includes the set."]
+theorem subset_closure : k ⊆ closure k := fun _ hx => mem_closure.2 fun _ hK => hK hx
+
+@[to_additive]
+theorem not_mem_of_not_mem_closure {P : G} (hP : P ∉ closure k) : P ∉ k := fun h =>
+  hP (subset_closure h)
+
+open Set
+
+/-- A subgroup `K` includes `closure k` if and only if it includes `k`. -/
+@[to_additive (attr := simp)
+  "An additive subgroup `K` includes `closure k` if and only if it includes `k`"]
+theorem closure_le : closure k ≤ K ↔ k ⊆ K :=
+  ⟨Subset.trans subset_closure, fun h => sInf_le h⟩
+
+@[to_additive]
+theorem closure_eq_of_le (h₁ : k ⊆ K) (h₂ : K ≤ closure k) : closure k = K :=
+  le_antisymm ((closure_le <| K).2 h₁) h₂
+
+/-- An induction principle for closure membership. If `p` holds for `1` and all elements of `k`, and
+is preserved under multiplication and inverse, then `p` holds for all elements of the closure
+of `k`.
+
+See also `Subgroup.closure_induction_left` and `Subgroup.closure_induction_right` for versions that
+only require showing `p` is preserved by multiplication by elements in `k`. -/
+@[to_additive (attr := elab_as_elim)
+      "An induction principle for additive closure membership. If `p`
+      holds for `0` and all elements of `k`, and is preserved under addition and inverses, then `p`
+      holds for all elements of the additive closure of `k`.
+
+      See also `AddSubgroup.closure_induction_left` and `AddSubgroup.closure_induction_left` for
+      versions that only require showing `p` is preserved by addition by elements in `k`."]
+theorem closure_induction {p : (g : G) → g ∈ closure k → Prop}
+    (mem : ∀ x (hx : x ∈ k), p x (subset_closure hx)) (one : p 1 (one_mem _))
+    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
+    (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx :=
+  let K : Subgroup G :=
+    { carrier := { x | ∃ hx, p x hx }
+      mul_mem' := fun ⟨_, ha⟩ ⟨_, hb⟩ ↦ ⟨_, mul _ _ _ _ ha hb⟩
+      one_mem' := ⟨_, one⟩
+      inv_mem' := fun ⟨_, hb⟩ ↦ ⟨_, inv _ _ hb⟩ }
+  closure_le (K := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
+
+@[deprecated closure_induction (since := "2024-10-10")]
+alias closure_induction' := closure_induction
+
+/-- An induction principle for closure membership for predicates with two arguments. -/
+@[to_additive (attr := elab_as_elim)
+      "An induction principle for additive closure membership, for
+      predicates with two arguments."]
+theorem closure_induction₂ {p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop}
+    (mem : ∀ (x) (y) (hx : x ∈ k) (hy : y ∈ k), p x y (subset_closure hx) (subset_closure hy))
+    (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
+    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
+    (mul_right : ∀ y z x hy hz hx, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
+    (inv_left : ∀ x y hx hy, p x y hx hy → p x⁻¹ y (inv_mem hx) hy)
+    (inv_right : ∀ x y hx hy, p x y hx hy → p x y⁻¹ hx (inv_mem hy))
+    {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy := by
+  induction hy using closure_induction with
+  | mem z hz => induction hx using closure_induction with
+    | mem _ h => exact mem _ _ h hz
+    | one => exact one_left _ (subset_closure hz)
+    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
+    | inv _ _ h => exact inv_left _ _ _ _ h
+  | one => exact one_right x hx
+  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
+  | inv _ _ h => exact inv_right _ _ _ _ h
+
+@[to_additive (attr := simp)]
+theorem closure_closure_coe_preimage {k : Set G} : closure (((↑) : closure k → G) ⁻¹' k) = ⊤ :=
+  eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
+    closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem)
+      (fun _ _ ↦ inv_mem) hx'
+
+variable (G)
+
+/-- `closure` forms a Galois insertion with the coercion to set. -/
+@[to_additive "`closure` forms a Galois insertion with the coercion to set."]
+protected def gi : GaloisInsertion (@closure G _) (↑) where
+  choice s _ := closure s
+  gc s t := @closure_le _ _ t s
+  le_l_u _s := subset_closure
+  choice_eq _s _h := rfl
+
+variable {G}
+
+/-- Subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
+then `closure h ≤ closure k`. -/
+@[to_additive
+      "Additive subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
+      then `closure h ≤ closure k`"]
+theorem closure_mono ⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k :=
+  (Subgroup.gi G).gc.monotone_l h'
+
+/-- Closure of a subgroup `K` equals `K`. -/
+@[to_additive (attr := simp) "Additive closure of an additive subgroup `K` equals `K`"]
+theorem closure_eq : closure (K : Set G) = K :=
+  (Subgroup.gi G).l_u_eq K
+
+@[to_additive (attr := simp)]
+theorem closure_empty : closure (∅ : Set G) = ⊥ :=
+  (Subgroup.gi G).gc.l_bot
+
+@[to_additive (attr := simp)]
+theorem closure_univ : closure (univ : Set G) = ⊤ :=
+  @coe_top G _ ▸ closure_eq ⊤
+
+@[to_additive]
+theorem closure_union (s t : Set G) : closure (s ∪ t) = closure s ⊔ closure t :=
+  (Subgroup.gi G).gc.l_sup
+
+@[to_additive]
+theorem sup_eq_closure (H H' : Subgroup G) : H ⊔ H' = closure ((H : Set G) ∪ (H' : Set G)) := by
+  simp_rw [closure_union, closure_eq]
+
+@[to_additive]
+theorem closure_iUnion {ι} (s : ι → Set G) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
+  (Subgroup.gi G).gc.l_iSup
+
+@[to_additive (attr := simp)]
+theorem closure_eq_bot_iff : closure k = ⊥ ↔ k ⊆ {1} := le_bot_iff.symm.trans <| closure_le _
+
+@[to_additive]
+theorem iSup_eq_closure {ι : Sort*} (p : ι → Subgroup G) :
+    ⨆ i, p i = closure (⋃ i, (p i : Set G)) := by simp_rw [closure_iUnion, closure_eq]
+
+/-- The subgroup generated by an element of a group equals the set of integer number powers of
+    the element. -/
+@[to_additive
+      "The `AddSubgroup` generated by an element of an `AddGroup` equals the set of
+      natural number multiples of the element."]
+theorem mem_closure_singleton {x y : G} : y ∈ closure ({x} : Set G) ↔ ∃ n : ℤ, x ^ n = y := by
+  refine
+    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
+      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
+  · intro y hy
+    rw [eq_of_mem_singleton hy]
+    exact ⟨1, zpow_one x⟩
+  · exact ⟨0, zpow_zero x⟩
+  · rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
+    exact ⟨n + m, zpow_add x n m⟩
+  rintro _ _ ⟨n, rfl⟩
+  exact ⟨-n, zpow_neg x n⟩
+
+@[to_additive]
+theorem closure_singleton_one : closure ({1} : Set G) = ⊥ := by
+  simp [eq_bot_iff_forall, mem_closure_singleton]
+
+@[to_additive (attr := simp)]
+lemma mem_closure_singleton_self (x : G) : x ∈ closure ({x} : Set G) := by
+  simpa [-subset_closure] using subset_closure (k := {x})
+
+@[to_additive]
+theorem le_closure_toSubmonoid (S : Set G) : Submonoid.closure S ≤ (closure S).toSubmonoid :=
+  Submonoid.closure_le.2 subset_closure
+
+@[to_additive]
+theorem closure_eq_top_of_mclosure_eq_top {S : Set G} (h : Submonoid.closure S = ⊤) :
+    closure S = ⊤ :=
+  (eq_top_iff' _).2 fun _ => le_closure_toSubmonoid _ <| h.symm ▸ trivial
+
+@[to_additive]
+theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (· ≤ ·) K)
+    {x : G} : x ∈ (iSup K : Subgroup G) ↔ ∃ i, x ∈ K i := by
+  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup K i hi⟩
+  suffices x ∈ closure (⋃ i, (K i : Set G)) → ∃ i, x ∈ K i by
+    simpa only [closure_iUnion, closure_eq (K _)] using this
+  refine fun hx ↦ closure_induction (fun _ ↦ mem_iUnion.1) ?_ ?_ ?_ hx
+  · exact hι.elim fun i ↦ ⟨i, (K i).one_mem⟩
+  · rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩
+    rcases hK i j with ⟨k, hki, hkj⟩
+    exact ⟨k, mul_mem (hki hi) (hkj hj)⟩
+  · rintro _ _ ⟨i, hi⟩
+    exact ⟨i, inv_mem hi⟩
+
+@[to_additive]
+theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (· ≤ ·) S) :
+    ((⨆ i, S i : Subgroup G) : Set G) = ⋃ i, S i :=
+  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]
+
+@[to_additive]
+theorem mem_sSup_of_directedOn {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (· ≤ ·) K)
+    {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s := by
+  haveI : Nonempty K := Kne.to_subtype
+  simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, Subtype.coe_mk,
+    exists_prop]
+
+variable {C : Type*} [CommGroup C] {s t : Subgroup C} {x : C}
+
+@[to_additive]
+theorem mem_sup : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x :=
+  ⟨fun h => by
+    rw [sup_eq_closure] at h
+    refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
+    · rintro y (h | h)
+      · exact ⟨y, h, 1, t.one_mem, by simp⟩
+      · exact ⟨1, s.one_mem, y, h, by simp⟩
+    · exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
+    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
+      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
+    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
+      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩, by
+    rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz⟩
+
+@[to_additive]
+theorem mem_sup' : x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y : C) * z = x :=
+  mem_sup.trans <| by simp only [SetLike.exists, coe_mk, exists_prop]
+
+@[to_additive]
+theorem mem_closure_pair {x y z : C} :
+    z ∈ closure ({x, y} : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z := by
+  rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
+  simp_rw [mem_closure_singleton, exists_exists_eq_and]
+
+@[to_additive]
+theorem disjoint_def {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1 :=
+  disjoint_iff_inf_le.trans <| by simp only [Disjoint, SetLike.le_def, mem_inf, mem_bot, and_imp]
+
+@[to_additive]
+theorem disjoint_def' {H₁ H₂ : Subgroup G} :
+    Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1 :=
+  disjoint_def.trans ⟨fun h _x _y hx hy hxy ↦ h hx <| hxy.symm ▸ hy, fun h _x hx hx' ↦ h hx hx' rfl⟩
+
+@[to_additive]
+theorem disjoint_iff_mul_eq_one {H₁ H₂ : Subgroup G} :
+    Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1 :=
+  disjoint_def'.trans
+    ⟨fun h x y hx hy hxy =>
+      let hx1 : x = 1 := h hx (H₂.inv_mem hy) (eq_inv_iff_mul_eq_one.mpr hxy)
+      ⟨hx1, by simpa [hx1] using hxy⟩,
+      fun h _ _ hx hy hxy => (h hx (H₂.inv_mem hy) (mul_inv_eq_one.mpr hxy)).1⟩
+
+@[to_additive]
+theorem mul_injective_of_disjoint {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
+    Function.Injective (fun g => g.1 * g.2 : H₁ × H₂ → G) := by
+  intro x y hxy
+  rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
+  replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
+  rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
+    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
+
+end Subgroup
diff --git a/Mathlib/Algebra/Group/Subgroup/Map.lean b/Mathlib/Algebra/Group/Subgroup/Map.lean
new file mode 100644
index 0000000000000..84450e745384e
--- /dev/null
+++ b/Mathlib/Algebra/Group/Subgroup/Map.lean
@@ -0,0 +1,527 @@
+/-
+Copyright (c) 2020 Kexing Ying. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kexing Ying
+-/
+import Mathlib.Algebra.Group.Subgroup.Lattice
+
+/-!
+# `map` and `comap` for subgroups
+
+We prove results about images and preimages of subgroups under group homomorphisms. The bundled
+subgroups use bundled monoid homomorphisms.
+
+Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
+
+## Main definitions
+
+Notation used here:
+
+- `G N` are `Group`s
+
+- `H` is a `Subgroup` of `G`
+
+- `x` is an element of type `G` or type `A`
+
+- `f g : N →* G` are group homomorphisms
+
+- `s k` are sets of elements of type `G`
+
+Definitions in the file:
+
+* `Subgroup.comap H f` : the preimage of a subgroup `H` along the group homomorphism `f` is also a
+  subgroup
+
+* `Subgroup.map f H` : the image of a subgroup `H` along the group homomorphism `f` is also a
+  subgroup
+
+## Implementation notes
+
+Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
+membership of a subgroup's underlying set.
+
+## Tags
+subgroup, subgroups
+-/
+
+assert_not_exists OrderedAddCommMonoid
+assert_not_exists Multiset
+assert_not_exists Ring
+
+open Function
+open scoped Int
+
+variable {G G' G'' : Type*} [Group G] [Group G'] [Group G'']
+variable {A : Type*} [AddGroup A]
+
+namespace Subgroup
+
+variable (H K : Subgroup G) {k : Set G}
+
+open Set
+
+variable {N : Type*} [Group N] {P : Type*} [Group P]
+
+/-- The preimage of a subgroup along a monoid homomorphism is a subgroup. -/
+@[to_additive
+      "The preimage of an `AddSubgroup` along an `AddMonoid` homomorphism
+      is an `AddSubgroup`."]
+def comap {N : Type*} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G :=
+  { H.toSubmonoid.comap f with
+    carrier := f ⁻¹' H
+    inv_mem' := fun {a} ha => show f a⁻¹ ∈ H by rw [f.map_inv]; exact H.inv_mem ha }
+
+@[to_additive (attr := simp)]
+theorem coe_comap (K : Subgroup N) (f : G →* N) : (K.comap f : Set G) = f ⁻¹' K :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_comap {K : Subgroup N} {f : G →* N} {x : G} : x ∈ K.comap f ↔ f x ∈ K :=
+  Iff.rfl
+
+@[to_additive]
+theorem comap_mono {f : G →* N} {K K' : Subgroup N} : K ≤ K' → comap f K ≤ comap f K' :=
+  preimage_mono
+
+@[to_additive]
+theorem comap_comap (K : Subgroup P) (g : N →* P) (f : G →* N) :
+    (K.comap g).comap f = K.comap (g.comp f) :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem comap_id (K : Subgroup N) : K.comap (MonoidHom.id _) = K := by
+  ext
+  rfl
+
+@[simp]
+theorem toAddSubgroup_comap {G₂ : Type*} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
+    s.toAddSubgroup.comap (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.comap f) := rfl
+
+@[simp]
+theorem _root_.AddSubgroup.toSubgroup_comap {A A₂ : Type*} [AddGroup A] [AddGroup A₂]
+    (f : A →+ A₂) (s : AddSubgroup A₂) :
+    s.toSubgroup.comap (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.comap f) := rfl
+
+/-- The image of a subgroup along a monoid homomorphism is a subgroup. -/
+@[to_additive
+      "The image of an `AddSubgroup` along an `AddMonoid` homomorphism
+      is an `AddSubgroup`."]
+def map (f : G →* N) (H : Subgroup G) : Subgroup N :=
+  { H.toSubmonoid.map f with
+    carrier := f '' H
+    inv_mem' := by
+      rintro _ ⟨x, hx, rfl⟩
+      exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩ }
+
+@[to_additive (attr := simp)]
+theorem coe_map (f : G →* N) (K : Subgroup G) : (K.map f : Set N) = f '' K :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_map {f : G →* N} {K : Subgroup G} {y : N} : y ∈ K.map f ↔ ∃ x ∈ K, f x = y := Iff.rfl
+
+@[to_additive]
+theorem mem_map_of_mem (f : G →* N) {K : Subgroup G} {x : G} (hx : x ∈ K) : f x ∈ K.map f :=
+  mem_image_of_mem f hx
+
+@[to_additive]
+theorem apply_coe_mem_map (f : G →* N) (K : Subgroup G) (x : K) : f x ∈ K.map f :=
+  mem_map_of_mem f x.prop
+
+@[to_additive]
+theorem map_mono {f : G →* N} {K K' : Subgroup G} : K ≤ K' → map f K ≤ map f K' :=
+  image_subset _
+
+@[to_additive (attr := simp)]
+theorem map_id : K.map (MonoidHom.id G) = K :=
+  SetLike.coe_injective <| image_id _
+
+@[to_additive]
+theorem map_map (g : N →* P) (f : G →* N) : (K.map f).map g = K.map (g.comp f) :=
+  SetLike.coe_injective <| image_image _ _ _
+
+@[to_additive (attr := simp)]
+theorem map_one_eq_bot : K.map (1 : G →* N) = ⊥ :=
+  eq_bot_iff.mpr <| by
+    rintro x ⟨y, _, rfl⟩
+    simp
+
+@[to_additive]
+theorem mem_map_equiv {f : G ≃* N} {K : Subgroup G} {x : N} :
+    x ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K := by
+  erw [@Set.mem_image_equiv _ _ (↑K) f.toEquiv x]; rfl
+
+-- The simpNF linter says that the LHS can be simplified via `Subgroup.mem_map`.
+-- However this is a higher priority lemma.
+-- https://github.com/leanprover/std4/issues/207
+@[to_additive (attr := simp 1100, nolint simpNF)]
+theorem mem_map_iff_mem {f : G →* N} (hf : Function.Injective f) {K : Subgroup G} {x : G} :
+    f x ∈ K.map f ↔ x ∈ K :=
+  hf.mem_set_image
+
+@[to_additive]
+theorem map_equiv_eq_comap_symm' (f : G ≃* N) (K : Subgroup G) :
+    K.map f.toMonoidHom = K.comap f.symm.toMonoidHom :=
+  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)
+
+@[to_additive]
+theorem map_equiv_eq_comap_symm (f : G ≃* N) (K : Subgroup G) :
+    K.map f = K.comap (G := N) f.symm :=
+  map_equiv_eq_comap_symm' _ _
+
+@[to_additive]
+theorem comap_equiv_eq_map_symm (f : N ≃* G) (K : Subgroup G) :
+    K.comap (G := N) f = K.map f.symm :=
+  (map_equiv_eq_comap_symm f.symm K).symm
+
+@[to_additive]
+theorem comap_equiv_eq_map_symm' (f : N ≃* G) (K : Subgroup G) :
+    K.comap f.toMonoidHom = K.map f.symm.toMonoidHom :=
+  (map_equiv_eq_comap_symm f.symm K).symm
+
+@[to_additive]
+theorem map_symm_eq_iff_map_eq {H : Subgroup N} {e : G ≃* N} :
+    H.map ↑e.symm = K ↔ K.map ↑e = H := by
+  constructor <;> rintro rfl
+  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
+      MulEquiv.coe_monoidHom_refl, map_id]
+  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
+      MulEquiv.coe_monoidHom_refl, map_id]
+
+@[to_additive]
+theorem map_le_iff_le_comap {f : G →* N} {K : Subgroup G} {H : Subgroup N} :
+    K.map f ≤ H ↔ K ≤ H.comap f :=
+  image_subset_iff
+
+@[to_additive]
+theorem gc_map_comap (f : G →* N) : GaloisConnection (map f) (comap f) := fun _ _ =>
+  map_le_iff_le_comap
+
+@[to_additive]
+theorem map_sup (H K : Subgroup G) (f : G →* N) : (H ⊔ K).map f = H.map f ⊔ K.map f :=
+  (gc_map_comap f).l_sup
+
+@[to_additive]
+theorem map_iSup {ι : Sort*} (f : G →* N) (s : ι → Subgroup G) :
+    (iSup s).map f = ⨆ i, (s i).map f :=
+  (gc_map_comap f).l_iSup
+
+@[to_additive]
+theorem map_inf (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
+    (H ⊓ K).map f = H.map f ⊓ K.map f := SetLike.coe_injective (Set.image_inter hf)
+
+@[to_additive]
+theorem map_iInf {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f)
+    (s : ι → Subgroup G) : (iInf s).map f = ⨅ i, (s i).map f := by
+  apply SetLike.coe_injective
+  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)
+
+@[to_additive]
+theorem comap_sup_comap_le (H K : Subgroup N) (f : G →* N) :
+    comap f H ⊔ comap f K ≤ comap f (H ⊔ K) :=
+  Monotone.le_map_sup (fun _ _ => comap_mono) H K
+
+@[to_additive]
+theorem iSup_comap_le {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) :
+    ⨆ i, (s i).comap f ≤ (iSup s).comap f :=
+  Monotone.le_map_iSup fun _ _ => comap_mono
+
+@[to_additive]
+theorem comap_inf (H K : Subgroup N) (f : G →* N) : (H ⊓ K).comap f = H.comap f ⊓ K.comap f :=
+  (gc_map_comap f).u_inf
+
+@[to_additive]
+theorem comap_iInf {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) :
+    (iInf s).comap f = ⨅ i, (s i).comap f :=
+  (gc_map_comap f).u_iInf
+
+@[to_additive]
+theorem map_inf_le (H K : Subgroup G) (f : G →* N) : map f (H ⊓ K) ≤ map f H ⊓ map f K :=
+  le_inf (map_mono inf_le_left) (map_mono inf_le_right)
+
+@[to_additive]
+theorem map_inf_eq (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
+    map f (H ⊓ K) = map f H ⊓ map f K := by
+  rw [← SetLike.coe_set_eq]
+  simp [Set.image_inter hf]
+
+@[to_additive (attr := simp)]
+theorem map_bot (f : G →* N) : (⊥ : Subgroup G).map f = ⊥ :=
+  (gc_map_comap f).l_bot
+
+@[to_additive (attr := simp)]
+theorem map_top_of_surjective (f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤ := by
+  rw [eq_top_iff]
+  intro x _
+  obtain ⟨y, hy⟩ := h x
+  exact ⟨y, trivial, hy⟩
+
+@[to_additive (attr := simp)]
+theorem comap_top (f : G →* N) : (⊤ : Subgroup N).comap f = ⊤ :=
+  (gc_map_comap f).u_top
+
+/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`. -/
+@[to_additive "For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`."]
+def subgroupOf (H K : Subgroup G) : Subgroup K :=
+  H.comap K.subtype
+
+/-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`. -/
+@[to_additive (attr := simps) "If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`."]
+def subgroupOfEquivOfLe {G : Type*} [Group G] {H K : Subgroup G} (h : H ≤ K) :
+    H.subgroupOf K ≃* H where
+  toFun g := ⟨g.1, g.2⟩
+  invFun g := ⟨⟨g.1, h g.2⟩, g.2⟩
+  left_inv _g := Subtype.ext (Subtype.ext rfl)
+  right_inv _g := Subtype.ext rfl
+  map_mul' _g _h := rfl
+
+@[to_additive (attr := simp)]
+theorem comap_subtype (H K : Subgroup G) : H.comap K.subtype = H.subgroupOf K :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem comap_inclusion_subgroupOf {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) :
+    (H.subgroupOf K₂).comap (inclusion h) = H.subgroupOf K₁ :=
+  rfl
+
+@[to_additive]
+theorem coe_subgroupOf (H K : Subgroup G) : (H.subgroupOf K : Set K) = K.subtype ⁻¹' H :=
+  rfl
+
+@[to_additive]
+theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h : G) ∈ H :=
+  Iff.rfl
+
+-- TODO(kmill): use `K ⊓ H` order for RHS to match `Subtype.image_preimage_coe`
+@[to_additive (attr := simp)]
+theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K :=
+  SetLike.ext' <| by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm
+
+@[to_additive (attr := simp)]
+theorem bot_subgroupOf : (⊥ : Subgroup G).subgroupOf H = ⊥ :=
+  Eq.symm (Subgroup.ext fun _g => Subtype.ext_iff)
+
+@[to_additive (attr := simp)]
+theorem top_subgroupOf : (⊤ : Subgroup G).subgroupOf H = ⊤ :=
+  rfl
+
+@[to_additive]
+theorem subgroupOf_bot_eq_bot : H.subgroupOf ⊥ = ⊥ :=
+  Subsingleton.elim _ _
+
+@[to_additive]
+theorem subgroupOf_bot_eq_top : H.subgroupOf ⊥ = ⊤ :=
+  Subsingleton.elim _ _
+
+@[to_additive (attr := simp)]
+theorem subgroupOf_self : H.subgroupOf H = ⊤ :=
+  top_unique fun g _hg => g.2
+
+@[to_additive (attr := simp)]
+theorem subgroupOf_inj {H₁ H₂ K : Subgroup G} :
+    H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K := by
+  simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall
+
+@[to_additive (attr := simp)]
+theorem inf_subgroupOf_right (H K : Subgroup G) : (H ⊓ K).subgroupOf K = H.subgroupOf K :=
+  subgroupOf_inj.2 (inf_right_idem _ _)
+
+@[to_additive (attr := simp)]
+theorem inf_subgroupOf_left (H K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K := by
+  rw [inf_comm, inf_subgroupOf_right]
+
+@[to_additive (attr := simp)]
+theorem subgroupOf_eq_bot {H K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K := by
+  rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]
+
+@[to_additive (attr := simp)]
+theorem subgroupOf_eq_top {H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H := by
+  rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]
+
+variable (H : Subgroup G)
+
+@[to_additive]
+instance map_isCommutative (f : G →* G') [H.IsCommutative] : (H.map f).IsCommutative :=
+  ⟨⟨by
+      rintro ⟨-, a, ha, rfl⟩ ⟨-, b, hb, rfl⟩
+      rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← map_mul, ← map_mul]
+      exact congr_arg f (Subtype.ext_iff.mp (mul_comm (⟨a, ha⟩ : H) ⟨b, hb⟩))⟩⟩
+
+@[to_additive]
+theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCommutative] :
+    (H.comap f).IsCommutative :=
+  ⟨⟨fun a b =>
+      Subtype.ext
+        (by
+          have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)
+          rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul,
+            hf.eq_iff] at this)⟩⟩
+
+@[to_additive]
+instance subgroupOf_isCommutative [H.IsCommutative] : (H.subgroupOf K).IsCommutative :=
+  H.comap_injective_isCommutative Subtype.coe_injective
+
+end Subgroup
+
+namespace MulEquiv
+variable {H : Type*} [Group H]
+
+/--
+An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
+defined by sending subgroups to their inverse images.
+
+See also `MulEquiv.mapSubgroup` which maps subgroups to their forward images.
+-/
+@[simps]
+def comapSubgroup (f : G ≃* H) : Subgroup H ≃o Subgroup G where
+  toFun := Subgroup.comap f
+  invFun := Subgroup.comap f.symm
+  left_inv sg := by simp [Subgroup.comap_comap]
+  right_inv sh := by simp [Subgroup.comap_comap]
+  map_rel_iff' {sg1 sg2} :=
+    ⟨fun h => by simpa [Subgroup.comap_comap] using
+      Subgroup.comap_mono (f := (f.symm : H →* G)) h, Subgroup.comap_mono⟩
+
+/--
+An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
+defined by sending subgroups to their forward images.
+
+See also `MulEquiv.comapSubgroup` which maps subgroups to their inverse images.
+-/
+@[simps]
+def mapSubgroup {H : Type*} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup H where
+  toFun := Subgroup.map f
+  invFun := Subgroup.map f.symm
+  left_inv sg := by simp [Subgroup.map_map]
+  right_inv sh := by simp [Subgroup.map_map]
+  map_rel_iff' {sg1 sg2} :=
+    ⟨fun h => by simpa [Subgroup.map_map] using
+      Subgroup.map_mono (f := (f.symm : H →* G)) h, Subgroup.map_mono⟩
+
+end MulEquiv
+
+namespace Subgroup
+
+open MonoidHom
+
+variable {N : Type*} [Group N] (f : G →* N)
+
+@[to_additive]
+theorem map_comap_le (H : Subgroup N) : map f (comap f H) ≤ H :=
+  (gc_map_comap f).l_u_le _
+
+@[to_additive]
+theorem le_comap_map (H : Subgroup G) : H ≤ comap f (map f H) :=
+  (gc_map_comap f).le_u_l _
+
+@[to_additive]
+theorem map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f)
+    (hr : Function.RightInverse g f) (H : Subgroup G) : map f H = comap g H :=
+  SetLike.ext' <| by rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]
+
+/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
+use `MulEquiv.subgroupMap` for better definitional equalities. -/
+@[to_additive
+      "An additive subgroup is isomorphic to its image under an injective function. If you
+      have an isomorphism, use `AddEquiv.addSubgroupMap` for better definitional equalities."]
+noncomputable def equivMapOfInjective (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
+    H ≃* H.map f :=
+  { Equiv.Set.image f H hf with map_mul' := fun _ _ => Subtype.ext (f.map_mul _ _) }
+
+@[to_additive (attr := simp)]
+theorem coe_equivMapOfInjective_apply (H : Subgroup G) (f : G →* N) (hf : Function.Injective f)
+    (h : H) : (equivMapOfInjective H f hf h : N) = f h :=
+  rfl
+
+end Subgroup
+
+variable {N : Type*} [Group N]
+
+namespace MonoidHom
+
+/-- The `MonoidHom` from the preimage of a subgroup to itself. -/
+@[to_additive (attr := simps!) "the `AddMonoidHom` from the preimage of an
+additive subgroup to itself."]
+def subgroupComap (f : G →* G') (H' : Subgroup G') : H'.comap f →* H' :=
+  f.submonoidComap H'.toSubmonoid
+
+/-- The `MonoidHom` from a subgroup to its image. -/
+@[to_additive (attr := simps!) "the `AddMonoidHom` from an additive subgroup to its image"]
+def subgroupMap (f : G →* G') (H : Subgroup G) : H →* H.map f :=
+  f.submonoidMap H.toSubmonoid
+
+@[to_additive]
+theorem subgroupMap_surjective (f : G →* G') (H : Subgroup G) :
+    Function.Surjective (f.subgroupMap H) :=
+  f.submonoidMap_surjective H.toSubmonoid
+
+end MonoidHom
+
+namespace MulEquiv
+
+variable {H K : Subgroup G}
+
+/-- Makes the identity isomorphism from a proof two subgroups of a multiplicative
+    group are equal. -/
+@[to_additive
+      "Makes the identity additive isomorphism from a proof
+      two subgroups of an additive group are equal."]
+def subgroupCongr (h : H = K) : H ≃* K :=
+  { Equiv.setCongr <| congr_arg _ h with map_mul' := fun _ _ => rfl }
+
+@[to_additive (attr := simp)]
+lemma subgroupCongr_apply (h : H = K) (x) :
+    (MulEquiv.subgroupCongr h x : G) = x := rfl
+
+@[to_additive (attr := simp)]
+lemma subgroupCongr_symm_apply (h : H = K) (x) :
+    ((MulEquiv.subgroupCongr h).symm x : G) = x := rfl
+
+/-- A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
+use `Subgroup.equiv_map_of_injective`. -/
+@[to_additive
+      "An additive subgroup is isomorphic to its image under an isomorphism. If you only
+      have an injective map, use `AddSubgroup.equiv_map_of_injective`."]
+def subgroupMap (e : G ≃* G') (H : Subgroup G) : H ≃* H.map (e : G →* G') :=
+  MulEquiv.submonoidMap (e : G ≃* G') H.toSubmonoid
+
+@[to_additive (attr := simp)]
+theorem coe_subgroupMap_apply (e : G ≃* G') (H : Subgroup G) (g : H) :
+    ((subgroupMap e H g : H.map (e : G →* G')) : G') = e g :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem subgroupMap_symm_apply (e : G ≃* G') (H : Subgroup G) (g : H.map (e : G →* G')) :
+    (e.subgroupMap H).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩ :=
+  rfl
+
+end MulEquiv
+
+namespace MonoidHom
+
+open Subgroup
+
+@[to_additive]
+theorem closure_preimage_le (f : G →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
+  (closure_le _).2 fun x hx => by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx
+
+/-- The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup
+generated by the image of the set. -/
+@[to_additive
+      "The image under an `AddMonoid` hom of the `AddSubgroup` generated by a set equals
+      the `AddSubgroup` generated by the image of the set."]
+theorem map_closure (f : G →* N) (s : Set G) : (closure s).map f = closure (f '' s) :=
+  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subgroup.gi N).gc (Subgroup.gi G).gc
+    fun _ ↦ rfl
+
+end MonoidHom
+
+namespace Subgroup
+
+@[to_additive (attr := simp)]
+theorem equivMapOfInjective_coe_mulEquiv (H : Subgroup G) (e : G ≃* G') :
+    H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H := by
+  ext
+  rfl
+
+end Subgroup
diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
index cf8febc23281b..357b32013f358 100644
--- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
@@ -3,7 +3,8 @@ Copyright (c) 2020 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Int
+import Mathlib.Algebra.Group.Subgroup.Map
 
 /-!
 # Subgroups generated by an element
diff --git a/Mathlib/Algebra/Group/Submonoid/Units.lean b/Mathlib/Algebra/Group/Submonoid/Units.lean
index 96ce6d155d1e4..111adf47e20ff 100644
--- a/Mathlib/Algebra/Group/Submonoid/Units.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Units.lean
@@ -5,7 +5,7 @@ Authors: Wrenna Robson
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Group.Submonoid.Pointwise
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Lattice
 
 /-!
 
diff --git a/Mathlib/Algebra/Module/Submodule/Ker.lean b/Mathlib/Algebra/Module/Submodule/Ker.lean
index b291dd847675d..dfa7ba1ee50ad 100644
--- a/Mathlib/Algebra/Module/Submodule/Ker.lean
+++ b/Mathlib/Algebra/Module/Submodule/Ker.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Frédéric Dupuis,
   Heather Macbeth
 -/
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Algebra.Module.Submodule.Map
 
 /-!
diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean
index 8a537d9a01ba5..76744e1fa2be2 100644
--- a/Mathlib/Algebra/Module/Submodule/Lattice.lean
+++ b/Mathlib/Algebra/Module/Submodule/Lattice.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Lattice
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.Module.Submodule.Defs
 import Mathlib.Algebra.Module.Equiv.Defs
diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
index bf9a103f9a34a..ac43875d2bd8a 100644
--- a/Mathlib/Algebra/Module/Submodule/Map.lean
+++ b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Frédéric Dupuis,
   Heather Macbeth
 -/
-
+import Mathlib.Algebra.Group.Subgroup.Map
 import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.LinearMap
diff --git a/Mathlib/Algebra/Order/Archimedean/Basic.lean b/Mathlib/Algebra/Order/Archimedean/Basic.lean
index 7756989822b78..c2c50a58878f6 100644
--- a/Mathlib/Algebra/Order/Archimedean/Basic.lean
+++ b/Mathlib/Algebra/Order/Archimedean/Basic.lean
@@ -30,6 +30,8 @@ number `n` such that `x ≤ n • y`.
 * `ℕ`, `ℤ`, and `ℚ` are archimedean.
 -/
 
+assert_not_exists Finset
+
 open Int Set
 
 variable {α : Type*}
diff --git a/Mathlib/Algebra/Order/Archimedean/Hom.lean b/Mathlib/Algebra/Order/Archimedean/Hom.lean
index c4e7b11c89739..03816d8b0f244 100644
--- a/Mathlib/Algebra/Order/Archimedean/Hom.lean
+++ b/Mathlib/Algebra/Order/Archimedean/Hom.lean
@@ -14,6 +14,8 @@ ordered field. Reciprocally, such an ordered ring homomorphism exists when the c
 conditionally complete.
 -/
 
+assert_not_exists Finset
+
 variable {α β : Type*}
 
 /-- There is at most one ordered ring homomorphism from a linear ordered field to an archimedean
diff --git a/Mathlib/Algebra/Order/Archimedean/Submonoid.lean b/Mathlib/Algebra/Order/Archimedean/Submonoid.lean
index fccc02aa01ab0..b30d6bec3e7ff 100644
--- a/Mathlib/Algebra/Order/Archimedean/Submonoid.lean
+++ b/Mathlib/Algebra/Order/Archimedean/Submonoid.lean
@@ -22,6 +22,8 @@ submonoid of the ambient group.
   submonoid.
 -/
 
+assert_not_exists Finset
+
 @[to_additive]
 instance SubmonoidClass.instMulArchimedean {M S : Type*} [SetLike S M] [OrderedCommMonoid M]
     [SubmonoidClass S M] [MulArchimedean M] (H : S) : MulArchimedean H := by
diff --git a/Mathlib/Algebra/Order/Chebyshev.lean b/Mathlib/Algebra/Order/Chebyshev.lean
index b0be97b492f03..d359503ea08c9 100644
--- a/Mathlib/Algebra/Order/Chebyshev.lean
+++ b/Mathlib/Algebra/Order/Chebyshev.lean
@@ -7,8 +7,7 @@ import Mathlib.Algebra.Order.Monovary
 import Mathlib.Algebra.Order.Rearrangement
 import Mathlib.GroupTheory.Perm.Cycle.Basic
 import Mathlib.Tactic.GCongr
-import Mathlib.Tactic.Positivity.Basic
-import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Tactic.Positivity
 
 /-!
 # Chebyshev's sum inequality
diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean
index 5e5aaf78be137..d3d6e7b16dc1d 100644
--- a/Mathlib/Algebra/Order/Floor.lean
+++ b/Mathlib/Algebra/Order/Floor.lean
@@ -13,7 +13,7 @@ import Mathlib.Order.GaloisConnection
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Positivity.Basic
 
 /-!
 # Floor and ceil
@@ -54,6 +54,8 @@ many lemmas.
 rounding, floor, ceil
 -/
 
+assert_not_exists Finset
+
 open Set
 
 variable {F α β : Type*}
diff --git a/Mathlib/Algebra/Order/Nonneg/Floor.lean b/Mathlib/Algebra/Order/Nonneg/Floor.lean
index a3472c9dde95b..1fdd9eefd1892 100644
--- a/Mathlib/Algebra/Order/Nonneg/Floor.lean
+++ b/Mathlib/Algebra/Order/Nonneg/Floor.lean
@@ -19,6 +19,8 @@ This is used to derive algebraic structures on `ℝ≥0` and `ℚ≥0` automatic
 * `{x : α // 0 ≤ x}` is a `FloorSemiring` if `α` is.
 -/
 
+assert_not_exists Finset
+
 namespace Nonneg
 
 variable {α : Type*}
diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
index 72fdec393def4..018e1506eb3ec 100644
--- a/Mathlib/Algebra/Ring/Parity.lean
+++ b/Mathlib/Algebra/Ring/Parity.lean
@@ -113,6 +113,8 @@ lemma Odd.add_odd : Odd a → Odd b → Even (a + b) := by
 
 @[simp] lemma Even.add_one (h : Even a) : Odd (a + 1) := h.add_odd odd_one
 @[simp] lemma Even.one_add (h : Even a) : Odd (1 + a) := h.odd_add odd_one
+@[simp] lemma Odd.add_one (h : Odd a) : Even (a + 1) := h.add_odd odd_one
+@[simp] lemma Odd.one_add (h : Odd a) : Even (1 + a) := odd_one.add_odd h
 
 lemma odd_two_mul_add_one (a : α) : Odd (2 * a + 1) := ⟨_, rfl⟩
 
diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean
index c9a57e5bb6985..6efcaa447e727 100644
--- a/Mathlib/Analysis/Analytic/Inverse.lean
+++ b/Mathlib/Analysis/Analytic/Inverse.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Analytic.Composition
 import Mathlib.Analysis.Analytic.Linear
-import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Tactic.Positivity
 
 /-!
 
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean
index 6b5f7dc3f86f0..3bc95aa8d8223 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean
@@ -678,7 +678,7 @@ theorem HasFDerivAt.list_prod' {l : List ι} {x : E}
         smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x := by
   simp only [← List.finRange_map_get l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
-    (hasFDerivAt_pi.mpr fun i ↦ h l[i] (List.getElem_mem i.isLt))) ?_
+    (hasFDerivAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem _))) ?_
   ext m
   simp [← List.map_map]
 
@@ -690,7 +690,7 @@ theorem HasFDerivWithinAt.list_prod' {l : List ι} {x : E}
         smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) s x := by
   simp only [← List.finRange_map_get l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
-    (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem i.isLt))) ?_
+    (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem _))) ?_
   ext m
   simp [← List.map_map]
 
diff --git a/Mathlib/Analysis/Calculus/Monotone.lean b/Mathlib/Analysis/Calculus/Monotone.lean
index 599a701b6b211..f54f48fe98117 100644
--- a/Mathlib/Analysis/Calculus/Monotone.lean
+++ b/Mathlib/Analysis/Calculus/Monotone.lean
@@ -108,7 +108,7 @@ theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) :
       filter_upwards [this]
       rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
       rw [mem_Iio]
-      norm_num; nlinarith
+      nlinarith
   -- Deduce the correct limit on the left, by sandwiching.
   have L4 :
     Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv f.measure volume x).toReal) := by
@@ -118,7 +118,7 @@ theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) :
       refine div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 ?_)
       apply f.mono.le_leftLim
       have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
-      norm_num; linarith
+      linarith
     · filter_upwards [self_mem_nhdsWithin]
       rintro y (hy : y < x)
       refine div_le_div_of_nonpos_of_le (by linarith) ?_
@@ -161,7 +161,7 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
         filter_upwards [this]
         rintro y ⟨hy : x < y, h'y : y < x + 1⟩
         rw [mem_Ioi]
-        norm_num; nlinarith
+        nlinarith
     -- apply the sandwiching argument, with the helper function and `g`
     apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
     · filter_upwards [self_mem_nhdsWithin] with y hy
@@ -190,7 +190,7 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
         rintro y hy
         rw [mem_Ioo] at hy
         rw [mem_Iio]
-        norm_num; nlinarith
+        nlinarith
     -- apply the sandwiching argument, with `g` and the helper function
     apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
     · filter_upwards [self_mem_nhdsWithin]
@@ -203,7 +203,7 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
       rw [mem_Iio, ← sub_neg] at hy
       have : 0 < (y - x) ^ 2 := sq_pos_of_neg hy
       apply div_le_div_of_nonpos_of_le hy.le
-      exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
+      exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by linarith))
   -- conclude global differentiability
   rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, (nhds_left'_sup_nhds_right' x).symm,
     tendsto_sup]
diff --git a/Mathlib/Analysis/Complex/AbelLimit.lean b/Mathlib/Analysis/Complex/AbelLimit.lean
index 25d7f649514c6..7e5aea15a8967 100644
--- a/Mathlib/Analysis/Complex/AbelLimit.lean
+++ b/Mathlib/Analysis/Complex/AbelLimit.lean
@@ -6,7 +6,7 @@ Authors: Jeremy Tan
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.SpecificLimits.Normed
 import Mathlib.Tactic.Peel
-import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Tactic.Positivity
 
 /-!
 # Abel's limit theorem
diff --git a/Mathlib/Analysis/Convex/Uniform.lean b/Mathlib/Analysis/Convex/Uniform.lean
index cbea3a0fbb080..5c0511976660c 100644
--- a/Mathlib/Analysis/Convex/Uniform.lean
+++ b/Mathlib/Analysis/Convex/Uniform.lean
@@ -96,16 +96,7 @@ theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :
     _ ≤ 2 - δ + δ' + δ' :=
       (add_le_add_three (h (h₁ _ hx') (h₁ _ hy') hxy') (h₂ _ hx hx'.le) (h₂ _ hy hy'.le))
     _ ≤ 2 - δ' := by
-      dsimp only [δ']
-      rw [← le_sub_iff_add_le, ← le_sub_iff_add_le, sub_sub, sub_sub]
-      refine sub_le_sub_left ?_ _
-      ring_nf
-      rw [← mul_div_cancel₀ δ three_ne_zero]
-      norm_num
-      -- Porting note: these three extra lines needed to make `exact` work
-      have : 3 * (δ / 3) * (1 / 3) = δ / 3 := by linarith
-      rw [this, mul_comm]
-      gcongr
+      suffices δ' ≤ δ / 3 by linarith
       exact min_le_of_right_le <| min_le_right _ _
 
 theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :
diff --git a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
index 12f3131cc2e8b..8244981055401 100644
--- a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
+++ b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
@@ -680,7 +680,15 @@ theorem eLpNorm_le_eLpNorm_fderiv_of_le [FiniteDimensional ℝ F]
   have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ := by
     rw [inv_inv, NNReal.coe_sub]
     · simp
-    · gcongr
+    · #adaptation_note
+      /-- This should just be `gcongr`, but this is not working as of nightly-2024-11-20. -/
+      exact
+      inv_anti₀
+        (lt_of_lt_of_le
+          (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ≥0 Nat.cast_one)
+            (Eq.refl (Nat.ble 1 1)))
+          hp)
+        (le_of_lt h2p)
   have : (q : ℝ≥0∞) ≤ p' := by
     have H : (p' : ℝ)⁻¹ ≤ (↑q)⁻¹ := trans hp' hpq
     norm_cast at H ⊢
@@ -688,7 +696,15 @@ theorem eLpNorm_le_eLpNorm_fderiv_of_le [FiniteDimensional ℝ F]
     · dsimp
       have : 0 < p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹ := by
         simp only [tsub_pos_iff_lt]
-        gcongr
+        #adaptation_note
+        /-- This should just be `gcongr`, but this is not working as of nightly-2024-11-20. -/
+        exact
+          inv_strictAnti₀
+            (lt_of_lt_of_le
+              (Mathlib.Meta.Positivity.pos_of_isNat
+                (Mathlib.Meta.NormNum.isNat_ofNat ℝ≥0 Nat.cast_one) (Eq.refl (Nat.ble 1 1)))
+              hp)
+            h2p
       positivity
     · positivity
   set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index 4242b77e0dfd6..91cdbe19d79a5 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl, Yaël Dillies
 -/
 import Mathlib.Algebra.CharP.Defs
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Analysis.Normed.Group.Seminorm
 import Mathlib.Topology.Metrizable.Uniformity
 import Mathlib.Topology.Sequences
diff --git a/Mathlib/Analysis/Normed/Group/Seminorm.lean b/Mathlib/Analysis/Normed/Group/Seminorm.lean
index 38c8d7fee64ca..e895bf01b8d3c 100644
--- a/Mathlib/Analysis/Normed/Group/Seminorm.lean
+++ b/Mathlib/Analysis/Normed/Group/Seminorm.lean
@@ -44,6 +44,7 @@ having a superfluous `add_le'` field in the resulting structure. The same applie
 norm, seminorm
 -/
 
+assert_not_exists Finset
 
 open Set
 
diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean
index b077709ddf4da..93a65386cf5e2 100644
--- a/Mathlib/Analysis/PSeries.lean
+++ b/Mathlib/Analysis/PSeries.lean
@@ -386,12 +386,9 @@ theorem sum_Ioc_inv_sq_le_sub {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) :
   simp only [sub_eq_add_neg, add_assoc, Nat.cast_add, Nat.cast_one, le_add_neg_iff_add_le,
     add_le_iff_nonpos_right, neg_add_le_iff_le_add, add_zero]
   have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
-  have B : 0 < (n : α) + 1 := by linarith
   field_simp
-  rw [div_le_div_iff₀ _ A, ← sub_nonneg]
-  · ring_nf
-    rw [add_comm]
-    exact B.le
+  rw [div_le_div_iff₀ _ A]
+  · linarith
   · -- Porting note: was `nlinarith`
     positivity
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
index 86a1929d236cc..6a9a40ef2d4ff 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
@@ -57,7 +57,7 @@ theorem Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma {s t a b : ℝ} (hs : 0 <
   let f : ℝ → ℝ → ℝ → ℝ := fun c u x => exp (-c * x) * x ^ (c * (u - 1))
   have e : IsConjExponent (1 / a) (1 / b) := Real.isConjExponent_one_div ha hb hab
   have hab' : b = 1 - a := by linarith
-  have hst : 0 < a * s + b * t := add_pos (mul_pos ha hs) (mul_pos hb ht)
+  have hst : 0 < a * s + b * t := by positivity
   -- some properties of f:
   have posf : ∀ c u x : ℝ, x ∈ Ioi (0 : ℝ) → 0 ≤ f c u x := fun c u x hx =>
     mul_nonneg (exp_pos _).le (rpow_pos_of_pos hx _).le
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
index 5aa71529e87e1..c6b70bd4eaffa 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
@@ -53,11 +53,9 @@ theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
   intro x hex y _ hxy
   have x_pos : 0 < x := lt_of_lt_of_le (exp_pos (1 / a)) hex
   have y_pos : 0 < y := by linarith
-  have x_nonneg : 0 ≤ x := le_trans (le_of_lt (exp_pos (1 / a))) hex
-  have y_nonneg : 0 ≤ y := by linarith
   nth_rw 1 [← rpow_one y]
   nth_rw 1 [← rpow_one x]
-  rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_nonneg, rpow_mul x_nonneg,
+  rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_pos.le, rpow_mul x_pos.le,
     log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
     mul_div_assoc, mul_le_mul_left (one_div_pos.mpr ha)]
   refine log_div_self_antitoneOn ?_ ?_ ?_
@@ -65,14 +63,14 @@ theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
     convert rpow_le_rpow _ hex (le_of_lt ha) using 1
     · rw [← exp_mul]
       simp only [Real.exp_eq_exp]
-      field_simp [(ne_of_lt ha).symm]
-    exact le_of_lt (exp_pos (1 / a))
+      field_simp
+    positivity
   · simp only [Set.mem_setOf_eq]
     convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
     · rw [← exp_mul]
       simp only [Real.exp_eq_exp]
-      field_simp [(ne_of_lt ha).symm]
-    exact le_of_lt (exp_pos (1 / a))
+      field_simp
+    positivity
   gcongr
 
 theorem log_div_sqrt_antitoneOn : AntitoneOn (fun x : ℝ => log x / √x) { x | exp 2 ≤ x } := by
diff --git a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
index aed53500fa639..88db5d1e3d0c9 100644
--- a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
+++ b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
@@ -10,7 +10,6 @@ import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.Positivity
-import Mathlib.Tactic.Positivity.Finset
 import Mathlib.Tactic.Ring
 
 /-!
diff --git a/Mathlib/Combinatorics/Derangements/Basic.lean b/Mathlib/Combinatorics/Derangements/Basic.lean
index 9620588f45486..ac4e2f3b84276 100644
--- a/Mathlib/Combinatorics/Derangements/Basic.lean
+++ b/Mathlib/Combinatorics/Derangements/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Dynamics.FixedPoints.Basic
 import Mathlib.GroupTheory.Perm.Option
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Logic.Equiv.Option
+import Mathlib.Tactic.ApplyFun
 
 /-!
 # Derangements on types
diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean
index 20b7c32701611..e1bf3970d658a 100644
--- a/Mathlib/Combinatorics/Enumerative/Composition.lean
+++ b/Mathlib/Combinatorics/Enumerative/Composition.lean
@@ -150,7 +150,7 @@ theorem sum_blocksFun : ∑ i, c.blocksFun i = n := by
   conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
 
 theorem blocksFun_mem_blocks (i : Fin c.length) : c.blocksFun i ∈ c.blocks :=
-  getElem_mem _
+  get_mem _ _
 
 @[simp]
 theorem one_le_blocks {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i :=
@@ -158,7 +158,7 @@ theorem one_le_blocks {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i :=
 
 @[simp]
 theorem one_le_blocks' {i : ℕ} (h : i < c.length) : 1 ≤ c.blocks[i] :=
-  c.one_le_blocks (getElem_mem h)
+  c.one_le_blocks (get_mem (blocks c) _)
 
 @[simp]
 theorem blocks_pos' (i : ℕ) (h : i < c.length) : 0 < c.blocks[i] :=
diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
index a5d36c33b508b..6d675a7865092 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
@@ -10,7 +10,6 @@ import Mathlib.Combinatorics.SimpleGraph.Clique
 import Mathlib.Data.Finset.Sym
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.Positivity
-import Mathlib.Tactic.Positivity.Finset
 
 /-!
 # Triangles in graphs
diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean
index 96836f66517c4..120674ea5f000 100644
--- a/Mathlib/Data/ENNReal/Basic.lean
+++ b/Mathlib/Data/ENNReal/Basic.lean
@@ -85,6 +85,7 @@ context, or if we have `(f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞)`.
 
 -/
 
+assert_not_exists Finset
 
 open Function Set NNReal
 
diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean
index b8d5585f00ed8..29e19adc50a21 100644
--- a/Mathlib/Data/Finset/Density.lean
+++ b/Mathlib/Data/Finset/Density.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Data.Fintype.Card
 import Mathlib.Data.NNRat.Order
 import Mathlib.Data.Rat.Cast.CharZero
-import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Positivity.Basic
 
 /-!
 # Density of a finite set
diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean
index 486acd9c00f1b..d4354b5039a5b 100644
--- a/Mathlib/Data/Finset/Sort.lean
+++ b/Mathlib/Data/Finset/Sort.lean
@@ -113,7 +113,7 @@ theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).le
     obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
     rw [← hi]
     exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.zero_le i)
-  · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.getElem_mem h)
+  · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
     exact s.min'_le _ this
 
 theorem sorted_zero_eq_min' {s : Finset α} {h : 0 < (s.sort (· ≤ ·)).length} :
@@ -130,7 +130,7 @@ theorem sorted_last_eq_max'_aux (s : Finset α)
   let l := s.sort (· ≤ ·)
   apply le_antisymm
   · have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s :=
-      (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.getElem_mem h)
+      (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
     exact s.le_max' _ this
   · have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H)
     obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
diff --git a/Mathlib/Data/Int/Log.lean b/Mathlib/Data/Int/Log.lean
index e6f5f9f457159..4d5f3c0e38722 100644
--- a/Mathlib/Data/Int/Log.lean
+++ b/Mathlib/Data/Int/Log.lean
@@ -46,6 +46,7 @@ def digits (b : ℕ) (q : ℚ) (n : ℕ) : ℕ :=
 * `Int.neg_log_inv_eq_clog`, `Int.neg_clog_inv_eq_log`: the link between the two definitions.
 -/
 
+assert_not_exists Finset
 
 variable {R : Type*} [LinearOrderedSemifield R] [FloorSemiring R]
 
diff --git a/Mathlib/Data/Int/WithZero.lean b/Mathlib/Data/Int/WithZero.lean
index 4a74559dbbf98..5cf5aebd6da66 100644
--- a/Mathlib/Data/Int/WithZero.lean
+++ b/Mathlib/Data/Int/WithZero.lean
@@ -26,6 +26,8 @@ the morphism `WithZeroMultInt.toNNReal`.
 WithZero, multiplicative, nnreal
 -/
 
+assert_not_exists Finset
+
 noncomputable section
 
 open scoped NNReal
diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean
index 876e1a2130482..34485c3ee467f 100644
--- a/Mathlib/Data/List/Cycle.lean
+++ b/Mathlib/Data/List/Cycle.lean
@@ -217,7 +217,7 @@ theorem prev_ne_cons_cons (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz
   · rw [prev, dif_neg hy, if_neg hz]
 
 theorem next_mem (h : x ∈ l) : l.next x h ∈ l :=
-  nextOr_mem (getElem_mem _)
+  nextOr_mem (get_mem _ _)
 
 theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by
   cases' l with hd tl
@@ -233,7 +233,7 @@ theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by
       · exact mem_cons_of_mem _ (hl _ _)
 
 theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) :
-    next l (l.get i) (getElem_mem _) =
+    next l (l.get i) (get_mem _ _) =
       l.get ⟨(i + 1) % l.length, Nat.mod_lt _ (i.1.zero_le.trans_lt i.2)⟩ :=
   match l, h, i with
   | [], _, i => by simpa using i.2
@@ -254,7 +254,7 @@ theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) :
     · subst hi'
       rw [next_getLast_cons]
       · simp [hi', get]
-      · rw [get_cons_succ]; exact getElem_mem _
+      · rw [get_cons_succ]; exact get_mem _ _
       · exact hx'
       · simp [getLast_eq_getElem]
       · exact hn.of_cons
@@ -271,12 +271,12 @@ theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) :
         intro h
         have := nodup_iff_injective_get.1 hn h
         simp at this; simp [this] at hi'
-      · rw [get_cons_succ]; exact getElem_mem _
+      · rw [get_cons_succ]; exact get_mem _ _
 
 -- Unused variable linter incorrectly reports that `h` is unused here.
 set_option linter.unusedVariables false in
 theorem prev_get (l : List α) (h : Nodup l) (i : Fin l.length) :
-    prev l (l.get i) (getElem_mem _) =
+    prev l (l.get i) (get_mem _ _) =
       l.get ⟨(i + (l.length - 1)) % l.length, Nat.mod_lt _ i.pos⟩ :=
   match l with
   | [] => by simpa using i.2
diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean
index fbcf74a9eec72..b355f9e72ed52 100644
--- a/Mathlib/Data/List/NodupEquivFin.lean
+++ b/Mathlib/Data/List/NodupEquivFin.lean
@@ -49,7 +49,7 @@ variable [DecidableEq α]
 the set of elements of `l`. -/
 @[simps]
 def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l } where
-  toFun i := ⟨get l i, getElem_mem i.2⟩
+  toFun i := ⟨get l i, get_mem _ _⟩
   invFun x := ⟨indexOf (↑x) l, indexOf_lt_length.2 x.2⟩
   left_inv i := by simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H]
   right_inv x := by simp
diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index 9fffafbea6995..02d70c2c3d123 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -19,6 +19,8 @@ Note that we cannot talk about `Int.fract`, which currently only works for rings
 nnrat, rationals, ℚ≥0, floor
 -/
 
+assert_not_exists Finset
+
 namespace NNRat
 
 instance : FloorSemiring ℚ≥0 where
diff --git a/Mathlib/Data/NNReal/Star.lean b/Mathlib/Data/NNReal/Star.lean
index c1f11b1539a4e..47c6a75c17849 100644
--- a/Mathlib/Data/NNReal/Star.lean
+++ b/Mathlib/Data/NNReal/Star.lean
@@ -10,6 +10,8 @@ import Mathlib.Data.Real.Star
 # The non-negative real numbers are a `*`-ring, with the trivial `*`-structure
 -/
 
+assert_not_exists Finset
+
 open scoped NNReal
 
 instance : StarRing ℝ≥0 := starRingOfComm
diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean
index 66006dd0fc062..7b67abd634887 100644
--- a/Mathlib/Data/Rat/Floor.lean
+++ b/Mathlib/Data/Rat/Floor.lean
@@ -21,6 +21,7 @@ division and modulo arithmetic are derived as well as some simple inequalities.
 rat, rationals, ℚ, floor
 -/
 
+assert_not_exists Finset
 
 open Int
 
diff --git a/Mathlib/Data/Real/Archimedean.lean b/Mathlib/Data/Real/Archimedean.lean
index 55226e28d84b8..a42f86a993916 100644
--- a/Mathlib/Data/Real/Archimedean.lean
+++ b/Mathlib/Data/Real/Archimedean.lean
@@ -14,6 +14,8 @@ import Mathlib.Order.Interval.Set.Disjoint
 
 -/
 
+assert_not_exists Finset
+
 open scoped Classical
 open Pointwise CauSeq
 
diff --git a/Mathlib/Data/Real/ENatENNReal.lean b/Mathlib/Data/Real/ENatENNReal.lean
index 9385bd57ec211..f022dc59fe0b4 100644
--- a/Mathlib/Data/Real/ENatENNReal.lean
+++ b/Mathlib/Data/Real/ENatENNReal.lean
@@ -12,6 +12,7 @@ import Mathlib.Data.ENNReal.Basic
 In this file we define a coercion from `ℕ∞` to `ℝ≥0∞` and prove some basic lemmas about this map.
 -/
 
+assert_not_exists Finset
 
 open scoped Classical
 open NNReal ENNReal
diff --git a/Mathlib/Data/Real/Pointwise.lean b/Mathlib/Data/Real/Pointwise.lean
index 8672dab314d36..e071edd0c5ddc 100644
--- a/Mathlib/Data/Real/Pointwise.lean
+++ b/Mathlib/Data/Real/Pointwise.lean
@@ -22,6 +22,7 @@ This is true more generally for conditionally complete linear order whose defaul
 don't have those yet.
 -/
 
+assert_not_exists Finset
 
 open Set
 
diff --git a/Mathlib/Data/Vector/Mem.lean b/Mathlib/Data/Vector/Mem.lean
index 9cf9359b65623..dc09c5bb58415 100644
--- a/Mathlib/Data/Vector/Mem.lean
+++ b/Mathlib/Data/Vector/Mem.lean
@@ -22,7 +22,7 @@ namespace Vector
 variable {α β : Type*} {n : ℕ} (a a' : α)
 
 @[simp]
-theorem get_mem (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList := List.getElem_mem _
+theorem get_mem (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList := List.get_mem _ _
 
 theorem mem_iff_get (v : Vector α n) : a ∈ v.toList ↔ ∃ i, v.get i = a := by
   simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get]
diff --git a/Mathlib/GroupTheory/Archimedean.lean b/Mathlib/GroupTheory/Archimedean.lean
index c31b5072d4f20..e67010ff8ade4 100644
--- a/Mathlib/GroupTheory/Archimedean.lean
+++ b/Mathlib/GroupTheory/Archimedean.lean
@@ -31,6 +31,8 @@ The result is also used in `Topology.Instances.Real` as an ingredient in the cla
 subgroups of `ℝ`.
 -/
 
+assert_not_exists Finset
+
 open Set
 variable {G : Type*} [LinearOrderedCommGroup G] [MulArchimedean G]
 
diff --git a/Mathlib/GroupTheory/Coprod/Basic.lean b/Mathlib/GroupTheory/Coprod/Basic.lean
index 084c569e85fa9..93e15e7696015 100644
--- a/Mathlib/GroupTheory/Coprod/Basic.lean
+++ b/Mathlib/GroupTheory/Coprod/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.PUnitInstances.Algebra
 import Mathlib.GroupTheory.Congruence.Basic
diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean
index 35f5a97da6e4a..d365be175ae24 100644
--- a/Mathlib/GroupTheory/FreeGroup/Basic.lean
+++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.List.Sublists
 
diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean
index ed5ab1ed24c4a..ae7eaef28b78d 100644
--- a/Mathlib/GroupTheory/GroupAction/Basic.lean
+++ b/Mathlib/GroupTheory/GroupAction/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Map
 import Mathlib.Data.Finite.Sigma
 import Mathlib.Data.Set.Finite.Basic
 import Mathlib.Data.Set.Finite.Range
diff --git a/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean b/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
index f968df45e92a9..38834797ad222 100644
--- a/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
+++ b/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Antoine Chambert-Loir. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Lattice
 import Mathlib.GroupTheory.GroupAction.FixedPoints
 
 /-!
diff --git a/Mathlib/GroupTheory/Perm/ClosureSwap.lean b/Mathlib/GroupTheory/Perm/ClosureSwap.lean
index b00b89f6c6ce7..2256c8a2e0210 100644
--- a/Mathlib/GroupTheory/Perm/ClosureSwap.lean
+++ b/Mathlib/GroupTheory/Perm/ClosureSwap.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Thomas Browning, Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Junyan Xu
 -/
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.FixedPoints
 import Mathlib.GroupTheory.Perm.Support
diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
index d09dd86518f64..bfb55453b7c78 100644
--- a/Mathlib/GroupTheory/Perm/Sign.lean
+++ b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -3,14 +3,15 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Conj
+import Mathlib.Algebra.Group.Subgroup.Lattice
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.Ring.Int.Units
 import Mathlib.Data.Finset.Fin
 import Mathlib.Data.Finset.Sort
+import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Sum
 import Mathlib.Data.Int.Order.Units
-import Mathlib.Data.Fintype.Prod
 import Mathlib.GroupTheory.Perm.Support
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.Tactic.NormNum.Ineq
diff --git a/Mathlib/GroupTheory/PresentedGroup.lean b/Mathlib/GroupTheory/PresentedGroup.lean
index ddfb60a247e99..dccb34fb884fd 100644
--- a/Mathlib/GroupTheory/PresentedGroup.lean
+++ b/Mathlib/GroupTheory/PresentedGroup.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Michael Howes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Howes, Newell Jensen
 -/
+import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.GroupTheory.FreeGroup.Basic
 import Mathlib.GroupTheory.QuotientGroup.Defs
 
diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
index f193d7652942f..d33a94cc017c6 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -5,7 +5,7 @@ Authors: Kevin Buzzard, Patrick Massot
 -/
 -- This file is to a certain extent based on `quotient_module.lean` by Johannes Hölzl.
 
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.GroupTheory.Congruence.Hom
 import Mathlib.GroupTheory.Coset.Defs
 
diff --git a/Mathlib/GroupTheory/SemidirectProduct.lean b/Mathlib/GroupTheory/SemidirectProduct.lean
index f3ac71a7ce4c7..f89efaef708f7 100644
--- a/Mathlib/GroupTheory/SemidirectProduct.lean
+++ b/Mathlib/GroupTheory/SemidirectProduct.lean
@@ -3,7 +3,8 @@ Copyright (c) 2020 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Aut
+import Mathlib.Algebra.Group.Subgroup.Ker
 
 /-!
 # Semidirect product
diff --git a/Mathlib/GroupTheory/Subgroup/Saturated.lean b/Mathlib/GroupTheory/Subgroup/Saturated.lean
index 6cbc7b2c45d71..e68e30ed0f303 100644
--- a/Mathlib/GroupTheory/Subgroup/Saturated.lean
+++ b/Mathlib/GroupTheory/Subgroup/Saturated.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Ker
 import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
diff --git a/Mathlib/LinearAlgebra/Ray.lean b/Mathlib/LinearAlgebra/Ray.lean
index 7890952886f09..d569b5c080c98 100644
--- a/Mathlib/LinearAlgebra/Ray.lean
+++ b/Mathlib/LinearAlgebra/Ray.lean
@@ -6,7 +6,7 @@ Authors: Joseph Myers
 import Mathlib.Algebra.Order.Module.Algebra
 import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.Algebra.Ring.Subring.Units
-import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Positivity.Basic
 
 /-!
 # Rays in modules
diff --git a/Mathlib/MeasureTheory/Measure/Count.lean b/Mathlib/MeasureTheory/Measure/Count.lean
index b91e37e621e4a..6d5d487517d6d 100644
--- a/Mathlib/MeasureTheory/Measure/Count.lean
+++ b/Mathlib/MeasureTheory/Measure/Count.lean
@@ -98,33 +98,21 @@ theorem count_apply_lt_top [MeasurableSingletonClass α] : count s < ∞ ↔ s.F
     _ ↔ ¬s.Infinite := not_congr count_apply_eq_top
     _ ↔ s.Finite := Classical.not_not
 
-theorem empty_of_count_eq_zero' (s_mble : MeasurableSet s) (hsc : count s = 0) : s = ∅ := by
-  have hs : s.Finite := by
-    rw [← count_apply_lt_top' s_mble, hsc]
-    exact WithTop.top_pos
-  simpa [count_apply_finite' hs s_mble] using hsc
-
-theorem empty_of_count_eq_zero [MeasurableSingletonClass α] (hsc : count s = 0) : s = ∅ := by
-  have hs : s.Finite := by
-    rw [← count_apply_lt_top, hsc]
-    exact WithTop.top_pos
-  simpa [count_apply_finite _ hs] using hsc
-
 @[simp]
-theorem count_eq_zero_iff' (s_mble : MeasurableSet s) : count s = 0 ↔ s = ∅ :=
-  ⟨empty_of_count_eq_zero' s_mble, fun h => h.symm ▸ count_empty⟩
+theorem count_eq_zero_iff : count s = 0 ↔ s = ∅ where
+  mp h := eq_empty_of_forall_not_mem fun x hx ↦ by
+    simpa [hx] using ((ENNReal.le_tsum x).trans <| le_sum_apply _ _).trans_eq h
+  mpr := by rintro rfl; exact count_empty
 
-@[simp]
-theorem count_eq_zero_iff [MeasurableSingletonClass α] : count s = 0 ↔ s = ∅ :=
-  ⟨empty_of_count_eq_zero, fun h => h.symm ▸ count_empty⟩
+lemma count_ne_zero_iff : count s ≠ 0 ↔ s.Nonempty :=
+  count_eq_zero_iff.not.trans nonempty_iff_ne_empty.symm
 
-theorem count_ne_zero' (hs' : s.Nonempty) (s_mble : MeasurableSet s) : count s ≠ 0 := by
-  rw [Ne, count_eq_zero_iff' s_mble]
-  exact hs'.ne_empty
+alias ⟨_, count_ne_zero⟩ := count_ne_zero_iff
 
-theorem count_ne_zero [MeasurableSingletonClass α] (hs' : s.Nonempty) : count s ≠ 0 := by
-  rw [Ne, count_eq_zero_iff]
-  exact hs'.ne_empty
+@[deprecated (since := "2024-11-20")] alias ⟨empty_of_count_eq_zero, _⟩ := count_eq_zero_iff
+@[deprecated (since := "2024-11-20")] alias empty_of_count_eq_zero' := empty_of_count_eq_zero
+@[deprecated (since := "2024-11-20")] alias count_eq_zero_iff' := count_eq_zero_iff
+@[deprecated (since := "2024-11-20")] alias count_ne_zero' := count_ne_zero
 
 @[simp]
 theorem count_singleton' {a : α} (ha : MeasurableSet ({a} : Set α)) : count ({a} : Set α) = 1 := by
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 8cf14fc5dc9a6..3d62ba5101860 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -748,6 +748,11 @@ theorem coe_zero {_m : MeasurableSpace α} : ⇑(0 : Measure α) = 0 :=
   ext s hs
   simp [hs]
 
+@[simp] lemma _root_.MeasureTheory.OuterMeasure.toMeasure_eq_zero {ms : MeasurableSpace α}
+    {μ : OuterMeasure α} (h : ms ≤ μ.caratheodory) : μ.toMeasure h = 0 ↔ μ = 0 where
+  mp hμ := by ext s; exact le_bot_iff.1 <| (le_toMeasure_apply _ _ _).trans_eq congr($hμ s)
+  mpr := by rintro rfl; simp
+
 @[nontriviality]
 lemma apply_eq_zero_of_isEmpty [IsEmpty α] {_ : MeasurableSpace α} (μ : Measure α) (s : Set α) :
     μ s = 0 := by
@@ -1274,10 +1279,11 @@ theorem sum_apply₀ (f : ι → Measure α) {s : Set α} (hs : NullMeasurableSe
 /-! For the next theorem, the countability assumption is necessary. For a counterexample, consider
 an uncountable space, with a distinguished point `x₀`, and the sigma-algebra made of countable sets
 not containing `x₀`, and their complements. All points but `x₀` are measurable.
-Consider the sum of the Dirac masses at points different from `x₀`, and `s = x₀`. For any Dirac mass
-`δ_x`, we have `δ_x (x₀) = 0`, so `∑' x, δ_x (x₀) = 0`. On the other hand, the measure `sum δ_x`
-gives mass one to each point different from `x₀`, so it gives infinite mass to any measurable set
-containing `x₀` (as such a set is uncountable), and by outer regularity one get `sum δ_x {x₀} = ∞`.
+Consider the sum of the Dirac masses at points different from `x₀`, and `s = {x₀}`. For any Dirac
+mass `δ_x`, we have `δ_x (x₀) = 0`, so `∑' x, δ_x (x₀) = 0`. On the other hand, the measure
+`sum δ_x` gives mass one to each point different from `x₀`, so it gives infinite mass to any
+measurable set containing `x₀` (as such a set is uncountable), and by outer regularity one gets
+`sum δ_x {x₀} = ∞`.
 -/
 theorem sum_apply_of_countable [Countable ι] (f : ι → Measure α) (s : Set α) :
     sum f s = ∑' i, f i s := by
diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
index 22fc2f2d46e5e..0d34bda52b147 100644
--- a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
+++ b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
@@ -102,7 +102,7 @@ theorem exists_approx_aux (n : ℕ) (h : abv.IsAdmissible) :
       /-- This proof was nicer prior to https://github.com/leanprover/lean4/pull/4400.
       Please feel welcome to improve it, by avoiding use of `List.get` in favour of `GetElem`. -/
       have : ∀ i h, t ((Finset.univ.filter fun x ↦ t x = s).toList.get ⟨i, h⟩) = s := fun i h ↦
-        (Finset.mem_filter.mp (Finset.mem_toList.mp (List.getElem_mem h))).2
+        (Finset.mem_filter.mp (Finset.mem_toList.mp (List.get_mem _ ⟨i, h⟩))).2
       simp only [Nat.succ_eq_add_one, Finset.length_toList, List.get_eq_getElem] at this
       simp only [Nat.succ_eq_add_one, List.get_eq_getElem, Fin.coe_castLE]
       rw [this _ (Nat.lt_of_le_of_lt (Nat.le_of_lt_succ i₁.2) hs),
diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean
index 9fc7ee0822135..b5c6b98a175d6 100644
--- a/Mathlib/NumberTheory/FermatPsp.lean
+++ b/Mathlib/NumberTheory/FermatPsp.lean
@@ -197,10 +197,8 @@ private theorem psp_from_prime_psp {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_p
   have hi_p : 1 ≤ p := Nat.one_le_of_lt p_gt_two
   have hi_bsquared : 0 < b ^ 2 - 1 := by
     -- Porting note: was `by nlinarith [Nat.one_le_pow 2 b hi_b]`
-    have h0 := mul_le_mul b_ge_two b_ge_two zero_le_two hi_b.le
-    have h1 : 1 < 2 * 2 := by omega
-    have := tsub_pos_of_lt (h1.trans_le h0)
-    rwa [pow_two]
+    have := Nat.pow_le_pow_left b_ge_two 2
+    omega
   have hi_bpowtwop : 1 ≤ b ^ (2 * p) := Nat.one_le_pow (2 * p) b hi_b
   have hi_bpowpsubone : 1 ≤ b ^ (p - 1) := Nat.one_le_pow (p - 1) b hi_b
   -- Other useful facts
diff --git a/Mathlib/NumberTheory/Harmonic/Defs.lean b/Mathlib/NumberTheory/Harmonic/Defs.lean
index 51c8f7036e358..29d3f5fa6bbe5 100644
--- a/Mathlib/NumberTheory/Harmonic/Defs.lean
+++ b/Mathlib/NumberTheory/Harmonic/Defs.lean
@@ -5,7 +5,7 @@ Authors: Koundinya Vajjha, Thomas Browning
 -/
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Tactic.Positivity
 
 /-!
 
diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
index f4c849d0063d4..ff3eef6b03cda 100644
--- a/Mathlib/NumberTheory/Modular.lean
+++ b/Mathlib/NumberTheory/Modular.lean
@@ -458,11 +458,8 @@ theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |g 1 0| 
       specialize this hc
       linarith
   intro hc
-  replace hc : 0 < c ^ 4 := by
-    change 0 < c ^ (2 * 2); rw [pow_mul]; apply sq_pos_of_pos (sq_pos_of_ne_zero hc)
-  have h₁ := mul_lt_mul_of_pos_right
-      (mul_lt_mul'' (three_lt_four_mul_im_sq_of_mem_fdo hg) (three_lt_four_mul_im_sq_of_mem_fdo hz)
-      (by norm_num) (by norm_num)) hc
+  have h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4 := by
+    gcongr <;> apply three_lt_four_mul_im_sq_of_mem_fdo <;> assumption
   have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
     div_le_one_of_le₀
       (pow_four_le_pow_two_of_pow_two_le (z.c_mul_im_sq_le_normSq_denom g))
diff --git a/Mathlib/Order/Max.lean b/Mathlib/Order/Max.lean
index 36518a3cb4aa5..7cf8fc7da8e5c 100644
--- a/Mathlib/Order/Max.lean
+++ b/Mathlib/Order/Max.lean
@@ -200,6 +200,14 @@ protected theorem IsBot.isMin (h : IsBot a) : IsMin a := fun b _ => h b
 
 protected theorem IsTop.isMax (h : IsTop a) : IsMax a := fun b _ => h b
 
+theorem IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i := by
+  simp_rw [le_antisymm_iff, h j, true_and]
+  exact ⟨(· (h j)), Function.swap (fun _ ↦ h · |>.trans ·)⟩
+
+theorem IsBot.isMin_iff {α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMin j ↔ j = i := by
+  simp_rw [le_antisymm_iff, h j, and_true]
+  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ Preorder.le_trans j i h' a (h h')⟩
+
 @[simp]
 theorem isBot_toDual_iff : IsBot (toDual a) ↔ IsTop a :=
   Iff.rfl
diff --git a/Mathlib/Probability/UniformOn.lean b/Mathlib/Probability/UniformOn.lean
index 524e33e17554c..828768e8f1610 100644
--- a/Mathlib/Probability/UniformOn.lean
+++ b/Mathlib/Probability/UniformOn.lean
@@ -42,7 +42,7 @@ open MeasureTheory MeasurableSpace
 
 namespace ProbabilityTheory
 
-variable {Ω : Type*} [MeasurableSpace Ω]
+variable {Ω : Type*} [MeasurableSpace Ω] {s : Set Ω}
 
 /-- Given a set `s`, `uniformOn s` is the uniform measure on `s`, defined as the counting measure
 conditioned by `s`. One should think of `uniformOn s t` as the proportion of `s` that is contained
@@ -70,6 +70,16 @@ theorem uniformOn_empty {s : Set Ω} : uniformOn s ∅ = 0 := by simp
 @[deprecated (since := "2024-10-09")]
 alias condCount_empty := uniformOn_empty
 
+/-- See `uniformOn_eq_zero` for a version assuming `MeasurableSingletonClass Ω` instead of
+`MeasurableSet s`. -/
+@[simp] lemma uniformOn_eq_zero' (hs : MeasurableSet s) : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by
+  simp [uniformOn, hs]
+
+/-- See `uniformOn_eq_zero'` for a version assuming `MeasurableSet s` instead of
+`MeasurableSingletonClass Ω`. -/
+@[simp] lemma uniformOn_eq_zero [MeasurableSingletonClass Ω] :
+    uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by simp [uniformOn]
+
 theorem finite_of_uniformOn_ne_zero {s t : Set Ω} (h : uniformOn s t ≠ 0) : s.Finite := by
   by_contra hs'
   simp [uniformOn, cond, Measure.count_apply_infinite hs'] at h
@@ -93,7 +103,7 @@ variable [MeasurableSingletonClass Ω]
 theorem uniformOn_isProbabilityMeasure {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
     IsProbabilityMeasure (uniformOn s) := by
   apply cond_isProbabilityMeasure_of_finite
-  · exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
+  · rwa [Measure.count_ne_zero_iff]
   · exact (Measure.count_apply_lt_top.2 hs).ne
 
 @[deprecated (since := "2024-10-09")]
@@ -120,7 +130,7 @@ alias condCount_inter_self := uniformOn_inter_self
 
 theorem uniformOn_self (hs : s.Finite) (hs' : s.Nonempty) : uniformOn s s = 1 := by
   rw [uniformOn, cond_apply hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]
-  · exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
+  · rwa [Measure.count_ne_zero_iff]
   · exact (Measure.count_apply_lt_top.2 hs).ne
 
 @[deprecated (since := "2024-10-09")]
diff --git a/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean b/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
index 669cd38417774..a941b75c4e02a 100644
--- a/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
+++ b/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@@ -3,12 +3,12 @@ Copyright (c) 2024 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Jireh Loreaux
 -/
-
+import Mathlib.Algebra.Group.Subgroup.Map
+import Mathlib.Algebra.Module.Opposite
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.RingTheory.Congruence.Opposite
 import Mathlib.RingTheory.Ideal.Defs
 import Mathlib.RingTheory.TwoSidedIdeal.Lattice
-import Mathlib.Algebra.Module.Opposite
 
 /-!
 # Operations on two-sided ideals
diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean
index 3798b879812e6..0326607cfdb06 100644
--- a/Mathlib/Tactic/Abel.lean
+++ b/Mathlib/Tactic/Abel.lean
@@ -247,11 +247,11 @@ theorem term_atom_pfg {α} [AddCommGroup α] (x x' : α) (h : x = x') : x = term
 /-- Interpret an expression as an atom for `abel`'s normal form. -/
 def evalAtom (e : Expr) : M (NormalExpr × Expr) := do
   let { expr := e', proof?, .. } ← (← readThe AtomM.Context).evalAtom e
-  let i ← AtomM.addAtom e'
+  let (i, a) ← AtomM.addAtom e'
   let p ← match proof? with
   | none => iapp ``term_atom #[e]
-  | some p => iapp ``term_atom_pf #[e, e', p]
-  return (← term' (← intToExpr 1, 1) (i, e') (← zero'), p)
+  | some p => iapp ``term_atom_pf #[e, a, p]
+  return (← term' (← intToExpr 1, 1) (i, a) (← zero'), p)
 
 theorem unfold_sub {α} [SubtractionMonoid α] (a b c : α) (h : a + -b = c) : a - b = c := by
   rw [sub_eq_add_neg, h]
diff --git a/Mathlib/Tactic/FBinop.lean b/Mathlib/Tactic/FBinop.lean
index 96c3a9db63cb6..8e58cb0849763 100644
--- a/Mathlib/Tactic/FBinop.lean
+++ b/Mathlib/Tactic/FBinop.lean
@@ -185,18 +185,14 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
   | .term _ trees e =>
     modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
   | .binop ref f lhs rhs =>
-    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) (do
+    withRef ref <| withTermInfoContext' .anonymous ref do
       let lhs ← toExprCore lhs
       let mut rhs ← toExprCore rhs
-      mkBinOp f lhs rhs)
-      -- FIXME the signature of withInfoContext' has changed, not sure yet what to put here:
-      (do failure)
+      mkBinOp f lhs rhs
   | .macroExpansion macroName stx stx' nested =>
-    withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) (do
+    withRef stx <| withTermInfoContext' macroName stx do
       withMacroExpansion stx stx' do
-        toExprCore nested)
-      -- FIXME the signature of withInfoContext' has changed, not sure yet what to put here:
-      (do failure)
+        toExprCore nested
 
 /-- Try to coerce elements in the tree to `maxS` when needed. -/
 private def applyCoe (t : Tree) (maxS : SRec) : TermElabM Tree := do
diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean
index a47257466df27..90aeed7ba3815 100644
--- a/Mathlib/Tactic/GCongr/Core.lean
+++ b/Mathlib/Tactic/GCongr/Core.lean
@@ -367,7 +367,7 @@ partial def _root_.Lean.MVarId.gcongr
   for lem in (gcongrExt.getState (← getEnv)).getD (relName, lhsHead, varyingArgs) #[] do
     let gs ← try
       -- Try `apply`-ing such a lemma to the goal.
-      Except.ok <$> g.apply (← mkConstWithFreshMVarLevels lem.declName)
+      Except.ok <$> withReducibleAndInstances (g.apply (← mkConstWithFreshMVarLevels lem.declName))
     catch e => pure (Except.error e)
     match gs with
     | .error e =>
diff --git a/Mathlib/Tactic/ITauto.lean b/Mathlib/Tactic/ITauto.lean
index f0449d9828b14..f87cbcddd6ec3 100644
--- a/Mathlib/Tactic/ITauto.lean
+++ b/Mathlib/Tactic/ITauto.lean
@@ -486,7 +486,7 @@ partial def reify (e : Q(Prop)) : AtomM IProp :=
   | ~q(@Ne Prop $a $b) => return .not (.eq (← reify a) (← reify b))
   | e =>
     if e.isArrow then return .imp (← reify e.bindingDomain!) (← reify e.bindingBody!)
-    else return .var (← AtomM.addAtom e)
+    else return .var (← AtomM.addAtom e).1
 
 /-- Once we have a proof object, we have to apply it to the goal. -/
 partial def applyProof (g : MVarId) (Γ : NameMap Expr) (p : Proof) : MetaM Unit :=
diff --git a/Mathlib/Tactic/Linarith/Preprocessing.lean b/Mathlib/Tactic/Linarith/Preprocessing.lean
index 489ff96d9f25c..348309a7774af 100644
--- a/Mathlib/Tactic/Linarith/Preprocessing.lean
+++ b/Mathlib/Tactic/Linarith/Preprocessing.lean
@@ -274,12 +274,12 @@ partial def findSquares (s : RBSet (Nat × Bool) lexOrd.compare) (e : Expr) :
   | (``HPow.hPow, #[_, _, _, _, a, b]) => match b.numeral? with
     | some 2 => do
       let s ← findSquares s a
-      let ai ← AtomM.addAtom a
+      let (ai, _) ← AtomM.addAtom a
       return (s.insert (ai, true))
     | _ => e.foldlM findSquares s
   | (``HMul.hMul, #[_, _, _, _, a, b]) => do
-    let ai ← AtomM.addAtom a
-    let bi ← AtomM.addAtom b
+    let (ai, _) ← AtomM.addAtom a
+    let (bi, _) ← AtomM.addAtom b
     if ai = bi then do
       let s ← findSquares s a
       return (s.insert (ai, false))
diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index 3e2a44a3d836f..9f5be314fe2ff 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -290,7 +290,10 @@ def duplicateImportsCheck (imports : Array Syntax)  : CommandElabM Unit := do
 @[inherit_doc Mathlib.Linter.linter.style.header]
 def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
   let mainModule ← getMainModule
-  unless Linter.getLinterValue linter.style.header (← getOptions) || (← isInMathlib mainModule) do
+  -- The linter skips files not imported in `Mathlib.lean`, to avoid linting "scratch files".
+  -- However, it is active in the test file `MathlibTest.Header` for the linter itself.
+  unless (← isInMathlib mainModule) || mainModule == `MathlibTest.Header do return
+  unless Linter.getLinterValue linter.style.header (← getOptions) do
     return
   if (← get).messages.hasErrors then
     return
diff --git a/Mathlib/Tactic/Linter/PPRoundtrip.lean b/Mathlib/Tactic/Linter/PPRoundtrip.lean
index dced1f5293546..df238e0927ee3 100644
--- a/Mathlib/Tactic/Linter/PPRoundtrip.lean
+++ b/Mathlib/Tactic/Linter/PPRoundtrip.lean
@@ -60,7 +60,7 @@ def polishSource (s : String) : String × Array Nat :=
   let preWS := split.foldl (init := #[]) fun p q =>
     let txt := q.trimLeft.length
     (p.push (q.length - txt)).push txt
-  let preWS := preWS.eraseIdx! 0
+  let preWS := preWS.eraseIdxIfInBounds 0
   let s := (split.map .trimLeft).filter (· != "")
   (" ".intercalate (s.filter (!·.isEmpty)), preWS)
 
diff --git a/Mathlib/Tactic/Module.lean b/Mathlib/Tactic/Module.lean
index 60209e345a89b..14274913e2c77 100644
--- a/Mathlib/Tactic/Module.lean
+++ b/Mathlib/Tactic/Module.lean
@@ -464,9 +464,9 @@ partial def parse (iM : Q(AddCommMonoid $M)) (x : Q($M)) :
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [], q(NF.zero_eq_eval $M)⟩
   /- anything else should be treated as an atom -/
   | _ =>
-    let k : ℕ ← AtomM.addAtom x
-    pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x), k)],
-      q(NF.atom_eq_eval $x)⟩
+    let (k, ⟨x', _⟩) ← AtomM.addAtomQ x
+    pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x'), k)],
+      q(NF.atom_eq_eval $x')⟩
 
 /-- Given expressions `R` and `M` representing types such that `M`'s is a module over `R`'s, and
 given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 3164aab00a49d..91b368722375e 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -133,7 +133,7 @@ partial def parse {u : Level} {α : Q(Type u)} (sα : Q(CommSemiring $α))
     (c : Ring.Cache sα) (e : Q($α)) : AtomM Poly := do
   let els := do
     try pure <| Poly.const (← (← NormNum.derive e).toRat)
-    catch _ => pure <| Poly.var (← addAtom e)
+    catch _ => pure <| Poly.var (← addAtom e).1
   let .const n _ := (← withReducible <| whnf e).getAppFn | els
   match n, c.rα with
   | ``HAdd.hAdd, _ | ``Add.add, _ => match e with
diff --git a/Mathlib/Tactic/Positivity.lean b/Mathlib/Tactic/Positivity.lean
index 8d76b597bcf25..7b2a24e70ec16 100644
--- a/Mathlib/Tactic/Positivity.lean
+++ b/Mathlib/Tactic/Positivity.lean
@@ -1,3 +1,4 @@
 import Mathlib.Tactic.Positivity.Basic
+import Mathlib.Tactic.Positivity.Finset
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Data.Int.Order.Basic
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
index 84faee3f1a0d4..b5dacb13e9ab5 100644
--- a/Mathlib/Tactic/Ring/Basic.lean
+++ b/Mathlib/Tactic/Ring/Basic.lean
@@ -512,9 +512,8 @@ mutual
 partial def ExBase.evalNatCast {a : Q(ℕ)} (va : ExBase sℕ a) : AtomM (Result (ExBase sα) q($a)) :=
   match va with
   | .atom _ => do
-    let a' : Q($α) := q($a)
-    let i ← addAtom a'
-    pure ⟨a', ExBase.atom i, (q(Eq.refl $a') : Expr)⟩
+    let (i, ⟨b', _⟩) ← addAtomQ q($a)
+    pure ⟨b', ExBase.atom i, q(Eq.refl $b')⟩
   | .sum va => do
     let ⟨_, vc, p⟩ ← va.evalNatCast
     pure ⟨_, .sum vc, p⟩
@@ -952,11 +951,11 @@ Evaluates an atom, an expression where `ring` can find no additional structure.
 def evalAtom (e : Q($α)) : AtomM (Result (ExSum sα) e) := do
   let r ← (← read).evalAtom e
   have e' : Q($α) := r.expr
-  let i ← addAtom e'
-  let ve' := (ExBase.atom i (e := e')).toProd (ExProd.mkNat sℕ 1).2 |>.toSum
+  let (i, ⟨a', _⟩) ← addAtomQ e'
+  let ve' := (ExBase.atom i (e := a')).toProd (ExProd.mkNat sℕ 1).2 |>.toSum
   pure ⟨_, ve', match r.proof? with
   | none => (q(atom_pf $e) : Expr)
-  | some (p : Q($e = $e')) => (q(atom_pf' $p) : Expr)⟩
+  | some (p : Q($e = $a')) => (q(atom_pf' $p) : Expr)⟩
 
 theorem inv_mul {R} [DivisionRing R] {a₁ a₂ a₃ b₁ b₃ c}
     (_ : (a₁⁻¹ : R) = b₁) (_ : (a₃⁻¹ : R) = b₃)
@@ -977,9 +976,8 @@ variable (dα : Q(DivisionRing $α))
 
 /-- Applies `⁻¹` to a polynomial to get an atom. -/
 def evalInvAtom (a : Q($α)) : AtomM (Result (ExBase sα) q($a⁻¹)) := do
-  let a' : Q($α) := q($a⁻¹)
-  let i ← addAtom a'
-  pure ⟨a', ExBase.atom i, (q(Eq.refl $a') : Expr)⟩
+  let (i, ⟨b', _⟩) ← addAtomQ q($a⁻¹)
+  pure ⟨b', ExBase.atom i, q(Eq.refl $b')⟩
 
 /-- Inverts a polynomial `va` to get a normalized result polynomial.
 
diff --git a/Mathlib/Tactic/TFAE.lean b/Mathlib/Tactic/TFAE.lean
index 45405bfe5ad58..ac5f1114a8529 100644
--- a/Mathlib/Tactic/TFAE.lean
+++ b/Mathlib/Tactic/TFAE.lean
@@ -298,18 +298,18 @@ elab_rules : tactic
   goal.withContext do
     let (tfaeListQ, tfaeList) ← getTFAEList (← goal.getType)
     closeMainGoal `tfae_finish <|← AtomM.run .reducible do
-      let is ← tfaeList.mapM AtomM.addAtom
+      let is ← tfaeList.mapM (fun e ↦ Prod.fst <$> AtomM.addAtom e)
       let mut hyps := #[]
       for hyp in ← getLocalHyps do
         let ty ← whnfR <|← instantiateMVars <|← inferType hyp
         if let (``Iff, #[p1, p2]) := ty.getAppFnArgs then
-          let q1 ← AtomM.addAtom p1
-          let q2 ← AtomM.addAtom p2
+          let (q1, _) ← AtomM.addAtom p1
+          let (q2, _) ← AtomM.addAtom p2
           hyps := hyps.push (q1, q2, ← mkAppM ``Iff.mp #[hyp])
           hyps := hyps.push (q2, q1, ← mkAppM ``Iff.mpr #[hyp])
         else if ty.isArrow then
-          let q1 ← AtomM.addAtom ty.bindingDomain!
-          let q2 ← AtomM.addAtom ty.bindingBody!
+          let (q1, _) ← AtomM.addAtom ty.bindingDomain!
+          let (q2, _) ← AtomM.addAtom ty.bindingBody!
           hyps := hyps.push (q1, q2, hyp)
       proveTFAE hyps (← get).atoms is tfaeListQ
 
diff --git a/Mathlib/Tactic/WLOG.lean b/Mathlib/Tactic/WLOG.lean
index 461949d04ab7b..cad9a19bf5bfd 100644
--- a/Mathlib/Tactic/WLOG.lean
+++ b/Mathlib/Tactic/WLOG.lean
@@ -77,7 +77,8 @@ def _root_.Lean.MVarId.wlog (goal : MVarId) (h : Option Name) (P : Expr)
   let (revertedFVars, HType) ← liftMkBindingM fun ctx => (do
     let f ← collectForwardDeps lctx fvars
     let revertedFVars := filterOutImplementationDetails lctx (f.map Expr.fvarId!)
-    let HType ← withFreshCache do mkAuxMVarType lctx (revertedFVars.map Expr.fvar) .natural HSuffix
+    let HType ← withFreshCache do
+      mkAuxMVarType lctx (revertedFVars.map Expr.fvar) .natural HSuffix (usedLetOnly := true)
     return (revertedFVars, HType))
       { preserveOrder := false, mainModule := ctx.mainModule }
   /- Set up the goal which will suppose `h`; this begins as a goal with type H (hence HExpr), and h
diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 5a21609d09845..7b7e6e47ae7f0 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -68,8 +68,7 @@ theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSub
         apply_rules [add_le_add_left, le_abs_self]
       _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
         rw [C]
-        apply_rules [add_le_add, mul_le_mul_of_nonneg_left, hn.le, le_refl]
-        norm_num
+        gcongr
       _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
         have : |embeddingOfSubset x b n - embeddingOfSubset x a n| ≤
             dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index 0b829028c0b11..bc85531a753a4 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Init
 import Lean.Meta.Tactic.Simp.Types
+import Qq
 
 /-!
 # A monad for tracking and deduplicating atoms
@@ -44,13 +45,33 @@ def AtomM.run {α : Type} (red : TransparencyMode) (m : AtomM α)
     MetaM α :=
   (m { red, evalAtom }).run' {}
 
-/-- Get the index corresponding to an atomic expression, if it has already been encountered, or
-put it in the list of atoms and return the new index, otherwise. -/
-def AtomM.addAtom (e : Expr) : AtomM Nat := do
+/-- If an atomic expression has already been encountered, get the index and the stored form of the
+atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
+If the atomic expression has *not* already been encountered, store it in the list of atoms, and
+return the new index (and the stored form of the atom, which will be itself).
+
+In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form.
+-/
+def AtomM.addAtom (e : Expr) : AtomM (Nat × Expr) := do
   let c ← get
   for h : i in [:c.atoms.size] do
     if ← withTransparency (← read).red <| isDefEq e c.atoms[i] then
-      return i
-  modifyGet fun c ↦ (c.atoms.size, { c with atoms := c.atoms.push e })
+      return (i, c.atoms[i])
+  modifyGet fun c ↦ ((c.atoms.size, e), { c with atoms := c.atoms.push e })
+
+open Qq in
+/-- If an atomic expression has already been encountered, get the index and the stored form of the
+atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
+If the atomic expression has *not* already been encountered, store it in the list of atoms, and
+return the new index (and the stored form of the atom, which will be itself).
+
+In a normalizing tactic, the expression returned by `addAtomQ` should be considered the normal form.
+
+This is a strongly-typed version of `AtomM.addAtom` for code using `Qq`.
+-/
+def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) :
+    AtomM (Nat × {e' : Q($α) // $e =Q $e'}) := do
+  let (n, e') ← AtomM.addAtom e
+  return (n, ⟨e', ⟨⟩⟩)
 
 end Mathlib.Tactic
diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index d59304f17cbfb..f2235b46071cf 100644
--- a/MathlibTest/abel.lean
+++ b/MathlibTest/abel.lean
@@ -141,3 +141,32 @@ example [AddCommGroup α] (x y z : α) (h : False) (w : x - x = y + z) : False :
   abel_nf at *
   guard_hyp w : 0 = y + z
   assumption
+
+section
+abbrev myId (a : ℤ) : ℤ := a
+
+/-
+Test that when `abel_nf` normalizes multiple expressions which contain a particular atom, it uses a
+form for that atom which is consistent between expressions.
+
+We can't use `guard_hyp h :ₛ` here, as while it does tell apart `x` and `myId x`, it also complains
+about differing instance paths.
+-/
+/--
+info: α : Type _
+a b : α
+x : ℤ
+R : ℤ → ℤ → Prop
+hR : Reflexive R
+h : R (2 • myId x) (2 • myId x)
+⊢ True
+-/
+#guard_msgs (info) in
+set_option pp.mvars false in
+example (x : ℤ) (R : ℤ → ℤ → Prop) (hR : Reflexive R) : True := by
+  have h : R (myId x + x) (x + myId x) := hR ..
+  abel_nf at h
+  trace_state
+  trivial
+
+end
diff --git a/MathlibTest/positivity.lean b/MathlibTest/positivity.lean
index da296d8d2860f..b3f2b9b7af6ba 100644
--- a/MathlibTest/positivity.lean
+++ b/MathlibTest/positivity.lean
@@ -1,10 +1,10 @@
+import Mathlib.Tactic.Positivity
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.MeasureTheory.Integral.Bochner
-import Mathlib.Tactic.Positivity.Finset
 
 /-! # Tests for the `positivity` tactic
 
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index ffdfe755e4dec..8a0a07fea0178 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -178,3 +178,28 @@ example {n : ℝ} (_hn : 0 ≤ n) : (n + 1 / 2) ^ 2 * (n + 1 + 1 / 3) ≤ (n + 1
   ring_nf
   trace_state
   exact test_sorry
+
+section
+abbrev myId (a : ℤ) : ℤ := a
+
+/-
+Test that when `ring_nf` normalizes multiple expressions which contain a particular atom, it uses a
+form for that atom which is consistent between expressions.
+
+We can't use `guard_hyp h :ₛ` here, as while it does tell apart `x` and `myId x`, it also complains
+about differing instance paths.
+-/
+/--
+info: x : ℤ
+R : ℤ → ℤ → Prop
+h : R (myId x * 2) (myId x * 2)
+⊢ True
+-/
+#guard_msgs (info) in
+example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
+  have h : R (myId x + x) (x + myId x) := test_sorry
+  ring_nf at h
+  trace_state
+  trivial
+
+end
diff --git a/lake-manifest.json b/lake-manifest.json
index 510e472529024..4f57aec3e05af 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ff2802eb3612dfd9586f5e080a9559db512c804f",
+   "rev": "f75fd1f8fb9df7c2a8300205df82e27dbfd23125",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "lean-pr-testing-6123",
diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt
index 7a7e8fb75bfe5..e04b49b8dc0f0 100644
--- a/scripts/no_lints_prime_decls.txt
+++ b/scripts/no_lints_prime_decls.txt
@@ -1088,6 +1088,7 @@ div_eq_iff_eq_mul'
 div_eq_of_eq_mul'
 div_eq_of_eq_mul''
 div_le_div''
+div_le_div_iff'
 div_le_div_left'
 div_le_div_right'
 div_left_inj'