refactor: Unify the different versions of mul_eq_one (#14996)

YaelDillies · YaelDillies · commit ce6b0a984cb0 · 2024-08-11T05:10:28.000Z
Replace `mul_eq_one_iff` and `Associates.mul_eq_one_iff` by a single lemma `mul_eq_one`. Rename `mul_eq_one_iff'` to `mul_eq_one_iff_of_one_le`. Similarly for the additive versions.
diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -365,7 +365,7 @@ theorem ballot_problem :
     exacts [Nat.cast_le.2 qp.le, ENNReal.natCast_ne_top _]
   rwa [ENNReal.toReal_eq_toReal (measure_lt_top _ _).ne] at this
   simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
-    add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
+    add_eq_zero, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
     not_false_iff, and_true_iff]
   push_neg
   exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
diff --git a/Mathlib/Algebra/Associated/Basic.lean b/Mathlib/Algebra/Associated/Basic.lean
@@ -844,20 +844,15 @@ theorem mk_pow (a : α) (n : ℕ) : Associates.mk (a ^ n) = Associates.mk a ^ n
 theorem dvd_eq_le : ((· ∣ ·) : Associates α → Associates α → Prop) = (· ≤ ·) :=
   rfl
 
-theorem mul_eq_one_iff {x y : Associates α} : x * y = 1 ↔ x = 1 ∧ y = 1 :=
-  Iff.intro
-    (Quotient.inductionOn₂ x y fun a b h =>
-      have : a * b ~ᵤ 1 := Quotient.exact h
-      ⟨Quotient.sound <| associated_one_of_associated_mul_one this,
-        Quotient.sound <| associated_one_of_associated_mul_one (b := a) (by rwa [mul_comm])⟩)
-    (by simp (config := { contextual := true }))
-
-theorem units_eq_one (u : (Associates α)ˣ) : u = 1 :=
-  Units.ext (mul_eq_one_iff.1 u.val_inv).1
-
 instance uniqueUnits : Unique (Associates α)ˣ where
-  default := 1
-  uniq := Associates.units_eq_one
+  uniq := by
+    rintro ⟨a, b, hab, hba⟩
+    revert hab hba
+    exact Quotient.inductionOn₂ a b $ fun a b hab hba ↦ Units.ext $ Quotient.sound $
+      associated_one_of_associated_mul_one $ Quotient.exact hab
+
+@[deprecated (since := "2024-07-22")] alias mul_eq_one_iff := mul_eq_one
+@[deprecated (since := "2024-07-22")] protected alias units_eq_one := Subsingleton.elim
 
 @[simp]
 theorem coe_unit_eq_one (u : (Associates α)ˣ) : (u : Associates α) = 1 := by
diff --git a/Mathlib/Algebra/BigOperators/Associated.lean b/Mathlib/Algebra/BigOperators/Associated.lean
@@ -129,7 +129,7 @@ theorem rel_associated_iff_map_eq_map {p q : Multiset α} :
 theorem prod_eq_one_iff {p : Multiset (Associates α)} :
     p.prod = 1 ↔ ∀ a ∈ p, (a : Associates α) = 1 :=
   Multiset.induction_on p (by simp)
-    (by simp (config := { contextual := true }) [mul_eq_one_iff, or_imp, forall_and])
+    (by simp (config := { contextual := true }) [mul_eq_one, or_imp, forall_and])
 
 theorem prod_le_prod {p q : Multiset (Associates α)} (h : p ≤ q) : p.prod ≤ q.prod := by
   haveI := Classical.decEq (Associates α)
@@ -146,7 +146,7 @@ variable [CancelCommMonoidWithZero α]
 
 theorem exists_mem_multiset_le_of_prime {s : Multiset (Associates α)} {p : Associates α}
     (hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a :=
-  Multiset.induction_on s (fun ⟨d, Eq⟩ => (hp.ne_one (mul_eq_one_iff.1 Eq.symm).1).elim)
+  Multiset.induction_on s (fun ⟨d, Eq⟩ => (hp.ne_one (mul_eq_one.1 Eq.symm).1).elim)
     fun a s ih h =>
     have : p ≤ a * s.prod := by simpa using h
     match Prime.le_or_le hp this with
diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@@ -147,7 +147,7 @@ theorem prod_eq_one_iff_of_one_le' :
       (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
     intro a s ha ih H
     have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
-    rw [prod_insert ha, mul_eq_one_iff' (H _ <| mem_insert_self _ _) (one_le_prod' this),
+    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
       forall_mem_insert, ih this]
 
 @[to_additive sum_eq_zero_iff_of_nonpos]
diff --git a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
@@ -3,6 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
+import Mathlib.Algebra.Group.Units
 import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Algebra.NeZero
@@ -110,11 +111,11 @@ theorem one_le (a : α) : 1 ≤ a :=
 theorem bot_eq_one : (⊥ : α) = 1 :=
   le_antisymm bot_le (one_le ⊥)
 
---TODO: This is a special case of `mul_eq_one`. We need the instance
--- `CanonicallyOrderedCommMonoid α → Unique αˣ`
-@[to_additive (attr := simp)]
-theorem mul_eq_one_iff : a * b = 1 ↔ a = 1 ∧ b = 1 :=
-  mul_eq_one_iff' (one_le _) (one_le _)
+@[to_additive] instance CanonicallyOrderedCommMonoid.toUniqueUnits : Unique αˣ where
+  uniq a := Units.ext ((mul_eq_one_iff_of_one_le (α := α) (one_le _) $ one_le _).1 a.mul_inv).1
+
+@[deprecated (since := "2024-07-24")] alias mul_eq_one_iff := mul_eq_one
+@[deprecated (since := "2024-07-24")] alias add_eq_zero_iff := add_eq_zero
 
 @[to_additive (attr := simp)]
 theorem le_one_iff_eq_one : a ≤ 1 ↔ a = 1 :=
@@ -129,7 +130,7 @@ theorem eq_one_or_one_lt (a : α) : a = 1 ∨ 1 < a := (one_le a).eq_or_lt.imp_l
 
 @[to_additive (attr := simp) add_pos_iff]
 theorem one_lt_mul_iff : 1 < a * b ↔ 1 < a ∨ 1 < b := by
-  simp only [one_lt_iff_ne_one, Ne, mul_eq_one_iff, not_and_or]
+  simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]
 
 @[to_additive]
 theorem exists_one_lt_mul_of_lt (h : a < b) : ∃ (c : _) (_ : 1 < c), a * c = b := by
diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@@ -954,7 +954,7 @@ section PartialOrder
 variable [PartialOrder α]
 
 @[to_additive]
-theorem mul_eq_one_iff' [CovariantClass α α (· * ·) (· ≤ ·)]
+theorem mul_eq_one_iff_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
     a * b = 1 ↔ a = 1 ∧ b = 1 :=
   Iff.intro
@@ -969,6 +969,9 @@ theorem mul_eq_one_iff' [CovariantClass α α (· * ·) (· ≤ ·)]
     -- `fun ⟨ha', hb'⟩ => by rw [ha', hb', mul_one]`,
     -- had its `to_additive`-ization fail due to some bug
 
+@[deprecated (since := "2024-07-24")] alias mul_eq_one_iff' := mul_eq_one_iff_of_one_le
+@[deprecated (since := "2024-07-24")] alias add_eq_zero_iff' := add_eq_zero_iff_of_nonneg
+
 section Left
 
 variable [CovariantClass α α (· * ·) (· ≤ ·)] {a b : α}
diff --git a/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean b/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
@@ -915,7 +915,7 @@ lemma mul_self_add_mul_self_eq_zero [IsRightCancelAdd α] [NoZeroDivisors α]
     [ZeroLEOneClass α] [ExistsAddOfLE α] [PosMulMono α]
     [CovariantClass α α (· + ·) (· ≤ ·)] [CovariantClass α α (· + ·) (· < ·)] :
     a * a + b * b = 0 ↔ a = 0 ∧ b = 0 := by
-  rw [add_eq_zero_iff', mul_self_eq_zero (M₀ := α), mul_self_eq_zero (M₀ := α)] <;>
+  rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := α), mul_self_eq_zero (M₀ := α)] <;>
     apply mul_self_nonneg
 
 lemma eq_zero_of_mul_self_add_mul_self_eq_zero [IsRightCancelAdd α] [NoZeroDivisors α]
diff --git a/Mathlib/Algebra/Polynomial/Monic.lean b/Mathlib/Algebra/Polynomial/Monic.lean
@@ -220,7 +220,7 @@ theorem Monic.eq_one_of_isUnit (hm : Monic p) (hpu : IsUnit p) : p = 1 := by
   nontriviality R
   obtain ⟨q, h⟩ := hpu.exists_right_inv
   have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
-  rw [h, natDegree_one, eq_comm, add_eq_zero_iff] at this
+  rw [h, natDegree_one, eq_comm, add_eq_zero] at this
   exact hm.natDegree_eq_zero_iff_eq_one.mp this.1
 
 theorem Monic.isUnit_iff (hm : p.Monic) : IsUnit p ↔ p = 1 :=
diff --git a/Mathlib/Algebra/Polynomial/RingDivision.lean b/Mathlib/Algebra/Polynomial/RingDivision.lean
@@ -179,7 +179,7 @@ theorem natDegree_eq_zero_of_isUnit (h : IsUnit p) : natDegree p = 0 := by
   nontriviality R
   obtain ⟨q, hq⟩ := h.exists_right_inv
   have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
-  rw [hq, natDegree_one, eq_comm, add_eq_zero_iff] at this
+  rw [hq, natDegree_one, eq_comm, add_eq_zero] at this
   exact this.1
 
 theorem degree_eq_zero_of_isUnit [Nontrivial R] (h : IsUnit p) : degree p = 0 :=
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -1170,7 +1170,8 @@ variable [LinearOrderedCommRing R] {a : ℍ[R]}
 @[simp]
 theorem normSq_eq_zero : normSq a = 0 ↔ a = 0 := by
   refine ⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩
-  rw [normSq_def', add_eq_zero_iff', add_eq_zero_iff', add_eq_zero_iff'] at h
+  rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
+    at h
   · exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2)
   all_goals apply_rules [sq_nonneg, add_nonneg]
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
@@ -148,7 +148,7 @@ theorem mapMono_comp (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [Mono i'] [Mono i] :
   have eq : Δ.len = Δ''.len + (k + k' + 2) := by omega
   rw [mapMono_eq_zero K (i' ≫ i) _ _]; rotate_left
   · by_contra h
-    simp only [self_eq_add_right, h, add_eq_zero_iff, and_false] at eq
+    simp only [self_eq_add_right, h, add_eq_zero, and_false] at eq
   · by_contra h
     simp only [h.1, add_right_inj] at eq
     omega
diff --git a/Mathlib/Analysis/BoundedVariation.lean b/Mathlib/Analysis/BoundedVariation.lean
@@ -292,7 +292,7 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ 
         apply Finset.sum_congr rfl fun i _hi => ?_
         dsimp only [w]
         simp only [← Npos, Nat.not_lt_zero, Nat.add_succ_sub_one, add_zero, if_false,
-          add_eq_zero_iff, Nat.one_ne_zero, false_and_iff, Nat.succ_add_sub_one, zero_add]
+          add_eq_zero, Nat.one_ne_zero, false_and_iff, Nat.succ_add_sub_one, zero_add]
         rw [add_comm 1 i]
       _ = ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) := by
         rw [Finset.range_eq_Ico]
diff --git a/Mathlib/Analysis/Convex/Basic.lean b/Mathlib/Analysis/Convex/Basic.lean
@@ -511,7 +511,8 @@ theorem Convex.exists_mem_add_smul_eq (h : Convex 𝕜 s) {x y : E} {p q : 𝕜}
   rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
   · use x, hx
     simp
-  · replace hpq : 0 < p + q := (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff' hp hq).1 hpq)
+  · replace hpq : 0 < p + q :=
+      (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
     refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
     simp only [smul_add, smul_smul, mul_div_cancel₀ _ hpq.ne']
 
diff --git a/Mathlib/Analysis/MeanInequalitiesPow.lean b/Mathlib/Analysis/MeanInequalitiesPow.lean
@@ -162,8 +162,8 @@ private theorem add_rpow_le_one_of_add_le_one {p : ℝ} (a b : ℝ≥0) (hab : a
 theorem add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0) (hp1 : 1 ≤ p) : a ^ p + b ^ p ≤ (a + b) ^ p := by
   have hp_pos : 0 < p := by positivity
   by_cases h_zero : a + b = 0
-  · simp [add_eq_zero_iff.mp h_zero, hp_pos.ne']
-  have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero_iff] at h_zero
+  · simp [add_eq_zero.mp h_zero, hp_pos.ne']
+  have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero] at h_zero
   have h_add : a / (a + b) + b / (a + b) = 1 := by rw [div_add_div_same, div_self h_zero]
   have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
   rw [div_rpow a (a + b), div_rpow b (a + b)] at h
diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean
@@ -758,10 +758,10 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1)
       apply (Nat.succ_pred_eq_of_pos _).symm
       exact (zero_le i.val).trans_lt (i.2.trans_le (Nat.sub_le n 1))
     simp only [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
-      Finset.mem_univ, forall_true_left, Finset.mem_filter, add_eq_zero_iff, and_false,
+      Finset.mem_univ, forall_true_left, Finset.mem_filter, add_eq_zero, and_false,
       add_left_inj, false_or, true_and]
     erw [Set.mem_setOf_eq]
-    simp [this, false_or_iff, add_right_inj, add_eq_zero_iff, one_ne_zero, false_and_iff,
+    simp [this, false_or_iff, add_right_inj, add_eq_zero, one_ne_zero, false_and_iff,
       Fin.val_mk]
     constructor
     · intro h
diff --git a/Mathlib/Data/Finsupp/Antidiagonal.lean b/Mathlib/Data/Finsupp/Antidiagonal.lean
@@ -63,7 +63,7 @@ theorem antidiagonal_single (a : α) (n : ℕ) :
     simp_rw [single_apply, Finsupp.add_apply] at h ⊢
     obtain rfl | hai := Decidable.eq_or_ne a i
     · exact ⟨if_pos rfl, if_pos rfl⟩
-    · simp_rw [if_neg hai, _root_.add_eq_zero_iff] at h ⊢
+    · simp_rw [if_neg hai, add_eq_zero] at h ⊢
       exact h.imp Eq.symm Eq.symm
   · rintro ⟨a, b, rfl, rfl, rfl⟩
     exact (single_add _ _ _).symm
diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -40,7 +40,7 @@ theorem factorization_eq_zero_iff_remainder {p r : ℕ} (i : ℕ) (pp : p.Prime)
   refine ⟨pp, ?_, ?_⟩
   · rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]
   · contrapose! hr0
-    exact (add_eq_zero_iff.mp hr0).2
+    exact (add_eq_zero.1 hr0).2
 
 /-- The only numbers with empty prime factorization are `0` and `1` -/
 theorem factorization_eq_zero_iff' (n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1 := by
diff --git a/Mathlib/Data/Nat/WithBot.lean b/Mathlib/Data/Nat/WithBot.lean
@@ -28,7 +28,7 @@ theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := b
   · simp [WithBot.bot_add]
   cases m
   · simp [WithBot.add_bot]
-  simp [← WithBot.coe_add, _root_.add_eq_zero_iff]
+  simp [← WithBot.coe_add, add_eq_zero_iff_of_nonneg]
 
 theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by
   cases n
diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean
@@ -587,15 +587,15 @@ theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Si
       · rfl
       · have : size rrl = 0 ∧ size rrr = 0 := by
           have := balancedSz_zero.1 hr.1.symm
-          rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this
+          rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
         cases sr.2.2.2.1.size_eq_zero.1 this.1
         cases sr.2.2.2.2.size_eq_zero.1 this.2
         obtain rfl : rrs = 1 := sr.2.2.1
         rw [if_neg, if_pos, rotateL_node, if_pos]; · rfl
         all_goals dsimp only [size]; decide
       · have : size rll = 0 ∧ size rlr = 0 := by
           have := balancedSz_zero.1 hr.1
-          rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this
+          rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
         cases sr.2.1.2.1.size_eq_zero.1 this.1
         cases sr.2.1.2.2.size_eq_zero.1 this.2
         obtain rfl : rls = 1 := sr.2.1.1
@@ -614,15 +614,15 @@ theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Si
       · rfl
       · have : size lrl = 0 ∧ size lrr = 0 := by
           have := balancedSz_zero.1 hl.1.symm
-          rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this
+          rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
         cases sl.2.2.2.1.size_eq_zero.1 this.1
         cases sl.2.2.2.2.size_eq_zero.1 this.2
         obtain rfl : lrs = 1 := sl.2.2.1
         rw [if_neg, if_pos, rotateR_node, if_neg]; · rfl
         all_goals dsimp only [size]; decide
       · have : size lll = 0 ∧ size llr = 0 := by
           have := balancedSz_zero.1 hl.1
-          rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this
+          rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
         cases sl.2.1.2.1.size_eq_zero.1 this.1
         cases sl.2.1.2.2.size_eq_zero.1 this.2
         obtain rfl : lls = 1 := sl.2.1.1
@@ -670,7 +670,7 @@ theorem balanceL_eq_balance {l x r} (sl : Sized l) (sr : Sized r) (H1 : size l =
   · cases' l with ls ll lx lr
     · have : size rl = 0 ∧ size rr = 0 := by
         have := H1 rfl
-        rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this
+        rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
       cases sr.2.1.size_eq_zero.1 this.1
       cases sr.2.2.size_eq_zero.1 this.2
       rw [sr.eq_node']; rfl
@@ -1011,7 +1011,7 @@ theorem Valid'.node4L {l} {x : α} {m} {y : α} {r o₁ o₂} (hl : Valid' o₁
       BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1) from
     Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2
   rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
-  · rw [hm.2.size_eq, Nat.succ_inj', add_eq_zero_iff] at m1
+  · rw [hm.2.size_eq, Nat.succ_inj', add_eq_zero] at m1
     rw [l0, m1.1, m1.2]; revert r0; rcases size r with (_ | _ | _) <;>
       [decide; decide; (intro r0; unfold BalancedSz delta; omega)]
   · rcases Nat.eq_zero_or_pos (size r) with r0 | r0
diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
@@ -150,7 +150,7 @@ theorem cos_angle_add_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
   by_cases hxy : ‖x + y‖ = 0
   · have h' := norm_add_sq_eq_norm_sq_add_norm_sq_real h
     rw [hxy, zero_mul, eq_comm,
-      add_eq_zero_iff' (mul_self_nonneg ‖x‖) (mul_self_nonneg ‖y‖), mul_self_eq_zero] at h'
+      add_eq_zero_iff_of_nonneg (mul_self_nonneg ‖x‖) (mul_self_nonneg ‖y‖), mul_self_eq_zero] at h'
     simp [h'.1]
   · exact div_mul_cancel₀ _ hxy
 
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
@@ -167,7 +167,7 @@ theorem posDef_prod_iff [PartialOrder P] [CovariantClass P P (· + ·) (· ≤ 
   · rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
     refine ⟨⟨hle₁, hle₂⟩, ?_⟩
     rintro ⟨x₁, x₂⟩ (hx : Q₁ x₁ + Q₂ x₂ = 0)
-    rw [add_eq_zero_iff' (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
+    rw [add_eq_zero_iff_of_nonneg (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
     rwa [Prod.mk_eq_zero]
 
 theorem PosDef.prod [PartialOrder P] [CovariantClass P P (· + ·) (· ≤ ·)]
diff --git a/Mathlib/MeasureTheory/Covering/Besicovitch.lean b/Mathlib/MeasureTheory/Covering/Besicovitch.lean
@@ -781,7 +781,7 @@ theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measur
       rw [ENNReal.div_lt_iff, one_mul]
       · conv_lhs => rw [← add_zero (N : ℝ≥0∞)]
         exact ENNReal.add_lt_add_left (ENNReal.natCast_ne_top N) zero_lt_one
-      · simp only [true_or_iff, add_eq_zero_iff, Ne, not_false_iff, one_ne_zero, and_false_iff]
+      · simp only [true_or_iff, add_eq_zero, Ne, not_false_iff, one_ne_zero, and_false_iff]
       · simp only [ENNReal.natCast_ne_top, Ne, not_false_iff, or_true_iff]
     rw [zero_mul] at C
     apply le_bot_iff.1
diff --git a/Mathlib/MeasureTheory/Decomposition/Jordan.lean b/Mathlib/MeasureTheory/Decomposition/Jordan.lean
@@ -454,7 +454,7 @@ theorem totalVariation_neg (s : SignedMeasure α) : (-s).totalVariation = s.tota
 
 theorem null_of_totalVariation_zero (s : SignedMeasure α) {i : Set α}
     (hs : s.totalVariation i = 0) : s i = 0 := by
-  rw [totalVariation, Measure.coe_add, Pi.add_apply, add_eq_zero_iff] at hs
+  rw [totalVariation, Measure.coe_add, Pi.add_apply, add_eq_zero] at hs
   rw [← toSignedMeasure_toJordanDecomposition s, toSignedMeasure, VectorMeasure.coe_sub,
     Pi.sub_apply, Measure.toSignedMeasure_apply, Measure.toSignedMeasure_apply]
   by_cases hi : MeasurableSet i
@@ -484,7 +484,7 @@ theorem totalVariation_absolutelyContinuous_iff (s : SignedMeasure α) (μ : Mea
     all_goals
       refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
       have := h hS₂
-      rw [totalVariation, Measure.add_apply, add_eq_zero_iff] at this
+      rw [totalVariation, Measure.add_apply, add_eq_zero] at this
     exacts [this.1, this.2]
   · refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
     rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
diff --git a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
@@ -126,7 +126,7 @@ theorem singularPart_mutuallySingular (s : SignedMeasure α) (μ : Measure α) :
   · obtain ⟨i, hi, hpos, hneg⟩ := s.toJordanDecomposition.mutuallySingular
     rw [s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ] at hpos
     rw [s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ] at hneg
-    rw [add_apply, add_eq_zero_iff] at hpos hneg
+    rw [add_apply, add_eq_zero] at hpos hneg
     exact ⟨i, hi, hpos.1, hneg.1⟩
   · rw [not_haveLebesgueDecomposition_iff] at hl
     cases' hl with hp hn
diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean
@@ -592,7 +592,7 @@ theorem ae_smul_measure {p : α → Prop} [Monoid R] [DistribMulAction R ℝ≥0
 
 theorem ae_add_measure_iff {p : α → Prop} {ν} :
     (∀ᵐ x ∂μ + ν, p x) ↔ (∀ᵐ x ∂μ, p x) ∧ ∀ᵐ x ∂ν, p x :=
-  add_eq_zero_iff
+  add_eq_zero
 
 theorem ae_eq_comp' {ν : Measure β} {f : α → β} {g g' : β → δ} (hf : AEMeasurable f μ)
     (h : g =ᵐ[ν] g') (h2 : μ.map f ≪ ν) : g ∘ f =ᵐ[μ] g' ∘ f :=
diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean
@@ -256,7 +256,7 @@ theorem bernoulliPowerSeries_mul_exp_sub_one : bernoulliPowerSeries A * (exp A -
   · simp
   simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
     coeff_one, coeff_exp, LinearMap.map_sub, factorial, if_pos, cast_succ, cast_one, cast_mul,
-    sub_zero, RingHom.map_one, add_eq_zero_iff, if_false, _root_.inv_one, zero_add, one_ne_zero,
+    sub_zero, RingHom.map_one, add_eq_zero, if_false, _root_.inv_one, zero_add, one_ne_zero,
     mul_zero, and_false_iff, sub_self, ← RingHom.map_mul, ← map_sum]
   cases' n with n
   · simp
diff --git a/Mathlib/NumberTheory/Zsqrtd/Basic.lean b/Mathlib/NumberTheory/Zsqrtd/Basic.lean
diff --git a/Mathlib/RingTheory/Coprime/Basic.lean b/Mathlib/RingTheory/Coprime/Basic.lean
diff --git a/Mathlib/RingTheory/GradedAlgebra/Basic.lean b/Mathlib/RingTheory/GradedAlgebra/Basic.lean
diff --git a/Mathlib/RingTheory/PowerSeries/Order.lean b/Mathlib/RingTheory/PowerSeries/Order.lean
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean
diff --git a/Mathlib/SetTheory/Cardinal/Divisibility.lean b/Mathlib/SetTheory/Cardinal/Divisibility.lean
