Basic.lean

/-
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.Conj
import Mathlib.Algebra.Group.Pi.Lemmas
import Mathlib.Algebra.Group.Subsemigroup.Operations
import Mathlib.Algebra.Group.Submonoid.Operations
import Mathlib.Data.Set.Image
import Mathlib.Tactic.ApplyFun

/-!
# Subgroups

This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
form (unbundled subgroups are in `Deprecated/Subgroups.lean`).

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.

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

## Main definitions

Notation used here:

- `G N` are `Group`s

- `A` is an `AddGroup`

- `H K` are `Subgroup`s of `G` or `AddSubgroup`s of `A`

- `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 G` : the type of subgroups of a group `G`

* `AddSubgroup A` : the type of subgroups of an additive group `A`

* `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.eq_locus 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

open Function
open Int

variable {G G' G'' : Type*} [Group G] [Group G'] [Group G'']
variable {A : Type*} [AddGroup A]

section SubgroupClass

/-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
class InvMemClass (S G : Type*) [Inv G] [SetLike S G] : Prop where
  /-- `s` is closed under inverses -/
  inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s

export InvMemClass (inv_mem)

/-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
class NegMemClass (S G : Type*) [Neg G] [SetLike S G] : Prop where
  /-- `s` is closed under negation -/
  neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s

export NegMemClass (neg_mem)

/-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
class SubgroupClass (S G : Type*) [DivInvMonoid G] [SetLike S G] extends SubmonoidClass S G,
  InvMemClass S G : Prop

/-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
additive subgroups of `G`. -/
class AddSubgroupClass (S G : Type*) [SubNegMonoid G] [SetLike S G] extends AddSubmonoidClass S G,
  NegMemClass S G : Prop

attribute [to_additive] InvMemClass SubgroupClass

attribute [aesop safe apply (rule_sets := [SetLike])] inv_mem neg_mem

@[to_additive (attr := simp)]
theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
    {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩

variable {M S : Type*} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H K : S}

/-- A subgroup is closed under division. -/
@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))
  "An additive subgroup is closed under subtraction."]
theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := by
  rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)

@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))]
theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
  | (n : ℕ) => by
    rw [zpow_natCast]
    exact pow_mem hx n
  | -[n+1] => by
    rw [zpow_negSucc]
    exact inv_mem (pow_mem hx n.succ)

variable [SetLike S G] [SubgroupClass S G]

@[to_additive]
theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
  inv_div b a ▸ inv_mem_iff

@[to_additive /-(attr := simp)-/] -- Porting note: `simp` cannot simplify LHS
theorem exists_inv_mem_iff_exists_mem {P : G → Prop} :
    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := by
  constructor <;>
    · rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

@[to_additive]
theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
  ⟨fun hba => by simpa using mul_mem hba (inv_mem h), fun hb => mul_mem hb h⟩

@[to_additive]
theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
  ⟨fun hab => by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩

namespace InvMemClass

/-- A subgroup of a group inherits an inverse. -/
@[to_additive "An additive subgroup of an `AddGroup` inherits an inverse."]
instance inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G]
  [InvMemClass S G] {H : S} : Inv H :=
  ⟨fun a => ⟨a⁻¹, inv_mem a.2⟩⟩

@[to_additive (attr := simp, norm_cast)]
theorem coe_inv (x : H) : (x⁻¹).1 = x.1⁻¹ :=
  rfl

end InvMemClass

namespace SubgroupClass

@[to_additive (attr := deprecated (since := "2024-01-15"))] alias coe_inv := InvMemClass.coe_inv

-- Here we assume H, K, and L are subgroups, but in fact any one of them
-- could be allowed to be a subsemigroup.
-- Counterexample where K and L are submonoids: H = ℤ, K = ℕ, L = -ℕ
-- Counterexample where H and K are submonoids: H = {n | n = 0 ∨ 3 ≤ n}, K = 3ℕ + 4ℕ, L = 5ℤ
@[to_additive]
theorem subset_union {H K L : S} : (H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L := by
  refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (· xH) (· xH)⟩
  rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
  exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp

/-- A subgroup of a group inherits a division -/
@[to_additive "An additive subgroup of an `AddGroup` inherits a subtraction."]
instance div {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G]
  [SubgroupClass S G] {H : S} : Div H :=
  ⟨fun a b => ⟨a / b, div_mem a.2 b.2⟩⟩

/-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/
instance _root_.AddSubgroupClass.zsmul {M S} [SubNegMonoid M] [SetLike S M]
    [AddSubgroupClass S M] {H : S} : SMul ℤ H :=
  ⟨fun n a => ⟨n • a.1, zsmul_mem a.2 n⟩⟩

/-- A subgroup of a group inherits an integer power. -/
@[to_additive existing]
instance zpow {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
  ⟨fun a n => ⟨a.1 ^ n, zpow_mem a.2 n⟩⟩

@[to_additive (attr := simp, norm_cast)]
theorem coe_div (x y : H) : (x / y).1 = x.1 / y.1 :=
  rfl

variable (H)

-- Prefer subclasses of `Group` over subclasses of `SubgroupClass`.
/-- A subgroup of a group inherits a group structure. -/
@[to_additive "An additive subgroup of an `AddGroup` inherits an `AddGroup` structure."]
instance (priority := 75) toGroup : Group H :=
  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

-- Prefer subclasses of `CommGroup` over subclasses of `SubgroupClass`.
/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
@[to_additive "An additive subgroup of an `AddCommGroup` is an `AddCommGroup`."]
instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [SubgroupClass S G] :
    CommGroup H :=
  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

/-- The natural group hom from a subgroup of group `G` to `G`. -/
@[to_additive (attr := coe)
  "The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
protected def subtype : H →* G where
  toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl

@[to_additive (attr := simp)]
theorem coeSubtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G) := by
  rfl

variable {H}

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl

@[to_additive (attr := simp, norm_cast)]
theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl

/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
def inclusion {H K : S} (h : H ≤ K) : H →* K :=
  MonoidHom.mk' (fun x => ⟨x, h x.prop⟩) fun _ _=> rfl

@[to_additive (attr := simp)]
theorem inclusion_self (x : H) : inclusion le_rfl x = x := by
  cases x
  rfl

@[to_additive (attr := simp)]
theorem inclusion_mk {h : H ≤ K} (x : G) (hx : x ∈ H) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
  rfl

@[to_additive]
theorem inclusion_right (h : H ≤ K) (x : K) (hx : (x : G) ∈ H) : inclusion h ⟨x, hx⟩ = x := by
  cases x
  rfl

@[simp]
theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
    inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x := by
  cases x
  rfl

@[to_additive (attr := simp)]
theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
  cases a
  simp only [inclusion, MonoidHom.mk'_apply]

@[to_additive (attr := simp)]
theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
    (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H := by
  ext
  simp only [MonoidHom.comp_apply, coeSubtype, coe_inclusion]

end SubgroupClass

end SubgroupClass

/-- A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse. -/
structure Subgroup (G : Type*) [Group G] extends Submonoid G where
  /-- `G` is closed under inverses -/
  inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier

/-- An additive subgroup of an additive group `G` is a subset containing 0, closed
under addition and additive inverse. -/
structure AddSubgroup (G : Type*) [AddGroup G] extends AddSubmonoid G where
  /-- `G` is closed under negation -/
  neg_mem' {x} : x ∈ carrier → -x ∈ carrier

attribute [to_additive] Subgroup

-- Porting note: Removed, translation already exists
-- attribute [to_additive AddSubgroup.toAddSubmonoid] Subgroup.toSubmonoid

/-- Reinterpret a `Subgroup` as a `Submonoid`. -/
add_decl_doc Subgroup.toSubmonoid

/-- Reinterpret an `AddSubgroup` as an `AddSubmonoid`. -/
add_decl_doc AddSubgroup.toAddSubmonoid

namespace Subgroup

@[to_additive]
instance : SetLike (Subgroup G) G where
  coe s := s.carrier
  coe_injective' p q h := by
    obtain ⟨⟨⟨hp,_⟩,_⟩,_⟩ := p
    obtain ⟨⟨⟨hq,_⟩,_⟩,_⟩ := q
    congr

-- Porting note: Below can probably be written more uniformly
@[to_additive]
instance : SubgroupClass (Subgroup G) G where
  inv_mem := Subgroup.inv_mem' _
  one_mem _ := (Subgroup.toSubmonoid _).one_mem'
  mul_mem := (Subgroup.toSubmonoid _).mul_mem'

@[to_additive (attr := simp, nolint simpNF)] -- Porting note (#10675): dsimp can not prove this
theorem mem_carrier {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

@[to_additive (attr := simp)]
theorem mem_mk {s : Set G} {x : G} (h_one) (h_mul) (h_inv) :
    x ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ↔ x ∈ s :=
  Iff.rfl

@[to_additive (attr := simp, norm_cast)]
theorem coe_set_mk {s : Set G} (h_one) (h_mul) (h_inv) :
    (mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv : Set G) = s :=
  rfl

@[to_additive (attr := simp)]
theorem mk_le_mk {s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv') :
    mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t :=
  Iff.rfl

initialize_simps_projections Subgroup (carrier → coe)
initialize_simps_projections AddSubgroup (carrier → coe)

@[to_additive (attr := simp)]
theorem coe_toSubmonoid (K : Subgroup G) : (K.toSubmonoid : Set G) = K :=
  rfl

@[to_additive (attr := simp)]
theorem mem_toSubmonoid (K : Subgroup G) (x : G) : x ∈ K.toSubmonoid ↔ x ∈ K :=
  Iff.rfl

@[to_additive]
theorem toSubmonoid_injective : Function.Injective (toSubmonoid : Subgroup G → Submonoid G) :=
  -- fun p q h => SetLike.ext'_iff.2 (show _ from SetLike.ext'_iff.1 h)
  fun p q h => by
    have := SetLike.ext'_iff.1 h
    rw [coe_toSubmonoid, coe_toSubmonoid] at this
    exact SetLike.ext'_iff.2 this

@[to_additive (attr := simp)]
theorem toSubmonoid_eq {p q : Subgroup G} : p.toSubmonoid = q.toSubmonoid ↔ p = q :=
  toSubmonoid_injective.eq_iff

@[to_additive (attr := mono)]
theorem toSubmonoid_strictMono : StrictMono (toSubmonoid : Subgroup G → Submonoid G) := fun _ _ =>
  id

@[to_additive (attr := mono)]
theorem toSubmonoid_mono : Monotone (toSubmonoid : Subgroup G → Submonoid G) :=
  toSubmonoid_strictMono.monotone

@[to_additive (attr := simp)]
theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q :=
  Iff.rfl

@[to_additive (attr := simp)]
lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩

end Subgroup

/-!
### 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)

/-- Copy of a subgroup with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive
      "Copy of an additive subgroup with a new `carrier` equal to the old one.
      Useful to fix definitional equalities"]
protected def copy (K : Subgroup G) (s : Set G) (hs : s = K) : Subgroup G where
  carrier := s
  one_mem' := hs.symm ▸ K.one_mem'
  mul_mem' := hs.symm ▸ K.mul_mem'
  inv_mem' hx := by simpa [hs] using hx -- Porting note: `▸` didn't work here

@[to_additive (attr := simp)]
theorem coe_copy (K : Subgroup G) (s : Set G) (hs : s = ↑K) : (K.copy s hs : Set G) = s :=
  rfl

@[to_additive]
theorem copy_eq (K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K :=
  SetLike.coe_injective hs

/-- Two subgroups are equal if they have the same elements. -/
@[to_additive (attr := ext) "Two `AddSubgroup`s are equal if they have the same elements."]
theorem ext {H K : Subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K :=
  SetLike.ext h

/-- A subgroup contains the group's 1. -/
@[to_additive "An `AddSubgroup` contains the group's 0."]
protected theorem one_mem : (1 : G) ∈ H :=
  one_mem _

/-- A subgroup is closed under multiplication. -/
@[to_additive "An `AddSubgroup` is closed under addition."]
protected theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H :=
  mul_mem

/-- A subgroup is closed under inverse. -/
@[to_additive "An `AddSubgroup` is closed under inverse."]
protected theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H :=
  inv_mem

/-- A subgroup is closed under division. -/
@[to_additive "An `AddSubgroup` is closed under subtraction."]
protected theorem div_mem {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
  div_mem hx hy

@[to_additive]
protected theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
  inv_mem_iff

@[to_additive]
protected theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
  div_mem_comm_iff

@[to_additive]
protected theorem exists_inv_mem_iff_exists_mem (K : Subgroup G) {P : G → Prop} :
    (∃ x : G, x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x :=
  exists_inv_mem_iff_exists_mem

@[to_additive]
protected theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
  mul_mem_cancel_right h

@[to_additive]
protected theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
  mul_mem_cancel_left h

@[to_additive]
protected theorem pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K :=
  pow_mem hx

@[to_additive]
protected theorem zpow_mem {x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K :=
  zpow_mem hx

/-- Construct a subgroup from a nonempty set that is closed under division. -/
@[to_additive "Construct a subgroup from a nonempty set that is closed under subtraction"]
def ofDiv (s : Set G) (hsn : s.Nonempty) (hs : ∀ᵉ (x ∈ s) (y ∈ s), x * y⁻¹ ∈ s) :
    Subgroup G :=
  have one_mem : (1 : G) ∈ s := by
    let ⟨x, hx⟩ := hsn
    simpa using hs x hx x hx
  have inv_mem : ∀ x, x ∈ s → x⁻¹ ∈ s := fun x hx => by simpa using hs 1 one_mem x hx
  { carrier := s
    one_mem' := one_mem
    inv_mem' := inv_mem _
    mul_mem' := fun hx hy => by simpa using hs _ hx _ (inv_mem _ hy) }

/-- A subgroup of a group inherits a multiplication. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an addition."]
instance mul : Mul H :=
  H.toSubmonoid.mul

/-- A subgroup of a group inherits a 1. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a zero."]
instance one : One H :=
  H.toSubmonoid.one

/-- A subgroup of a group inherits an inverse. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an inverse."]
instance inv : Inv H :=
  ⟨fun a => ⟨a⁻¹, H.inv_mem a.2⟩⟩

/-- A subgroup of a group inherits a division -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a subtraction."]
instance div : Div H :=
  ⟨fun a b => ⟨a / b, H.div_mem a.2 b.2⟩⟩

/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/
instance _root_.AddSubgroup.nsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H :=
  ⟨fun n a => ⟨n • a, H.nsmul_mem a.2 n⟩⟩

/-- A subgroup of a group inherits a natural power -/
@[to_additive existing]
protected instance npow : Pow H ℕ :=
  ⟨fun a n => ⟨a ^ n, H.pow_mem a.2 n⟩⟩

/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/
instance _root_.AddSubgroup.zsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H :=
  ⟨fun n a => ⟨n • a, H.zsmul_mem a.2 n⟩⟩

/-- A subgroup of a group inherits an integer power -/
@[to_additive existing]
instance zpow : Pow H ℤ :=
  ⟨fun a n => ⟨a ^ n, H.zpow_mem a.2 n⟩⟩

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y :=
  rfl

@[to_additive (attr := simp, norm_cast)]
theorem coe_one : ((1 : H) : G) = 1 :=
  rfl

@[to_additive (attr := simp, norm_cast)]
theorem coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) :=
  rfl

@[to_additive (attr := simp, norm_cast)]
theorem coe_div (x y : H) : (↑(x / y) : G) = ↑x / ↑y :=
  rfl

-- Porting note: removed simp, theorem has variable as head symbol
@[to_additive (attr := norm_cast)]
theorem coe_mk (x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x :=
  rfl

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl

@[to_additive (attr := norm_cast)] -- Porting note (#10685): dsimp can prove this
theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl

@[to_additive] -- This can be proved by `Submonoid.mk_eq_one`
theorem mk_eq_one {g : G} {h} : (⟨g, h⟩ : H) = 1 ↔ g = 1 := by simp

/-- A subgroup of a group inherits a group structure. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an `AddGroup` structure."]
instance toGroup {G : Type*} [Group G] (H : Subgroup G) : Group H :=
  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
@[to_additive "An `AddSubgroup` of an `AddCommGroup` is an `AddCommGroup`."]
instance toCommGroup {G : Type*} [CommGroup G] (H : Subgroup G) : CommGroup H :=
  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

/-- The natural group hom from a subgroup of group `G` to `G`. -/
@[to_additive "The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`."]
protected def subtype : H →* G where
  toFun := ((↑) : H → G); map_one' := rfl; map_mul' _ _ := rfl

@[to_additive (attr := simp)]
theorem coeSubtype : ⇑ H.subtype = ((↑) : H → G) :=
  rfl

@[to_additive]
theorem subtype_injective : Function.Injective (Subgroup.subtype H) :=
  Subtype.coe_injective

/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
  MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl

@[to_additive (attr := simp)]
theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
  cases a
  simp only [inclusion, coe_mk, MonoidHom.mk'_apply]

@[to_additive]
theorem inclusion_injective {H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h :=
  Set.inclusion_injective h

@[to_additive (attr := simp)]
theorem subtype_comp_inclusion {H K : Subgroup G} (hH : H ≤ K) :
    K.subtype.comp (inclusion hH) = H.subtype :=
  rfl

/-- 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 : Inf (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 h =>
    ⟨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 h => ⟨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`. -/
@[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`."]
theorem closure_induction {p : G → Prop} {x} (h : x ∈ closure k) (mem : ∀ x ∈ k, p x) (one : p 1)
    (mul : ∀ x y, p x → p y → p (x * y)) (inv : ∀ x, p x → p x⁻¹) : p x :=
  (@closure_le _ _ ⟨⟨⟨setOf p, fun {x y} ↦ mul x y⟩, one⟩, fun {x} ↦ inv x⟩ k).2 mem h

/-- A dependent version of `Subgroup.closure_induction`.  -/
@[to_additive (attr := elab_as_elim) "A dependent version of `AddSubgroup.closure_induction`. "]
theorem closure_induction' {p : ∀ x, x ∈ closure k → Prop}
    (mem : ∀ (x) (h : x ∈ k), p x (subset_closure h)) (one : p 1 (one_mem _))
    (mul : ∀ x hx y 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 := by
  refine Exists.elim ?_ fun (hx : x ∈ closure k) (hc : p x hx) => hc
  exact
    closure_induction hx (fun x hx => ⟨_, mem x hx⟩) ⟨_, one⟩
      (fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, mul _ _ _ _ hx hy⟩) fun x ⟨hx', hx⟩ => ⟨_, inv _ _ hx⟩

/-- 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 : G → G → Prop} {x} {y : G} (hx : x ∈ closure k) (hy : y ∈ closure k)
    (Hk : ∀ x ∈ k, ∀ y ∈ k, p x y) (H1_left : ∀ x, p 1 x) (H1_right : ∀ x, p x 1)
    (Hmul_left : ∀ x₁ x₂ y, p x₁ y → p x₂ y → p (x₁ * x₂) y)
    (Hmul_right : ∀ x y₁ y₂, p x y₁ → p x y₂ → p x (y₁ * y₂)) (Hinv_left : ∀ x y, p x y → p x⁻¹ y)
    (Hinv_right : ∀ x y, p x y → p x y⁻¹) : p x y :=
  closure_induction hx
    (fun x xk => closure_induction hy (Hk x xk) (H1_right x) (Hmul_right x) (Hinv_right x))
    (H1_left y) (fun z z' => Hmul_left z z' y) fun z => Hinv_left z y

@[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 x hx _ => by
      refine closure_induction' (fun g hg => ?_) ?_ (fun g₁ g₂ hg₁ hg₂ => ?_) (fun g hg => ?_) hx
      · exact subset_closure hg
      · exact one_mem _
      · exact mul_mem
      · exact inv_mem

/-- If all the elements of a set `s` commute, then `closure s` is a commutative group. -/
@[to_additive
      "If all the elements of a set `s` commute, then `closure s` is an additive
      commutative group."]
def closureCommGroupOfComm {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
    CommGroup (closure k) :=
  { (closure k).toGroup with
    mul_comm := fun x y => by
      ext
      simp only [Subgroup.coe_mul]
      refine
        closure_induction₂ x.prop y.prop hcomm (fun x => by simp only [mul_one, one_mul])
          (fun x => by simp only [mul_one, one_mul])
          (fun x y z h₁ h₂ => by rw [mul_assoc, h₂, ← mul_assoc, h₁, mul_assoc])
          (fun x y z h₁ h₂ => by rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc])
          (fun x y h => by
            rw [inv_mul_eq_iff_eq_mul, ← mul_assoc, h, mul_assoc, mul_inv_self, mul_one])
          fun x y h => by
          rw [mul_inv_eq_iff_eq_mul, mul_assoc, h, ← mul_assoc, inv_mul_self, one_mul] }

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]
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 hx (fun _ ↦ mem_iUnion.1) ?_ ?_ ?_
  · 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 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]

/-- Given `Subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`. -/
@[to_additive prod
      "Given `AddSubgroup`s `H`, `K` of `AddGroup`s `A`, `B` respectively, `H × K`
      as an `AddSubgroup` of `A × B`."]
def prod (H : Subgroup G) (K : Subgroup N) : Subgroup (G × N) :=
  { Submonoid.prod H.toSubmonoid K.toSubmonoid with
    inv_mem' := fun hx => ⟨H.inv_mem' hx.1, K.inv_mem' hx.2⟩ }

@[to_additive coe_prod]
theorem coe_prod (H : Subgroup G) (K : Subgroup N) :
    (H.prod K : Set (G × N)) = (H : Set G) ×ˢ (K : Set N) :=
  rfl

@[to_additive mem_prod]
theorem mem_prod {H : Subgroup G} {K : Subgroup N} {p : G × N} : p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K :=
  Iff.rfl

@[to_additive prod_mono]
theorem prod_mono : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) (@prod G _ N _) (@prod G _ N _) :=
  fun _s _s' hs _t _t' ht => Set.prod_mono hs ht

@[to_additive prod_mono_right]
theorem prod_mono_right (K : Subgroup G) : Monotone fun t : Subgroup N => K.prod t :=
  prod_mono (le_refl K)

@[to_additive prod_mono_left]
theorem prod_mono_left (H : Subgroup N) : Monotone fun K : Subgroup G => K.prod H := fun _ _ hs =>
  prod_mono hs (le_refl H)

@[to_additive prod_top]
theorem prod_top (K : Subgroup G) : K.prod (⊤ : Subgroup N) = K.comap (MonoidHom.fst G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

@[to_additive top_prod]
theorem top_prod (H : Subgroup N) : (⊤ : Subgroup G).prod H = H.comap (MonoidHom.snd G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

@[to_additive (attr := simp) top_prod_top]
theorem top_prod_top : (⊤ : Subgroup G).prod (⊤ : Subgroup N) = ⊤ :=
  (top_prod _).trans <| comap_top _

@[to_additive]
theorem bot_prod_bot : (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod, Prod.one_eq_mk]

@[to_additive le_prod_iff]
theorem le_prod_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K := by
  simpa only [← Subgroup.toSubmonoid_le] using Submonoid.le_prod_iff

@[to_additive prod_le_iff]
theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J := by
  simpa only [← Subgroup.toSubmonoid_le] using Submonoid.prod_le_iff

@[to_additive (attr := simp) prod_eq_bot_iff]
theorem prod_eq_bot_iff {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥ := by
  simpa only [← Subgroup.toSubmonoid_eq] using Submonoid.prod_eq_bot_iff

/-- Product of subgroups is isomorphic to their product as groups. -/
@[to_additive prodEquiv
      "Product of additive subgroups is isomorphic to their product
      as additive groups"]
def prodEquiv (H : Subgroup G) (K : Subgroup N) : H.prod K ≃* H × K :=
  { Equiv.Set.prod (H : Set G) (K : Set N) with map_mul' := fun _ _ => rfl }

section Pi

variable {η : Type*} {f : η → Type*}

-- defined here and not in Algebra.Group.Submonoid.Operations to have access to Algebra.Group.Pi
/-- A version of `Set.pi` for submonoids. Given an index set `I` and a family of submodules
`s : Π i, Submonoid f i`, `pi I s` is the submonoid of dependent functions `f : Π i, f i` such that
`f i` belongs to `Pi I s` whenever `i ∈ I`. -/
@[to_additive "A version of `Set.pi` for `AddSubmonoid`s. Given an index set `I` and a family
  of submodules `s : Π i, AddSubmonoid f i`, `pi I s` is the `AddSubmonoid` of dependent functions
  `f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`."]
def _root_.Submonoid.pi [∀ i, MulOneClass (f i)] (I : Set η) (s : ∀ i, Submonoid (f i)) :
    Submonoid (∀ i, f i) where
  carrier := I.pi fun i => (s i).carrier
  one_mem' i _ := (s i).one_mem
  mul_mem' hp hq i hI := (s i).mul_mem (hp i hI) (hq i hI)

variable [∀ i, Group (f i)]

/-- A version of `Set.pi` for subgroups. Given an index set `I` and a family of submodules
`s : Π i, Subgroup f i`, `pi I s` is the subgroup of dependent functions `f : Π i, f i` such that
`f i` belongs to `pi I s` whenever `i ∈ I`. -/
@[to_additive
      "A version of `Set.pi` for `AddSubgroup`s. Given an index set `I` and a family
      of submodules `s : Π i, AddSubgroup f i`, `pi I s` is the `AddSubgroup` of dependent functions
      `f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`."]
def pi (I : Set η) (H : ∀ i, Subgroup (f i)) : Subgroup (∀ i, f i) :=
  { Submonoid.pi I fun i => (H i).toSubmonoid with
    inv_mem' := fun hp i hI => (H i).inv_mem (hp i hI) }

@[to_additive]
theorem coe_pi (I : Set η) (H : ∀ i, Subgroup (f i)) :
    (pi I H : Set (∀ i, f i)) = Set.pi I fun i => (H i : Set (f i)) :=
  rfl

@[to_additive]
theorem mem_pi (I : Set η) {H : ∀ i, Subgroup (f i)} {p : ∀ i, f i} :
    p ∈ pi I H ↔ ∀ i : η, i ∈ I → p i ∈ H i :=
  Iff.rfl

@[to_additive]
theorem pi_top (I : Set η) : (pi I fun i => (⊤ : Subgroup (f i))) = ⊤ :=
  ext fun x => by simp [mem_pi]

@[to_additive]
theorem pi_empty (H : ∀ i, Subgroup (f i)) : pi ∅ H = ⊤ :=
  ext fun x => by simp [mem_pi]

@[to_additive]
theorem pi_bot : (pi Set.univ fun i => (⊥ : Subgroup (f i))) = ⊥ :=
  (eq_bot_iff_forall _).mpr fun p hp => by
    simp only [mem_pi, mem_bot] at *
    ext j
    exact hp j trivial

@[to_additive]
theorem le_pi_iff {I : Set η} {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
    J ≤ pi I H ↔ ∀ i : η, i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i := by
  constructor
  · intro h i hi
    rintro _ ⟨x, hx, rfl⟩
    exact (h hx) _ hi
  · intro h x hx i hi
    exact h i hi ⟨_, hx, rfl⟩

@[to_additive (attr := simp)]
theorem mulSingle_mem_pi [DecidableEq η] {I : Set η} {H : ∀ i, Subgroup (f i)} (i : η) (x : f i) :
    Pi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i := by
  constructor
  · intro h hi
    simpa using h i hi
  · intro h j hj
    by_cases heq : j = i
    · subst heq
      simpa using h hj
    · simp [heq, one_mem]

@[to_additive]
theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀ i, H i = ⊥ := by
  classical
    simp only [eq_bot_iff_forall]
    constructor
    · intro h i x hx
      have : MonoidHom.mulSingle f i x = 1 :=
        h (MonoidHom.mulSingle f i x) ((mulSingle_mem_pi i x).mpr fun _ => hx)
      simpa using congr_fun this i
    · exact fun h x hx => funext fun i => h _ _ (hx i trivial)

end Pi

/-- A subgroup is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` -/
structure Normal : Prop where
  /-- `N` is closed under conjugation -/
  conj_mem : ∀ n, n ∈ H → ∀ g : G, g * n * g⁻¹ ∈ H

attribute [class] Normal

end Subgroup

namespace AddSubgroup

/-- An AddSubgroup is normal if whenever `n ∈ H`, then `g + n - g ∈ H` for every `g : G` -/
structure Normal (H : AddSubgroup A) : Prop where
  /-- `N` is closed under additive conjugation -/
  conj_mem : ∀ n, n ∈ H → ∀ g : A, g + n + -g ∈ H

attribute [to_additive] Subgroup.Normal

attribute [class] Normal

end AddSubgroup

namespace Subgroup

variable {H K : Subgroup G}

@[to_additive]
instance (priority := 100) normal_of_comm {G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal :=
  ⟨by simp [mul_comm, mul_left_comm]⟩

namespace Normal

@[to_additive]
theorem conj_mem' (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) :
    g⁻¹ * n * g ∈ H := by
  convert nH.conj_mem n hn g⁻¹
  rw [inv_inv]

@[to_additive]
theorem mem_comm (nH : H.Normal) {a b : G} (h : a * b ∈ H) : b * a ∈ H := by
  have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
  -- Porting note: Previous code was:
  -- simpa
  simp_all only [inv_mul_cancel_left, inv_inv]

@[to_additive]
theorem mem_comm_iff (nH : H.Normal) {a b : G} : a * b ∈ H ↔ b * a ∈ H :=
  ⟨nH.mem_comm, nH.mem_comm⟩

end Normal

variable (H)

/-- A subgroup is characteristic if it is fixed by all automorphisms.
  Several equivalent conditions are provided by lemmas of the form `Characteristic.iff...` -/
structure Characteristic : Prop where
  /-- `H` is fixed by all automorphisms -/
  fixed : ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom = H

attribute [class] Characteristic

instance (priority := 100) normal_of_characteristic [h : H.Characteristic] : H.Normal :=
  ⟨fun a ha b => (SetLike.ext_iff.mp (h.fixed (MulAut.conj b)) a).mpr ha⟩

end Subgroup

namespace AddSubgroup

variable (H : AddSubgroup A)

/-- An `AddSubgroup` is characteristic if it is fixed by all automorphisms.
  Several equivalent conditions are provided by lemmas of the form `Characteristic.iff...` -/
structure Characteristic : Prop where
  /-- `H` is fixed by all automorphisms -/
  fixed : ∀ ϕ : A ≃+ A, H.comap ϕ.toAddMonoidHom = H

attribute [to_additive] Subgroup.Characteristic

attribute [class] Characteristic

instance (priority := 100) normal_of_characteristic [h : H.Characteristic] : H.Normal :=
  ⟨fun a ha b => (SetLike.ext_iff.mp (h.fixed (AddAut.conj b)) a).mpr ha⟩

end AddSubgroup

namespace Subgroup

variable {H K : Subgroup G}

@[to_additive]
theorem characteristic_iff_comap_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom = H :=
  ⟨Characteristic.fixed, Characteristic.mk⟩

@[to_additive]
theorem characteristic_iff_comap_le : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom ≤ H :=
  characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => le_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (h ϕ) fun g hg => h ϕ.symm ((congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mpr hg)⟩

@[to_additive]
theorem characteristic_iff_le_comap : H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.comap ϕ.toMonoidHom :=
  characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => ge_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (fun g hg => (congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mp (h ϕ.symm hg)) (h ϕ)⟩

@[to_additive]
theorem characteristic_iff_map_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom = H := by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

@[to_additive]
theorem characteristic_iff_map_le : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom ≤ H := by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

@[to_additive]
theorem characteristic_iff_le_map : H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.map ϕ.toMonoidHom := by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

@[to_additive]
instance botCharacteristic : Characteristic (⊥ : Subgroup G) :=
  characteristic_iff_le_map.mpr fun _ϕ => bot_le

@[to_additive]
instance topCharacteristic : Characteristic (⊤ : Subgroup G) :=
  characteristic_iff_map_le.mpr fun _ϕ => le_top


variable (H)

section Normalizer

/-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
@[to_additive "The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal."]
def normalizer : Subgroup G where
  carrier := { g : G | ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H }
  one_mem' := by simp
  mul_mem' {a b} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) (hb : ∀ n, n ∈ H ↔ b * n * b⁻¹ ∈ H) n := by
    rw [hb, ha]
    simp only [mul_assoc, mul_inv_rev]
  inv_mem' {a} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) n := by
    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_right_inv, mul_one]

-- variant for sets.
-- TODO should this replace `normalizer`?
/-- The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S` -/
@[to_additive
      "The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy
      `g+S-g=S`."]
def setNormalizer (S : Set G) : Subgroup G where
  carrier := { g : G | ∀ n, n ∈ S ↔ g * n * g⁻¹ ∈ S }
  one_mem' := by simp
  mul_mem' {a b} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) (hb : ∀ n, n ∈ S ↔ b * n * b⁻¹ ∈ S) n := by
    rw [hb, ha]
    simp only [mul_assoc, mul_inv_rev]
  inv_mem' {a} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) n := by
    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_right_inv, mul_one]

variable {H}

@[to_additive]
theorem mem_normalizer_iff {g : G} : g ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
  Iff.rfl

@[to_additive]
theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
  rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]

@[to_additive]
theorem mem_normalizer_iff' {g : G} : g ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
  ⟨fun h n => by rw [h, mul_assoc, mul_inv_cancel_right], fun h n => by
    rw [mul_assoc, ← h, inv_mul_cancel_right]⟩

@[to_additive]
theorem le_normalizer : H ≤ normalizer H := fun x xH n => by
  rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]

@[to_additive]
instance (priority := 100) normal_in_normalizer : (H.subgroupOf H.normalizer).Normal :=
  ⟨fun x xH g => by simpa only [mem_subgroupOf] using (g.2 x.1).1 xH⟩

@[to_additive]
theorem normalizer_eq_top : H.normalizer = ⊤ ↔ H.Normal :=
  eq_top_iff.trans
    ⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
      ⟨fun hb => h.conj_mem b hb a, fun hb => by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩

@[to_additive]
theorem le_normalizer_of_normal [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer :=
  fun x hx y =>
  ⟨fun yH => hK.conj_mem ⟨y, HK yH⟩ yH ⟨x, hx⟩, fun yH => by
    simpa [mem_subgroupOf, mul_assoc] using
      hK.conj_mem ⟨x * y * x⁻¹, HK yH⟩ yH ⟨x⁻¹, K.inv_mem hx⟩⟩

variable {N : Type*} [Group N]

/-- The preimage of the normalizer is contained in the normalizer of the preimage. -/
@[to_additive "The preimage of the normalizer is contained in the normalizer of the preimage."]
theorem le_normalizer_comap (f : N →* G) :
    H.normalizer.comap f ≤ (H.comap f).normalizer := fun x => by
  simp only [mem_normalizer_iff, mem_comap]
  intro h n
  simp [h (f n)]

/-- The image of the normalizer is contained in the normalizer of the image. -/
@[to_additive "The image of the normalizer is contained in the normalizer of the image."]
theorem le_normalizer_map (f : G →* N) : H.normalizer.map f ≤ (H.map f).normalizer := fun _ => by
  simp only [and_imp, exists_prop, mem_map, exists_imp, mem_normalizer_iff]
  rintro x hx rfl n
  constructor
  · rintro ⟨y, hy, rfl⟩
    use x * y * x⁻¹, (hx y).1 hy
    simp
  · rintro ⟨y, hyH, hy⟩
    use x⁻¹ * y * x
    rw [hx]
    simp [hy, hyH, mul_assoc]

variable (G)

/-- Every proper subgroup `H` of `G` is a proper normal subgroup of the normalizer of `H` in `G`. -/
def _root_.NormalizerCondition :=
  ∀ H : Subgroup G, H < ⊤ → H < normalizer H

variable {G}

/-- Alternative phrasing of the normalizer condition: Only the full group is self-normalizing.
This may be easier to work with, as it avoids inequalities and negations.  -/
theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
    NormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤ := by
  apply forall_congr'; intro H
  simp only [lt_iff_le_and_ne, le_normalizer, true_and_iff, le_top, Ne]
  tauto

variable (H)

end Normalizer

/-- Commutativity of a subgroup -/
structure IsCommutative : Prop where
  /-- `*` is commutative on `H` -/
  is_comm : Std.Commutative (α := H) (· * ·)

attribute [class] IsCommutative

/-- Commutativity of an additive subgroup -/
structure _root_.AddSubgroup.IsCommutative (H : AddSubgroup A) : Prop where
  /-- `+` is commutative on `H` -/
  is_comm : Std.Commutative (α := H) (· + ·)

attribute [to_additive] Subgroup.IsCommutative

attribute [class] AddSubgroup.IsCommutative

/-- A commutative subgroup is commutative. -/
@[to_additive "A commutative subgroup is commutative."]
instance IsCommutative.commGroup [h : H.IsCommutative] : CommGroup H :=
  { H.toGroup with mul_comm := h.is_comm.comm }

@[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}

/-- Given a set `s`, `conjugatesOfSet s` is the set of all conjugates of
the elements of `s`. -/
def conjugatesOfSet (s : Set G) : Set G :=
  ⋃ a ∈ s, conjugatesOf a

theorem mem_conjugatesOfSet_iff {x : G} : x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x := by
  erw [Set.mem_iUnion₂]; simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]

theorem subset_conjugatesOfSet : s ⊆ conjugatesOfSet s := fun (x : G) (h : x ∈ s) =>
  mem_conjugatesOfSet_iff.2 ⟨x, h, IsConj.refl _⟩

theorem conjugatesOfSet_mono {s t : Set G} (h : s ⊆ t) : conjugatesOfSet s ⊆ conjugatesOfSet t :=
  Set.biUnion_subset_biUnion_left h

theorem conjugates_subset_normal {N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) :
    conjugatesOf a ⊆ N := by
  rintro a hc
  obtain ⟨c, rfl⟩ := isConj_iff.1 hc
  exact tn.conj_mem a h c

theorem conjugatesOfSet_subset {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ N) :
    conjugatesOfSet s ⊆ N :=
  Set.iUnion₂_subset fun _x H => conjugates_subset_normal (h H)

/-- The set of conjugates of `s` is closed under conjugation. -/
theorem conj_mem_conjugatesOfSet {x c : G} :
    x ∈ conjugatesOfSet s → c * x * c⁻¹ ∈ conjugatesOfSet s := fun H => by
  rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩
  exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

end Group

namespace Subgroup

open Group

variable {s : Set G}

/-- The normal closure of a set `s` is the subgroup closure of all the conjugates of
elements of `s`. It is the smallest normal subgroup containing `s`. -/
def normalClosure (s : Set G) : Subgroup G :=
  closure (conjugatesOfSet s)

theorem conjugatesOfSet_subset_normalClosure : conjugatesOfSet s ⊆ normalClosure s :=
  subset_closure

theorem subset_normalClosure : s ⊆ normalClosure s :=
  Set.Subset.trans subset_conjugatesOfSet conjugatesOfSet_subset_normalClosure

theorem le_normalClosure {H : Subgroup G} : H ≤ normalClosure ↑H := fun _ h =>
  subset_normalClosure h

/-- The normal closure of `s` is a normal subgroup. -/
instance normalClosure_normal : (normalClosure s).Normal :=
  ⟨fun n h g => by
    refine Subgroup.closure_induction h (fun x hx => ?_) ?_ (fun x y ihx ihy => ?_) fun x ihx => ?_
    · exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
    · simpa using (normalClosure s).one_mem
    · rw [← conj_mul]
      exact mul_mem ihx ihy
    · rw [← conj_inv]
      exact inv_mem ihx⟩

/-- The normal closure of `s` is the smallest normal subgroup containing `s`. -/
theorem normalClosure_le_normal {N : Subgroup G} [N.Normal] (h : s ⊆ N) : normalClosure s ≤ N := by
  intro a w
  refine closure_induction w (fun x hx => ?_) ?_ (fun x y ihx ihy => ?_) fun x ihx => ?_
  · exact conjugatesOfSet_subset h hx
  · exact one_mem _
  · exact mul_mem ihx ihy
  · exact inv_mem ihx

theorem normalClosure_subset_iff {N : Subgroup G} [N.Normal] : s ⊆ N ↔ normalClosure s ≤ N :=
  ⟨normalClosure_le_normal, Set.Subset.trans subset_normalClosure⟩

theorem normalClosure_mono {s t : Set G} (h : s ⊆ t) : normalClosure s ≤ normalClosure t :=
  normalClosure_le_normal (Set.Subset.trans h subset_normalClosure)

theorem normalClosure_eq_iInf :
    normalClosure s = ⨅ (N : Subgroup G) (_ : Normal N) (_ : s ⊆ N), N :=
  le_antisymm (le_iInf fun N => le_iInf fun hN => le_iInf normalClosure_le_normal)
    (iInf_le_of_le (normalClosure s)
      (iInf_le_of_le (by infer_instance) (iInf_le_of_le subset_normalClosure le_rfl)))

@[simp]
theorem normalClosure_eq_self (H : Subgroup G) [H.Normal] : normalClosure ↑H = H :=
  le_antisymm (normalClosure_le_normal rfl.subset) le_normalClosure

-- @[simp] -- Porting note (#10618): simp can prove this
theorem normalClosure_idempotent : normalClosure ↑(normalClosure s) = normalClosure s :=
  normalClosure_eq_self _

theorem closure_le_normalClosure {s : Set G} : closure s ≤ normalClosure s := by
  simp only [subset_normalClosure, closure_le]

@[simp]
theorem normalClosure_closure_eq_normalClosure {s : Set G} :
    normalClosure ↑(closure s) = normalClosure s :=
  le_antisymm (normalClosure_le_normal closure_le_normalClosure) (normalClosure_mono subset_closure)

/-- The normal core of a subgroup `H` is the largest normal subgroup of `G` contained in `H`,
as shown by `Subgroup.normalCore_eq_iSup`. -/
def normalCore (H : Subgroup G) : Subgroup G where
  carrier := { a : G | ∀ b : G, b * a * b⁻¹ ∈ H }
  one_mem' a := by rw [mul_one, mul_inv_self]; exact H.one_mem
  inv_mem' {a} h b := (congr_arg (· ∈ H) conj_inv).mp (H.inv_mem (h b))
  mul_mem' {a b} ha hb c := (congr_arg (· ∈ H) conj_mul).mp (H.mul_mem (ha c) (hb c))

theorem normalCore_le (H : Subgroup G) : H.normalCore ≤ H := fun a h => by
  rw [← mul_one a, ← inv_one, ← one_mul a]
  exact h 1

instance normalCore_normal (H : Subgroup G) : H.normalCore.Normal :=
  ⟨fun a h b c => by
    rw [mul_assoc, mul_assoc, ← mul_inv_rev, ← mul_assoc, ← mul_assoc]; exact h (c * b)⟩

theorem normal_le_normalCore {H : Subgroup G} {N : Subgroup G} [hN : N.Normal] :
    N ≤ H.normalCore ↔ N ≤ H :=
  ⟨ge_trans H.normalCore_le, fun h_le n hn g => h_le (hN.conj_mem n hn g)⟩

theorem normalCore_mono {H K : Subgroup G} (h : H ≤ K) : H.normalCore ≤ K.normalCore :=
  normal_le_normalCore.mpr (H.normalCore_le.trans h)

theorem normalCore_eq_iSup (H : Subgroup G) :
    H.normalCore = ⨆ (N : Subgroup G) (_ : Normal N) (_ : N ≤ H), N :=
  le_antisymm
    (le_iSup_of_le H.normalCore
      (le_iSup_of_le H.normalCore_normal (le_iSup_of_le H.normalCore_le le_rfl)))
    (iSup_le fun _ => iSup_le fun _ => iSup_le normal_le_normalCore.mpr)

@[simp]
theorem normalCore_eq_self (H : Subgroup G) [H.Normal] : H.normalCore = H :=
  le_antisymm H.normalCore_le (normal_le_normalCore.mpr le_rfl)

-- @[simp] -- Porting note (#10618): simp can prove this
theorem normalCore_idempotent (H : Subgroup G) : H.normalCore.normalCore = H.normalCore :=
  H.normalCore.normalCore_eq_self

end Subgroup

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 (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_top_iff_surjective {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_iff_surjective

/-- 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_top_of_surjective {N} [Group N] (f : G →* N) (hf : Function.Surjective f) :
    f.range = (⊤ : Subgroup N) :=
  range_top_iff_surjective.2 hf

@[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 x y 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_self, map_one] }

@[to_additive]
theorem mem_ker (f : G →* M) {x : G} : x ∈ f.ker ↔ f x = 1 :=
  Iff.rfl

@[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_self, map_one]
  · rw [← one_mul x, ← mul_inv_self y, mul_assoc, map_mul, f.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 x 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') :
    (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
  SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

@[to_additive]
theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
    (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, f.mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_self y)]⟩

@[to_additive (attr := simp)]
lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (and_true_iff _).symm

@[to_additive (attr := simp)]
lemma ker_snd : ker (snd G G') = .prod ⊤ ⊥ := SetLike.ext fun _ => (true_and_iff _).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 (Subgroup.gc_map_comap f) (Subgroup.gi N).gc
    (Subgroup.gi G).gc fun _t => rfl

end MonoidHom

namespace Subgroup

variable {N : Type*} [Group N] (H : Subgroup G)

@[to_additive]
theorem Normal.map {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective f) :
    (H.map f).Normal := by
  rw [← normalizer_eq_top, ← top_le_iff, ← f.range_top_of_surjective hf, f.range_eq_map, ←
    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

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_top_of_surjective _ h).symm ▸ 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 (le_top.trans (f.range_top_of_surjective hf).ge)

@[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_iff]

@[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 (le_top.trans (ge_of_eq (f.range_top_of_surjective hf)))
    (le_top.trans (ge_of_eq (f.range_top_of_surjective hf)))

@[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
      "The preimage of the normalizer is equal to the normalizer of the preimage of
      a surjective function."]
theorem comap_normalizer_eq_of_surjective (H : Subgroup G) {f : N →* G}
    (hf : Function.Surjective f) : H.normalizer.comap f = (H.comap f).normalizer :=
  le_antisymm (le_normalizer_comap f)
    (by
      intro x hx
      simp only [mem_comap, mem_normalizer_iff] at *
      intro n
      rcases hf n with ⟨y, rfl⟩
      simp [hx y])

@[to_additive]
theorem comap_normalizer_eq_of_injective_of_le_range {N : Type*} [Group N] (H : Subgroup G)
    {f : N →* G} (hf : Function.Injective f) (h : H.normalizer ≤ f.range) :
    comap f H.normalizer = (comap f H).normalizer := by
  apply Subgroup.map_injective hf
  rw [map_comap_eq_self h]
  apply le_antisymm
  · refine le_trans (le_of_eq ?_) (map_mono (le_normalizer_comap _))
    rw [map_comap_eq_self h]
  · refine le_trans (le_normalizer_map f) (le_of_eq ?_)
    rw [map_comap_eq_self (le_trans le_normalizer h)]

@[to_additive]
theorem subgroupOf_normalizer_eq {H N : Subgroup G} (h : H.normalizer ≤ N) :
    H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer := by
  apply comap_normalizer_eq_of_injective_of_le_range
  · exact Subtype.coe_injective
  simpa

/-- The image of the normalizer is equal to the normalizer of the image of an isomorphism. -/
@[to_additive
      "The image of the normalizer is equal to the normalizer of the image of an
      isomorphism."]
theorem map_equiv_normalizer_eq (H : Subgroup G) (f : G ≃* N) :
    H.normalizer.map f.toMonoidHom = (H.map f.toMonoidHom).normalizer := by
  ext x
  simp only [mem_normalizer_iff, mem_map_equiv]
  rw [f.toEquiv.forall_congr]
  intro
  erw [f.toEquiv.symm_apply_apply]
  simp only [map_mul, map_inv]
  erw [f.toEquiv.symm_apply_apply]

/-- The image of the normalizer is equal to the normalizer of the image of a bijective
  function. -/
@[to_additive
      "The image of the normalizer is equal to the normalizer of the image of a bijective
        function."]
theorem map_normalizer_eq_of_bijective (H : Subgroup G) {f : G →* N} (hf : Function.Bijective f) :
    H.normalizer.map f = (H.map f).normalizer :=
  map_equiv_normalizer_eq H (MulEquiv.ofBijective f hf)

end Subgroup

namespace MonoidHom

variable {G₁ G₂ G₃ : Type*} [Group G₁] [Group G₂] [Group G₃]
variable (f : G₁ →* G₂) (f_inv : G₂ → G₁)

/-- Auxiliary definition used to define `liftOfRightInverse` -/
@[to_additive "Auxiliary definition used to define `liftOfRightInverse`"]
def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) :
    G₂ →* G₃ where
  toFun b := g (f_inv b)
  map_one' := hg (hf 1)
  map_mul' := by
    intro x y
    rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
    apply hg
    rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]
    simp only [hf _]

@[to_additive (attr := simp)]
theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃)
    (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x := by
  dsimp [liftOfRightInverseAux]
  rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
  apply hg
  rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]
  simp only [hf _]

/-- `liftOfRightInverse f hf g hg` is the unique group homomorphism `φ`

* such that `φ.comp f = g` (`MonoidHom.liftOfRightInverse_comp`),
* where `f : G₁ →+* G₂` has a RightInverse `f_inv` (`hf`),
* and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.

See `MonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.

```
   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
```
 -/
@[to_additive
      "`liftOfRightInverse f f_inv hf g hg` is the unique additive group homomorphism `φ`
      * such that `φ.comp f = g` (`AddMonoidHom.liftOfRightInverse_comp`),
      * where `f : G₁ →+ G₂` has a RightInverse `f_inv` (`hf`),
      * and `g : G₂ →+ G₃` satisfies `hg : f.ker ≤ g.ker`.
      See `AddMonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.
      ```
         G₁.
         |  \\
       f |   \\ g
         |    \\
         v     \\⌟
         G₂----> G₃
            ∃!φ
      ```"]
def liftOfRightInverse (hf : Function.RightInverse f_inv f) :
    { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) where
  toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2
  invFun φ := ⟨φ.comp f, fun x hx => (mem_ker _).mpr <| by simp [(mem_ker _).mp hx]⟩
  left_inv g := by
    ext
    simp only [comp_apply, liftOfRightInverseAux_comp_apply, Subtype.coe_mk]
  right_inv φ := by
    ext b
    simp [liftOfRightInverseAux, hf b]

/-- A non-computable version of `MonoidHom.liftOfRightInverse` for when no computable right
inverse is available, that uses `Function.surjInv`. -/
@[to_additive (attr := simp)
      "A non-computable version of `AddMonoidHom.liftOfRightInverse` for when no
      computable right inverse is available."]
noncomputable abbrev liftOfSurjective (hf : Function.Surjective f) :
    { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) :=
  f.liftOfRightInverse (Function.surjInv hf) (Function.rightInverse_surjInv hf)

@[to_additive (attr := simp)]
theorem liftOfRightInverse_comp_apply (hf : Function.RightInverse f_inv f)
    (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) (x : G₁) :
    (f.liftOfRightInverse f_inv hf g) (f x) = g.1 x :=
  f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x

@[to_additive (attr := simp)]
theorem liftOfRightInverse_comp (hf : Function.RightInverse f_inv f)
    (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) : (f.liftOfRightInverse f_inv hf g).comp f = g :=
  MonoidHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g

@[to_additive]
theorem eq_liftOfRightInverse (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃)
    (hg : f.ker ≤ g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) :
    h = f.liftOfRightInverse f_inv hf ⟨g, hg⟩ := by
  simp_rw [← hh]
  exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

end MonoidHom

variable {N : Type*} [Group N]

namespace Subgroup

-- Here `H.Normal` is an explicit argument so we can use dot notation with `comap`.
@[to_additive]
theorem Normal.comap {H : Subgroup N} (hH : H.Normal) (f : G →* N) : (H.comap f).Normal :=
  ⟨fun _ => by simp (config := { contextual := true }) [Subgroup.mem_comap, hH.conj_mem]⟩

@[to_additive]
instance (priority := 100) normal_comap {H : Subgroup N} [nH : H.Normal] (f : G →* N) :
    (H.comap f).Normal :=
  nH.comap _

-- Here `H.Normal` is an explicit argument so we can use dot notation with `subgroupOf`.
@[to_additive]
theorem Normal.subgroupOf {H : Subgroup G} (hH : H.Normal) (K : Subgroup G) :
    (H.subgroupOf K).Normal :=
  hH.comap _

@[to_additive]
instance (priority := 100) normal_subgroupOf {H N : Subgroup G} [N.Normal] :
    (N.subgroupOf H).Normal :=
  Subgroup.normal_comap _

theorem map_normalClosure (s : Set G) (f : G →* N) (hf : Surjective f) :
    (normalClosure s).map f = normalClosure (f '' s) := by
  have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
  apply le_antisymm
  · simp [map_le_iff_le_comap, normalClosure_le_normal, coe_comap,
      ← Set.image_subset_iff, subset_normalClosure]
  · exact normalClosure_le_normal (Set.image_subset f subset_normalClosure)

theorem comap_normalClosure (s : Set N) (f : G ≃* N) :
    normalClosure (f ⁻¹' s) = (normalClosure s).comap f := by
  have := Set.preimage_equiv_eq_image_symm s f.toEquiv
  simp_all [comap_equiv_eq_map_symm, map_normalClosure s f.symm f.symm.surjective]

lemma Normal.of_map_injective {G H : Type*} [Group G] [Group H] {φ : G →* H}
    (hφ : Function.Injective φ) {L : Subgroup G} (n : (L.map φ).Normal) : L.Normal :=
  L.comap_map_eq_self_of_injective hφ ▸ n.comap φ

theorem Normal.of_map_subtype {K : Subgroup G} {L : Subgroup K}
    (n : (Subgroup.map K.subtype L).Normal) : L.Normal :=
  n.of_map_injective K.subtype_injective

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

@[to_additive]
theorem normal_subgroupOf_iff {H K : Subgroup G} (hHK : H ≤ K) :
    (H.subgroupOf K).Normal ↔ ∀ h k, h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H :=
  ⟨fun hN h k hH hK => hN.conj_mem ⟨h, hHK hH⟩ hH ⟨k, hK⟩, fun hN =>
    { conj_mem := fun h hm k => hN h.1 k.1 hm k.2 }⟩

@[to_additive]
instance prod_subgroupOf_prod_normal {H₁ K₁ : Subgroup G} {H₂ K₂ : Subgroup N}
    [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal] :
    ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal where
  conj_mem n hgHK g :=
    ⟨h₁.conj_mem ⟨(n : G × N).fst, (mem_prod.mp n.2).1⟩ hgHK.1
        ⟨(g : G × N).fst, (mem_prod.mp g.2).1⟩,
      h₂.conj_mem ⟨(n : G × N).snd, (mem_prod.mp n.2).2⟩ hgHK.2
        ⟨(g : G × N).snd, (mem_prod.mp g.2).2⟩⟩

@[to_additive]
instance prod_normal (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] :
    (H.prod K).Normal where
  conj_mem n hg g :=
    ⟨hH.conj_mem n.fst (Subgroup.mem_prod.mp hg).1 g.fst,
      hK.conj_mem n.snd (Subgroup.mem_prod.mp hg).2 g.snd⟩

@[to_additive]
theorem inf_subgroupOf_inf_normal_of_right (A B' B : Subgroup G) (hB : B' ≤ B)
    [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal :=
  { conj_mem := fun {n} hn g =>
      ⟨mul_mem (mul_mem (mem_inf.1 g.2).1 (mem_inf.1 n.2).1) <|
        show ↑g⁻¹ ∈ A from (inv_mem (mem_inf.1 g.2).1),
        (normal_subgroupOf_iff hB).mp hN n g hn.2 (mem_inf.mp g.2).2⟩ }

@[to_additive]
theorem inf_subgroupOf_inf_normal_of_left {A' A : Subgroup G} (B : Subgroup G) (hA : A' ≤ A)
    [hN : (A'.subgroupOf A).Normal] : ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal :=
  { conj_mem := fun n hn g =>
      ⟨(normal_subgroupOf_iff hA).mp hN n g hn.1 (mem_inf.mp g.2).1,
        mul_mem (mul_mem (mem_inf.1 g.2).2 (mem_inf.1 n.2).2) <|
        show ↑g⁻¹ ∈ B from (inv_mem (mem_inf.1 g.2).2)⟩ }

@[to_additive]
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
  have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
  rwa [mul_assoc, mul_assoc, mul_right_inv, mul_one] at this

/-- Elements of disjoint, normal subgroups commute. -/
@[to_additive "Elements of disjoint, normal subgroups commute."]
theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal)
    (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y := by
  suffices x * y * x⁻¹ * y⁻¹ = 1 by
    show x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      -- Porting note: Previous code was:
      -- simpa
      simp only [this, mul_inv_rev, inv_inv]
  apply hdis.le_bot
  constructor
  · suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
    exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)
  · show x * y * x⁻¹ * y⁻¹ ∈ H₂
    apply H₂.mul_mem _ (H₂.inv_mem hy)
    apply hH₂.conj_mem _ hy

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 x y 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

open Subgroup

theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N}
    {hg' : g' ∈ N} (hc : IsConj g g') (ht : normalClosure ({⟨g, hg⟩} : Set N) = ⊤) :
    normalClosure ({⟨g', hg'⟩} : Set N) = ⊤ := by
  obtain ⟨c, rfl⟩ := isConj_iff.1 hc
  have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
    rintro ⟨x, hx⟩
    exact hn.conj_mem _ hx c
  have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.restrict N).codRestrict _ h) := by
    rintro ⟨x, hx⟩
    refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
    · have h := hn.conj_mem _ hx c⁻¹
      rwa [inv_inv] at h
    simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_self, one_mul]
    rw [mul_assoc, mul_inv_self, mul_one]
  rw [eq_top_iff, ← MonoidHom.range_top_of_surjective _ hs, MonoidHom.range_eq_map]
  refine le_trans (map_mono (eq_top_iff.1 ht)) (map_le_iff_le_comap.2 (normalClosure_le_normal ?_))
  rw [Set.singleton_subset_iff, SetLike.mem_coe]
  simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
    MonoidHom.restrict_apply, mem_comap]
  exact subset_normalClosure (Set.mem_singleton _)

end IsConj

namespace ConjClasses

/-- The conjugacy classes that are not trivial. -/
def noncenter (G : Type*) [Monoid G] : Set (ConjClasses G) :=
  {x | x.carrier.Nontrivial}

@[simp] lemma mem_noncenter {G} [Monoid G] (g : ConjClasses G) :
  g ∈ noncenter G ↔ g.carrier.Nontrivial := Iff.rfl

end ConjClasses

assert_not_exists Multiset
assert_not_exists Ring