diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
index 06d576a2260d79..d9cc082ed5ba50 100644
--- a/Mathlib/GroupTheory/Subgroup/Basic.lean
+++ b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -1373,6 +1373,15 @@ theorem coe_comap (K : Subgroup N) (f : G →* N) : (K.comap f : Set G) = f ⁻
 #align subgroup.coe_comap Subgroup.coe_comap
 #align add_subgroup.coe_comap AddSubgroup.coe_comap
 
+@[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
@@ -2729,6 +2738,14 @@ theorem subgroupOf_range_eq_of_le {G₁ G₂ : Type*} [Group G₁] [Group G₂]
 #align monoid_hom.subgroup_of_range_eq_of_le MonoidHom.subgroupOf_range_eq_of_le
 #align add_monoid_hom.add_subgroup_of_range_eq_of_le AddMonoidHom.addSubgroupOf_range_eq_of_le
 
+@[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 :=
@@ -2930,6 +2947,14 @@ lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (and_true
 @[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
diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean
index 5116c5f26ac8c5..d6af9170d4bac7 100644
--- a/Mathlib/LinearAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/Basic.lean
@@ -578,6 +578,22 @@ theorem map_toAddSubmonoid' (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M)
   SetLike.coe_injective rfl
 #align submodule.map_to_add_submonoid' Submodule.map_toAddSubmonoid'
 
+@[simp]
+theorem _root_.AddMonoidHom.coe_toIntLinearMap_map {A A₂ : Type*} [AddCommGroup A] [AddCommGroup A₂]
+    (f : A →+ A₂) (s : AddSubgroup A) :
+    (AddSubgroup.toIntSubmodule s).map f.toIntLinearMap =
+      AddSubgroup.toIntSubmodule (s.map f) := rfl
+
+@[simp]
+theorem _root_.MonoidHom.coe_toAdditive_map {G G₂ : Type*} [Group G] [Group G₂] (f : G →* G₂)
+    (s : Subgroup G) :
+    s.toAddSubgroup.map (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.map f) := rfl
+
+@[simp]
+theorem _root_.AddMonoidHom.coe_toMultiplicative_map {G G₂ : Type*} [AddGroup G] [AddGroup G₂]
+    (f : G →+ G₂) (s : AddSubgroup G) :
+    s.toSubgroup.map (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.map f) := rfl
+
 @[simp]
 theorem mem_map {f : F} {p : Submodule R M} {x : M₂} : x ∈ map f p ↔ ∃ y, y ∈ p ∧ f y = x :=
   Iff.rfl
@@ -669,6 +685,12 @@ theorem comap_coe (f : F) (p : Submodule R₂ M₂) : (comap f p : Set M) = f 
   rfl
 #align submodule.comap_coe Submodule.comap_coe
 
+@[simp]
+theorem AddMonoidHom.coe_toIntLinearMap_comap {A A₂ : Type*} [AddCommGroup A] [AddCommGroup A₂]
+    (f : A →+ A₂) (s : AddSubgroup A₂) :
+    (AddSubgroup.toIntSubmodule s).comap f.toIntLinearMap =
+      AddSubgroup.toIntSubmodule (s.comap f) := rfl
+
 @[simp]
 theorem mem_comap {f : F} {p : Submodule R₂ M₂} : x ∈ comap f p ↔ f x ∈ p :=
   Iff.rfl
@@ -1122,6 +1144,11 @@ lemma range_domRestrict_le_range [RingHomSurjective τ₁₂] (f : M →ₛₗ[
   rintro x ⟨⟨y, hy⟩, rfl⟩
   exact LinearMap.mem_range_self f y
 
+@[simp]
+theorem _root_.AddMonoidHom.coe_toIntLinearMap_range {M M₂ : Type*} [AddCommGroup M]
+    [AddCommGroup M₂] (f : M →+ M₂) :
+    LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range := rfl
+
 /-- A linear map version of `AddMonoidHom.eqLocusM` -/
 def eqLocus (f g : F) : Submodule R M :=
   { (f : M →+ M₂).eqLocusM g with
@@ -1288,6 +1315,10 @@ theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0 :=
   ⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩
 #align linear_map.ker_eq_top LinearMap.ker_eq_top
 
+@[simp]
+theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂]
+    (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker := rfl
+
 section
 
 variable [RingHomSurjective τ₁₂]
diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
index 2765fc6bf4a5af..ab40e8f28ec4b0 100644
--- a/Mathlib/NumberTheory/NumberField/Units.lean
+++ b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -139,7 +139,7 @@ instance [NumberField K] : Finite (torsion K) := inferInstance
 /-- The torsion subgroup is cylic. -/
 instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _
 
-/-- The order of the torsion subgroup as positive integer. -/
+/-- The order of the torsion subgroup as a positive integer. -/
 def torsionOrder [NumberField K] : ℕ+ := ⟨Fintype.card (torsion K), Fintype.card_pos⟩
 
 /-- If `k` does not divide `torsionOrder` then there are no nontrivial roots of unity of
@@ -178,7 +178,7 @@ This section is devoted to the proof of Dirichlet's unit theorem.
 We define a group morphism from `(𝓞 K)ˣ` to `{w : InfinitePlace K // w ≠ w₀} → ℝ` where `w₀` is a
 distinguished (arbitrary) infinite place, prove that its kernel is the torsion subgroup (see
 `logEmbedding_eq_zero_iff`) and that its image, called `unitLattice`, is a full `ℤ`-lattice. It
-follows that `unitLattice` is a free `ℤ`-module (see `unitLattice_moduleFree `) of rank
+follows that `unitLattice` is a free `ℤ`-module (see `instModuleFree_unitLattice`) of rank
 `card (InfinitePlaces K) - 1` (see `unitLattice_rank`). To prove that the `unitLattice` is a full
 `ℤ`-lattice, we need to prove that it is discrete (see `unitLattice_inter_ball_finite`) and that it
 spans the full space over `ℝ` (see `unitLattice_span_eq_top`); this is the main part of the proof,
@@ -401,8 +401,8 @@ theorem seq_norm_le (n : ℕ) :
 
 /-- Construct a unit associated to the place `w₁`. The family, for `w₁ ≠ w₀`, formed by the
 image by the `logEmbedding` of these units  is `ℝ`-linearly independent, see
-`unit_lattice_span_eq_top`. -/
-theorem exists_unit (w₁ : InfinitePlace K) :
+`unitLattice_span_eq_top`. -/
+theorem exists_unit (w₁ : InfinitePlace K ) :
     ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0 := by
   obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K < (convexBodyLtFactor K) * B := by
     simp_rw [mul_comm]
@@ -512,9 +512,8 @@ def unitLatticeEquiv : (unitLattice K) ≃ₗ[ℤ] Additive ((𝓞 K)ˣ ⧸ (tor
     (QuotientAddGroup.quotientKerEquivOfSurjective
       (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))) (fun x => ?_))
   · ext
-    rw [AddMonoidHom.mem_ker, AddMonoidHom.mem_ker, logEmbedding_eq_zero_iff,
-      MonoidHom.toAdditive_apply_apply, ofMul_eq_zero, QuotientGroup.mk'_apply,
-      QuotientGroup.eq_one_iff]
+    rw [MonoidHom.coe_toAdditive_ker, QuotientGroup.ker_mk', AddMonoidHom.mem_ker,
+      logEmbedding_eq_zero_iff]
     rfl
   · refine ⟨Additive.ofMul x.out', ?_⟩
     simp only [MonoidHom.toAdditive_apply_apply, toMul_ofMul, QuotientGroup.mk'_apply,
@@ -527,6 +526,26 @@ instance : Module.Free ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
 instance : Module.Finite ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
   Module.Finite.equiv (unitLatticeEquiv K)
 
+-- Note that we prove this instance first and then deduce from it the instance
+-- `Monoid.FG (𝓞 K)ˣ`, and not the other way around, due to no `Subgroup` version
+-- of `Submodule.fg_of_fg_map_of_fg_inf_ker` existing.
+instance : Module.Finite ℤ (Additive (𝓞 K)ˣ) := by
+  rw [Module.finite_def]
+  refine Submodule.fg_of_fg_map_of_fg_inf_ker
+    (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap ?_ ?_
+  · rw [Submodule.map_top, LinearMap.range_eq_top.mpr
+      (by exact QuotientGroup.mk'_surjective (torsion K)), ← Module.finite_def]
+    infer_instance
+  · rw [inf_of_le_right le_top, AddMonoidHom.coe_toIntLinearMap_ker, MonoidHom.coe_toAdditive_ker,
+      QuotientGroup.ker_mk', Submodule.fg_iff_add_subgroup_fg,
+      AddSubgroup.toIntSubmodule_toAddSubgroup, ← AddGroup.fg_iff_addSubgroup_fg]
+    have : Finite (Subgroup.toAddSubgroup (torsion K)) := (inferInstance : Finite (torsion K))
+    exact AddGroup.fg_of_finite
+
+instance : Monoid.FG (𝓞 K)ˣ := by
+  rw [Monoid.fg_iff_add_fg, ← AddGroup.fg_iff_addMonoid_fg, ← Module.Finite.iff_addGroup_fg]
+  infer_instance
+
 theorem rank_modTorsion :
     FiniteDimensional.finrank ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) = rank K := by
   rw [← LinearEquiv.finrank_eq (unitLatticeEquiv K), unitLattice_rank]
@@ -543,7 +562,7 @@ def fundSystem : Fin (rank K) → (𝓞 K)ˣ :=
 
 /-- The exponents that appear in the unique decomposition of a unit as the product of
 a root of unity and powers of the units of the fundamental system `fundSystem` (see
-`exist_unique_eq_mul_prod`) are given by the representation of the unit of `basisModTorsion`. -/
+`exist_unique_eq_mul_prod`) are given by the representation of the unit on `basisModTorsion`. -/
 theorem fun_eq_repr {x ζ : (𝓞 K)ˣ} {f : Fin (rank K) → ℤ} (hζ : ζ ∈ torsion K)
     (h : x = ζ * ∏ i, (fundSystem K i) ^ (f i)) :
     f = (basisModTorsion K).repr (Additive.ofMul ↑x) := by