chore(Units): better follow the naming convention (#26251)

YaelDillies · YaelDillies · commit cd11c28c6a0d · 2025-07-12T14:51:06.000Z
Moves
* `Units.ext` -&gt; `Units.val_injective`
* `Units.eq_iff` -&gt; `Units.val_inj`
diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean
@@ -1215,7 +1215,7 @@ variable (G₀ : Type*) [CommGroupWithZero G₀] [DecidableEq G₀]
 instance (priority := 100) : NormalizedGCDMonoid G₀ where
   normUnit x := if h : x = 0 then 1 else (Units.mk0 x h)⁻¹
   normUnit_zero := dif_pos rfl
-  normUnit_mul {x y} x0 y0 := Units.eq_iff.1 (by simp [x0, y0, mul_comm])
+  normUnit_mul {x y} x0 y0 := Units.ext <| by simp [x0, y0, mul_comm]
   normUnit_coe_units u := by simp
   gcd a b := if a = 0 ∧ b = 0 then 0 else 1
   lcm a b := if a = 0 ∨ b = 0 then 0 else 1
diff --git a/Mathlib/Algebra/Group/Center.lean b/Mathlib/Algebra/Group/Center.lean
@@ -257,7 +257,7 @@ theorem subset_center_units : ((↑) : Mˣ → M) ⁻¹' center M ⊆ Set.center
   fun _ ha => by
   rw [_root_.Semigroup.mem_center_iff]
   intro _
-  rw [← Units.eq_iff, Units.val_mul, Units.val_mul, ha.comm]
+  rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]
 
 @[to_additive (attr := simp)]
 theorem units_inv_mem_center {a : Mˣ} (ha : ↑a ∈ Set.center M) : ↑a⁻¹ ∈ Set.center M := by
diff --git a/Mathlib/Algebra/Group/Units/Defs.lean b/Mathlib/Algebra/Group/Units/Defs.lean
@@ -92,7 +92,8 @@ instance instInv : Inv αˣ :=
 attribute [instance] AddUnits.instNeg
 
 /-- See Note [custom simps projection] -/
-@[to_additive "See Note [custom simps projection]"]
+@[to_additive
+"See Note [custom simps projection]"]
 def Simps.val_inv (u : αˣ) : α := ↑(u⁻¹)
 
 initialize_simps_projections Units (as_prefix val, val_inv → null, inv → val_inv, as_prefix val_inv)
@@ -104,15 +105,20 @@ initialize_simps_projections AddUnits
 theorem val_mk (a : α) (b h₁ h₂) : ↑(Units.mk a b h₁ h₂) = a :=
   rfl
 
-@[to_additive (attr := ext)]
-theorem ext : Function.Injective (val : αˣ → α)
+@[to_additive]
+theorem val_injective : Function.Injective (val : αˣ → α)
   | ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
     simp only at e; subst v'; congr
     simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁
 
+@[to_additive (attr := ext)]
+theorem ext {u v : αˣ} (huv : u.val = v.val) : u = v := val_injective huv
+
 @[to_additive (attr := norm_cast)]
-theorem eq_iff {a b : αˣ} : (a : α) = b ↔ a = b :=
-  ext.eq_iff
+theorem val_inj {a b : αˣ} : (a : α) = b ↔ a = b :=
+  val_injective.eq_iff
+
+@[to_additive (attr := deprecated val_inj (since := "2025-06-21"))] alias eq_iff := val_inj
 
 /-- Units have decidable equality if the base `Monoid` has decidable equality. -/
 @[to_additive "Additive units have decidable equality
@@ -173,7 +179,7 @@ theorem val_one : ((1 : αˣ) : α) = 1 :=
   rfl
 
 @[to_additive (attr := simp, norm_cast)]
-theorem val_eq_one {a : αˣ} : (a : α) = 1 ↔ a = 1 := by rw [← Units.val_one, eq_iff]
+theorem val_eq_one {a : αˣ} : (a : α) = 1 ↔ a = 1 := by rw [← Units.val_one, val_inj]
 
 @[to_additive (attr := simp)]
 theorem inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁ :=
@@ -490,7 +496,7 @@ theorem unit_spec (h : IsUnit a) : ↑h.unit = a :=
 
 @[to_additive (attr := simp)]
 theorem unit_one (h : IsUnit (1 : M)) : h.unit = 1 :=
-  Units.eq_iff.1 rfl
+  Units.ext rfl
 
 @[to_additive]
 theorem unit_mul (ha : IsUnit a) (hb : IsUnit b) : (ha.mul hb).unit = ha.unit * hb.unit :=
diff --git a/Mathlib/Algebra/Group/Units/Hom.lean b/Mathlib/Algebra/Group/Units/Hom.lean
@@ -108,8 +108,7 @@ variable {M}
 theorem coeHom_apply (x : Mˣ) : coeHom M x = ↑x := rfl
 
 @[to_additive]
-theorem coeHom_injective : Function.Injective (coeHom M) :=
-  Units.ext
+theorem coeHom_injective : Function.Injective (coeHom M) := Units.val_injective
 
 section DivisionMonoid
 
diff --git a/Mathlib/Algebra/Order/Monoid/Units.lean b/Mathlib/Algebra/Order/Monoid/Units.lean
@@ -29,17 +29,17 @@ theorem val_lt_val [Monoid α] [Preorder α] {a b : αˣ} : (a : α) < b ↔ a <
 
 @[to_additive]
 instance instPartialOrderUnits [Monoid α] [PartialOrder α] : PartialOrder αˣ :=
-  PartialOrder.lift val Units.ext
+  PartialOrder.lift val val_injective
 
 @[to_additive]
 instance [Monoid α] [LinearOrder α] : LinearOrder αˣ :=
-  LinearOrder.lift' val Units.ext
+  LinearOrder.lift' val val_injective
 
 /-- `val : αˣ → α` as an order embedding. -/
 @[to_additive (attr := simps -fullyApplied)
   "`val : add_units α → α` as an order embedding."]
 def orderEmbeddingVal [Monoid α] [LinearOrder α] : αˣ ↪o α :=
-  ⟨⟨val, ext⟩, Iff.rfl⟩
+  ⟨⟨val, val_injective⟩, .rfl⟩
 
 @[to_additive (attr := simp, norm_cast)]
 theorem max_val [Monoid α] [LinearOrder α] {a b : αˣ} : (max a b).val = max a.val b.val :=
diff --git a/Mathlib/Algebra/Polynomial/UnitTrinomial.lean b/Mathlib/Algebra/Polynomial/UnitTrinomial.lean
@@ -241,7 +241,7 @@ theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k
   replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm
   rw [(isUnit_C.mpr v.isUnit).mul_right_inj] at h
   rw [binomial_eq_binomial u.ne_zero w.ne_zero] at h
-  simp only [add_left_inj, Units.eq_iff] at h
+  simp only [add_left_inj, Units.val_inj] at h
   rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
   · exact Or.inl (hq.trans hp.symm)
   · refine Or.inr ?_
@@ -268,7 +268,7 @@ theorem irreducible_aux3 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k
     mul_right_inj' (show 2 * (v : ℤ) ≠ 0 from mul_ne_zero two_ne_zero v.ne_zero)] at hadd
   replace hadd :=
     (Int.isUnit_add_isUnit_eq_isUnit_add_isUnit w.isUnit u.isUnit z.isUnit x.isUnit).mp hadd
-  simp only [Units.eq_iff] at hadd
+  simp only [Units.val_inj] at hadd
   rcases hadd with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
   · exact irreducible_aux2 hkm hmn hkm' hmn' u v w hp hq h
   · rw [← mirror_inj, trinomial_mirror hkm' hmn' w.ne_zero u.ne_zero] at hq
diff --git a/Mathlib/Algebra/Ring/Units.lean b/Mathlib/Algebra/Ring/Units.lean
@@ -39,8 +39,7 @@ protected theorem val_neg (u : αˣ) : (↑(-u) : α) = -u :=
 protected theorem coe_neg_one : ((-1 : αˣ) : α) = -1 :=
   rfl
 
-instance : HasDistribNeg αˣ :=
-  Units.ext.hasDistribNeg _ Units.val_neg Units.val_mul
+instance : HasDistribNeg αˣ := val_injective.hasDistribNeg _ Units.val_neg val_mul
 
 @[field_simps]
 theorem neg_divp (a : α) (u : αˣ) : -(a /ₚ u) = -a /ₚ u := by simp only [divp, neg_mul]
diff --git a/Mathlib/Analysis/Complex/Isometry.lean b/Mathlib/Analysis/Complex/Isometry.lean
@@ -157,4 +157,4 @@ theorem det_rotation (a : Circle) : LinearMap.det ((rotation a).toLinearEquiv :
 /-- The determinant of `rotation` (as a linear equiv) is equal to `1`. -/
 @[simp]
 theorem linearEquiv_det_rotation (a : Circle) : LinearEquiv.det (rotation a).toLinearEquiv = 1 := by
-  rw [← Units.eq_iff, LinearEquiv.coe_det, det_rotation, Units.val_one]
+  rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]
diff --git a/Mathlib/Data/Complex/Determinant.lean b/Mathlib/Data/Complex/Determinant.lean
@@ -26,7 +26,7 @@ theorem det_conjAe : LinearMap.det conjAe.toLinearMap = -1 := by
 /-- The determinant of `conjAe`, as a linear equiv. -/
 @[simp]
 theorem linearEquiv_det_conjAe : LinearEquiv.det conjAe.toLinearEquiv = -1 := by
-  rw [← Units.eq_iff, LinearEquiv.coe_det, AlgEquiv.toLinearEquiv_toLinearMap, det_conjAe,
+  rw [← Units.val_inj, LinearEquiv.coe_det, AlgEquiv.toLinearEquiv_toLinearMap, det_conjAe,
     Units.coe_neg_one]
 
 end Complex
diff --git a/Mathlib/Data/Fintype/Units.lean b/Mathlib/Data/Fintype/Units.lean
@@ -28,7 +28,7 @@ theorem Fintype.card_units_int : Fintype.card ℤˣ = 2 := rfl
 instance [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ :=
   Fintype.ofEquiv _ (unitsEquivProdSubtype α).symm
 
-instance [Monoid α] [Finite α] : Finite αˣ := Finite.of_injective _ Units.ext
+instance [Monoid α] [Finite α] : Finite αˣ := .of_injective _ Units.val_injective
 
 variable (α)
 
diff --git a/Mathlib/Data/ZMod/Units.lean b/Mathlib/Data/ZMod/Units.lean
@@ -104,7 +104,7 @@ lemma eq_unit_mul_divisor {N : ℕ} (a : ZMod N) :
     exact ⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩
   -- Lift it arbitrarily to a unit mod `N`.
   obtain ⟨u, hu⟩ := (unitsMap_surjective (⟨d, mul_comm d N₀ ▸ hN₀⟩ : N₀ ∣ N)) hu₀.unit
-  rw [unitsMap_def, ← Units.eq_iff, Units.coe_map, IsUnit.unit_spec, MonoidHom.coe_coe] at hu
+  rw [unitsMap_def, ← Units.val_inj, Units.coe_map, IsUnit.unit_spec, MonoidHom.coe_coe] at hu
   refine ⟨u.val, u.isUnit, ?_⟩
   rw [← natCast_zmod_val a, ← natCast_zmod_val u.1, ha₀, ← Nat.cast_mul,
     natCast_eq_natCast_iff, mul_comm _ d, Nat.ModEq]
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -302,7 +302,7 @@ theorem sum_pow_lt_card_sub_one (i : ℕ) (h : i < q - 1) : ∑ x : K, x ^ i = 0
   · simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]
   classical
     have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
-    let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.ext⟩
+    let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.val_injective⟩
     have : univ.map φ = univ \ {0} := by
       ext x
       simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
@@ -752,7 +752,7 @@ theorem unit_isSquare_iff (hF : ringChar F ≠ 2) (a : Fˣ) :
     constructor
     · rintro ⟨y, rfl⟩
       rw [← pow_two, ← pow_mul, hodd]
-      apply_fun Units.val using Units.ext
+      apply_fun Units.val using Units.val_injective
       push_cast
       exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
     · subst a; intro h
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -343,7 +343,7 @@ theorem orderOf_submonoid {H : Submonoid G} (y : H) : orderOf (y : G) = orderOf
 
 @[to_additive]
 theorem orderOf_units {y : Gˣ} : orderOf (y : G) = orderOf y :=
-  orderOf_injective (Units.coeHom G) Units.ext y
+  orderOf_injective (Units.coeHom G) Units.val_injective y
 
 /-- If the order of `x` is finite, then `x` is a unit with inverse `x ^ (orderOf x - 1)`. -/
 @[to_additive (attr := simps) "If the additive order of `x` is finite, then `x` is an additive
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
@@ -212,7 +212,7 @@ theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) : star x ∈ pi
   refine ⟨star y, ?_, by simp only [hy₂, Units.coe_star]⟩
   rw [← hy₂] at hx₃
   have hy₃ : y * star y = 1 := by
-    rw [← Units.eq_iff]
+    rw [← Units.val_inj]
     simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]
   apply_fun fun x => y⁻¹ * x at hy₃
   simp only [inv_mul_cancel_left, mul_one] at hy₃
diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean
@@ -401,7 +401,7 @@ theorem det_symm (f : M ≃ₗ[R] M) : LinearEquiv.det f.symm = LinearEquiv.det
 @[simp]
 theorem det_conj (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') :
     LinearEquiv.det ((e.symm.trans f).trans e) = LinearEquiv.det f := by
-  rw [← Units.eq_iff, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
+  rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
 
 attribute [irreducible] LinearEquiv.det
 
diff --git a/Mathlib/LinearAlgebra/Lagrange.lean b/Mathlib/LinearAlgebra/Lagrange.lean
@@ -527,7 +527,7 @@ theorem eval_nodal_derivative_eval_node_eq [DecidableEq ι] {i : ι} (hi : i ∈
   nodal (G : Set Rˣ).toFinset ((↑) : Rˣ → R) = X ^ (Fintype.card G) - 1 := by
   have h : degree (1 : R[X]) < degree ((X : R[X]) ^ Fintype.card G) := by simp [Fintype.card_pos]
   apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
-  · exact Set.injOn_of_injective Units.ext
+  · exact Units.val_injective.injOn
   · simp
   · rw [degree_sub_eq_left_of_degree_lt h, degree_nodal, Set.toFinset_card, degree_pow, degree_X,
       nsmul_eq_mul, mul_one, Nat.cast_inj]
diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
@@ -272,7 +272,7 @@ def center_equiv_rootsOfUnity' (i : n) :
     simpa [← hr, Submonoid.smul_def, Units.smul_def] using smul_one_eq_diagonal r
   right_inv a := by
     obtain ⟨⟨a, _⟩, ha⟩ := a
-    exact SetCoe.ext <| Units.eq_iff.mp <| by simp
+    exact SetCoe.ext <| Units.ext <| by simp
   map_mul' A B := by
     dsimp
     ext
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -1176,12 +1176,12 @@ theorem prod_eq_iff_prod_pow_moebius_eq_of_nonzero [CommGroupWithZero R] {f g :
         (forall_congr' fun n => ?_) <;>
     refine imp_congr_right fun hn => ?_
   · dsimp
-    rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0,
+    rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
       prod_congr rfl _]
     intro x hx
     rw [dif_pos (Nat.pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
   · dsimp
-    rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0,
+    rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
       prod_congr rfl _]
     intro x hx
     rw [dif_pos (Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal hx)),
@@ -1262,12 +1262,12 @@ theorem prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero [CommGroupWithZero R]
         (forall_congr' fun n => ?_) <;>
     refine imp_congr_right fun hn => ?_
   · dsimp
-    rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0,
+    rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
       prod_congr rfl _]
     intro x hx
     rw [dif_pos (Nat.pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
   · dsimp
-    rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0,
+    rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
       prod_congr rfl _]
     intro x hx
     rw [dif_pos (Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal hx)),
diff --git a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean
@@ -311,11 +311,11 @@ lemma Odd.not_even [NeZero (2 : S)] (hψ : Odd ψ) : ¬Even ψ :=
   not_and'.mp ψ.not_even_and_odd hψ
 
 lemma Odd.toUnitHom_eval_neg_one (hψ : ψ.Odd) : ψ.toUnitHom (-1) = -1 := by
-  rw [← Units.eq_iff, MulChar.coe_toUnitHom]
+  rw [← Units.val_inj, MulChar.coe_toUnitHom]
   exact hψ
 
 lemma Even.toUnitHom_eval_neg_one (hψ : ψ.Even) : ψ.toUnitHom (-1) = 1 := by
-  rw [← Units.eq_iff, MulChar.coe_toUnitHom]
+  rw [← Units.val_inj, MulChar.coe_toUnitHom]
   exact hψ
 
 lemma Odd.eval_neg (x : ZMod m) (hψ : ψ.Odd) : ψ (- x) = - ψ x := by
diff --git a/Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean b/Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean
@@ -25,7 +25,7 @@ lemma gaussSum_aux_of_mulShift (χ : DirichletCharacter R N) {d : ℕ}
     ext1 y
     simpa only [Int.cast_mul, Int.cast_natCast, mulShift_apply, mul_assoc, one_apply]
       using DFunLike.ext_iff.mp he (a * y)
-  rw [← Units.eq_iff, Units.val_one, ZMod.unitsMap_def, Units.coe_map] at hu
+  rw [← Units.val_inj, Units.val_one, ZMod.unitsMap_def, Units.coe_map] at hu
   have : ZMod.castHom hd (ZMod d) u.val = ((u.val.val : ℤ) : ZMod d) := by simp
   rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
     ZMod.intCast_eq_intCast_iff_dvd_sub] at hu
@@ -37,7 +37,7 @@ lemma factorsThrough_of_gaussSum_ne_zero [IsDomain R] {χ : DirichletCharacter R
     χ.FactorsThrough d := by
   rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]
   intro u hu
-  rw [MonoidHom.mem_ker, ← Units.eq_iff, MulChar.coe_toUnitHom]
+  rw [MonoidHom.mem_ker, ← Units.val_inj, MulChar.coe_toUnitHom]
   simpa only [Units.val_one, ne_eq, h_ne, not_false_eq_true, mul_eq_right₀] using
     gaussSum_aux_of_mulShift e χ hd he hu
 
diff --git a/Mathlib/NumberTheory/LucasPrimality.lean b/Mathlib/NumberTheory/LucasPrimality.lean
@@ -42,7 +42,7 @@ theorem lucas_primality (p : ℕ) (a : ZMod p) (ha : a ^ (p - 1) = 1)
   apply (Nat.card_units_zmod_lt_sub_one hp1).antisymm
   let a' : (ZMod p)ˣ := Units.mkOfMulEqOne a _ (by rwa [← pow_succ', tsub_add_eq_add_tsub hp1])
   calc p - 1 = orderOf a := (orderOf_eq_of_pow_and_pow_div_prime (tsub_pos_of_lt hp1) ha hd).symm
-    _ = orderOf a' := orderOf_injective (Units.coeHom _) Units.ext a'
+    _ = orderOf a' := orderOf_injective (Units.coeHom _) Units.val_injective a'
     _ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ
 
 /-- If `p` is prime, then there exists an `a` such that `a^(p-1) = 1 mod p`
@@ -58,7 +58,7 @@ theorem reverse_lucas_primality (p : ℕ) (hP : p.Prime) :
     rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card,
       ← Nat.prime_iff_card_units]
   have h2 := tsub_pos_iff_lt.2 hP.one_lt
-  rw [← orderOf_injective (Units.coeHom _) Units.ext _, orderOf_eq_iff h2] at h1
+  rw [← orderOf_injective (Units.coeHom _) Units.val_injective _, orderOf_eq_iff h2] at h1
   refine ⟨g, h1.1, fun q hq hqd ↦ ?_⟩
   replace hq := hq.one_lt
   exact h1.2 _ (Nat.div_lt_self h2 hq) (Nat.div_pos (Nat.le_of_dvd h2 hqd) (zero_lt_one.trans hq))
diff --git a/Mathlib/NumberTheory/MulChar/Basic.lean b/Mathlib/NumberTheory/MulChar/Basic.lean
@@ -154,7 +154,7 @@ theorem coe_toUnitHom (χ : MulChar R R') (a : Rˣ) : ↑(χ.toUnitHom a) = χ a
 noncomputable def ofUnitHom (f : Rˣ →* R'ˣ) : MulChar R R' where
   toFun := by classical exact fun x => if hx : IsUnit x then f hx.unit else 0
   map_one' := by
-    have h1 : (isUnit_one.unit : Rˣ) = 1 := Units.eq_iff.mp rfl
+    have h1 : (isUnit_one.unit : Rˣ) = 1 := Units.ext rfl
     simp only [h1, dif_pos, Units.val_eq_one, map_one, isUnit_one]
   map_mul' := by
     classical
@@ -163,7 +163,7 @@ noncomputable def ofUnitHom (f : Rˣ →* R'ˣ) : MulChar R R' where
       · simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
         by_cases hy : IsUnit y
         · simp only [hy, dif_pos]
-          have hm : (IsUnit.mul_iff.mpr ⟨hx, hy⟩).unit = hx.unit * hy.unit := Units.eq_iff.mp rfl
+          have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
           rw [hm, map_mul]
           norm_cast
         · simp only [hy, not_false_iff, dif_neg, mul_zero]
@@ -350,7 +350,7 @@ theorem pow_apply' (χ : MulChar R R') {n : ℕ} (hn : n ≠ 0) (a : R) : (χ ^
 
 lemma equivToUnitHom_mul_apply (χ₁ χ₂ : MulChar R R') (a : Rˣ) :
     equivToUnitHom (χ₁ * χ₂) a = equivToUnitHom χ₁ a * equivToUnitHom χ₂ a := by
-  apply_fun ((↑) : R'ˣ → R') using Units.ext
+  apply_fun ((↑) : R'ˣ → R') using Units.val_injective
   push_cast
   simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]
 
@@ -560,7 +560,7 @@ theorem sum_one_eq_card_units [DecidableEq R] :
     (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 :=
       Finset.sum_congr rfl fun a _ => ?_
     _ = ((Finset.univ : Finset R).filter IsUnit).card := Finset.sum_boole _ _
-    _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.ext⟩).card := ?_
+    _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.val_injective⟩).card := ?_
     _ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)
   · split_ifs with h
     · exact one_apply_coe h.unit
diff --git a/Mathlib/NumberTheory/NumberField/Units/Basic.lean b/Mathlib/NumberTheory/NumberField/Units/Basic.lean
@@ -65,7 +65,7 @@ instance : CoeHTC (𝓞 K)ˣ K :=
   ⟨fun x => algebraMap _ K (Units.val x)⟩
 
 theorem coe_injective : Function.Injective ((↑) : (𝓞 K)ˣ → K) :=
-  RingOfIntegers.coe_injective.comp Units.ext
+  RingOfIntegers.coe_injective.comp Units.val_injective
 
 variable {K}
 
@@ -196,7 +196,7 @@ theorem torsion_eq_one_or_neg_one_of_odd_finrank [NumberField K]
     · linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion _ x.1).1 x.2)]
     · exact Or.intro_left _ (orderOf_eq_one_iff.1 hi)
     · rw [← orderOf_units, CharP.orderOf_eq_two_iff 0 (by decide)] at hi
-      simp [← Units.eq_iff, ← Units.eq_iff, Units.val_neg, Units.val_one, hi]
+      simp [← Units.val_inj, ← Units.val_inj, Units.val_neg, Units.val_one, hi]
 
 theorem torsionOrder_eq_two_of_odd_finrank [NumberField K]
     (h : Odd (Module.finrank ℚ K)) : torsionOrder K = 2 := by
diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean
@@ -128,7 +128,7 @@ theorem ClassGroup.mk_eq_mk_of_coe_ideal {I J : (FractionalIdeal R⁰ <| Fractio
     have : IsUnit (mk' (FractionRing R) x ⟨y, mem_nonZeroDivisors_of_ne_zero hy⟩) := by
       simpa only [isUnit_iff_ne_zero, ne_eq, mk'_eq_zero_iff_eq_zero] using hx
     refine ⟨this.unit, ?_⟩
-    rw [mul_comm, ← Units.eq_iff, Units.val_mul, coe_toPrincipalIdeal]
+    rw [mul_comm, ← Units.val_inj, Units.val_mul, coe_toPrincipalIdeal]
     convert
       (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h
 
@@ -159,7 +159,7 @@ theorem ClassGroup.induction {P : ClassGroup R → Prop}
   QuotientGroup.induction_on x fun I => by
     have : I = (Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv)
       (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv I) := by
-      simp [← Units.eq_iff]
+      simp [← Units.val_inj]
     rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]
     exact h _
 
@@ -199,7 +199,7 @@ theorem ClassGroup.equiv_mk (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRi
   rw [ClassGroup.equiv, ClassGroup.mk_def]
   simp only [ClassGroup, QuotientGroup.congr_mk']
   congr
-  rw [← Units.eq_iff, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]
+  rw [← Units.val_inj, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]
   exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _
 
 @[simp]
@@ -251,7 +251,7 @@ theorem ClassGroup.equiv_mk0 [IsDedekindDomain R] (I : (Ideal R)⁰) :
       QuotientGroup.mk' (toPrincipalIdeal R K).range (FractionalIdeal.mk0 K I) := by
   rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]
   congr 1
-  simp [← Units.eq_iff]
+  simp [← Units.val_inj]
 
 theorem ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring [IsDedekindDomain R] {I J : (Ideal R)⁰} :
     ClassGroup.mk0 I =
diff --git a/Mathlib/RingTheory/Fintype.lean b/Mathlib/RingTheory/Fintype.lean
diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean
diff --git a/Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean b/Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean
diff --git a/Mathlib/RingTheory/Valuation/RankOne.lean b/Mathlib/RingTheory/Valuation/RankOne.lean
diff --git a/Mathlib/Topology/Algebra/Constructions.lean b/Mathlib/Topology/Algebra/Constructions.lean
diff --git a/Mathlib/Topology/Algebra/IsOpenUnits.lean b/Mathlib/Topology/Algebra/IsOpenUnits.lean
diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean
