Explicitly invoke eqComm for proofs

Vierkantor · Vierkantor · commit 884f5d61fb03 · 2026-04-14T15:53:47.000+02:00
diff --git a/Archive/Examples/IfNormalization/WithoutAesop.lean b/Archive/Examples/IfNormalization/WithoutAesop.lean
@@ -92,8 +92,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
           have := he₃ v
           simp_all? says
             simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true,
-              Bool.false_eq, Bool.true_eq, AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert,
-              reduceCtorEq, imp_false]
+              AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert, reduceCtorEq, imp_false]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
@@ -105,8 +104,8 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
           · subst h; simp_all
           · simp_all? says
               simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true,
-                Bool.false_eq, Bool.true_eq, AList.lookup_insert_eq_none, ne_eq, not_false_eq_true,
-                AList.lookup_insert_ne, implies_true]
+                AList.lookup_insert_eq_none, ne_eq, not_false_eq_true, AList.lookup_insert_ne,
+                implies_true]
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all
diff --git a/Archive/Imo/Imo2024Q5.lean b/Archive/Imo/Imo2024Q5.lean
@@ -938,7 +938,7 @@ lemma winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero (hN : 2
         lia
       · simp at hm
         exact m.notMem_monsterCells_of_fst_eq_zero rfl hm
-      · simp at h
+      · simp [eqComm] at h
       · dsimp only [Nat.reduceAdd, Nat.reduceDiv, Fin.mk_one] at hm
         have h1N : 1 ≤ N := by lia
         rw [m.mk_mem_monsterCells_iff_of_le (le_refl _) h1N] at hm
diff --git a/Mathlib/Algebra/CharP/Defs.lean b/Mathlib/Algebra/CharP/Defs.lean
@@ -68,7 +68,7 @@ lemma cast_eq_mod (k : ℕ) : (k : R) = (k % p : ℕ) :=
 
 lemma cast_eq_iff_mod_eq [IsLeftCancelAdd R] : (a : R) = (b : R) ↔ a % p = b % p := by
   wlog! hle : a ≤ b
-  · simpa [eq_comm] using (this _ _ hle.le)
+  · simpa only [eq_comm] using (this _ _ hle.le)
   obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le hle
   rw [Nat.cast_add, left_eq_add, CharP.cast_eq_zero_iff R p]
   constructor
diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean
@@ -289,7 +289,7 @@ lemma exact_zero_iff_surjective {M N : Type*} (P : Type*)
     [AddCommGroup M] [AddCommGroup N] [AddCommMonoid P] [Module R N] [Module R M]
     [Module R P] (f : M →ₗ[R] N) :
     Function.Exact f (0 : N →ₗ[R] P) ↔ Function.Surjective f := by
-  simp [range_eq_top, exact_iff]
+  simp [range_eq_top, exact_iff, eqComm]
 
 end LinearMap
 
diff --git a/Mathlib/Algebra/Group/Pi/Lemmas.lean b/Mathlib/Algebra/Group/Pi/Lemmas.lean
@@ -300,7 +300,7 @@ theorem Pi.update_eq_div_mul_mulSingle [∀ i, Group <| f i] (g : ∀ i : I, f i
   ext j
   rcases eq_or_ne i j with (rfl | h)
   · simp
-  · simp [h]
+  · simp [h, eqComm]
 
 @[to_additive]
 theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {M : Type*} [CommMonoid M]
diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -308,7 +308,7 @@ theorem mul_eq_zero : a * b = 0 ↔ a = 0 ∨ b = 0 :=
 /-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
 equals zero. -/
 -- This is not marked `@[simp]` since `simp` can derive this from `mul_eq_zero`.
-theorem zero_eq_mul : 0 = a * b ↔ a = 0 ∨ b = 0 := by simp
+theorem zero_eq_mul : 0 = a * b ↔ a = 0 ∨ b = 0 := by simp [eqComm]
 
 /-- If `α` has no zero divisors, then the product of two elements is nonzero iff both of them
 are nonzero. -/
diff --git a/Mathlib/Algebra/Order/Antidiag/Finsupp.lean b/Mathlib/Algebra/Order/Antidiag/Finsupp.lean
@@ -153,7 +153,7 @@ variable [DecidableEq ι] [DecidableEq μ] [AddCommMonoid μ] [PartialOrder μ]
   [CanonicallyOrderedAdd μ] [HasAntidiagonal μ]
 
 @[simp] lemma finsuppAntidiag_zero (s : Finset ι) : finsuppAntidiag s (0 : μ) = {0} := by
-  ext f; simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), -mem_piAntidiag, eq_comm, -eqComm]
+  ext f; simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]
 
 end CanonicallyOrderedAddCommMonoid
 end Finset
diff --git a/Mathlib/Algebra/Polynomial/Monic.lean b/Mathlib/Algebra/Polynomial/Monic.lean
@@ -503,7 +503,7 @@ theorem Monic.mul_right_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q
 theorem Monic.mul_natDegree_lt_iff (h : Monic p) {q : R[X]} :
     (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0 := by
   by_cases hq : q = 0
-  · suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simp [hq, ← h.natDegree_eq_zero]
+  · suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simp [hq, ← h.natDegree_eq_zero, iffComm]
     exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
   · simp [h.natDegree_mul', hq]
 
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean
@@ -83,7 +83,7 @@ lemma cfcₙ_map_prod (f : R → R) (a : A) (b : B)
       let φ := NonUnitalStarAlgHom.snd S A B
       exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb
   case neg =>
-    simp [cfcₙ_apply_of_not_map_zero _ hf₀]
+    simp [cfcₙ_apply_of_not_map_zero _ hf₀, eqComm]
 
 end nonunital_prod
 
diff --git a/Mathlib/Analysis/Complex/Arg.lean b/Mathlib/Analysis/Complex/Arg.lean
@@ -31,8 +31,6 @@ variable {x y : ℂ}
 namespace Complex
 
 set_option backward.isDefEq.respectTransparency false in
--- Non-terminal simp, used to be field_simp
-set_option linter.flexible false in
 -- see https://github.com/leanprover-community/mathlib4/issues/29041
 set_option linter.unusedSimpArgs false in
 theorem sameRay_iff : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg := by
diff --git a/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean b/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
@@ -221,7 +221,7 @@ theorem norm_image_sub_le_of_bound' [DecidableEq ι] (f : MultilinearMap 𝕜 E
         have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
           s.piecewise_insert _ _ _
         have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
-          simp [his]
+          simp [his, eqComm]
         rw [B, A, ← f.map_update_sub]
         apply le_trans (H _)
         gcongr with j
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@@ -432,7 +432,7 @@ theorem arg_neg_eq_arg_add_pi_iff {x : ℂ} :
   · rw [(ext rfl hi : x = x.re)]
     rcases lt_trichotomy x.re 0 with (hr | hr | hr)
     · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
-      simp [hr.not_gt, ← two_mul, Real.pi_ne_zero]
+      simp [hr.not_gt, ← two_mul, Real.pi_ne_zero, eqComm]
     · simp [hr, Real.pi_ne_zero.symm]
     · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
       simp [hr]
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@@ -473,7 +473,7 @@ theorem rpow_neg_one (x : ℝ) : x ^ (-1 : ℝ) = x⁻¹ := by
 -- TODO: fix non-terminal simp (acting on three goals, with different simp sets, leaving two)
 set_option linter.flexible false in
 theorem mul_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) : (x * y) ^ z = x ^ z * y ^ z := by
-  iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
+  iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all [eqComm]
   · rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]
   all_goals positivity
 
diff --git a/Mathlib/Computability/ContextFreeGrammar.lean b/Mathlib/Computability/ContextFreeGrammar.lean
@@ -301,14 +301,14 @@ lemma reverse_surjective : Surjective (reverse : ContextFreeGrammar T → Contex
 set_option backward.isDefEq.respectTransparency false in
 lemma produces_reverse : g.reverse.Produces u.reverse v.reverse ↔ g.Produces u v :=
   (Equiv.ofBijective _ ContextFreeRule.reverse_bijective).exists_congr
-    (by simp [ContextFreeRule.reverse_involutive.eq_iff, -eqComm])
+    (by simp [ContextFreeRule.reverse_involutive.eq_iff])
 
 alias ⟨_, Produces.reverse⟩ := produces_reverse
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma produces_reverse_comm : g.reverse.Produces u v ↔ g.Produces u.reverse v.reverse :=
   (Equiv.ofBijective _ ContextFreeRule.reverse_bijective).exists_congr
-    (by simp [ContextFreeRule.reverse_involutive.eq_iff, -eqComm])
+    (by simp [ContextFreeRule.reverse_involutive.eq_iff])
 
 protected lemma Derives.reverse (hg : g.Derives u v) : g.reverse.Derives u.reverse v.reverse := by
   induction hg with
diff --git a/Mathlib/Data/ENNReal/Operations.lean b/Mathlib/Data/ENNReal/Operations.lean
@@ -352,7 +352,7 @@ protected theorem add_sub_cancel_right (hb : b ≠ ∞) : a + b - b = a := by
 protected theorem sub_add_eq_add_sub (hab : b ≤ a) (b_ne_top : b ≠ ∞) :
     a - b + c = a + c - b := by
   by_cases c_top : c = ∞
-  · simpa [c_top]
+  · simpa [c_top, eqComm]
   refine ENNReal.eq_sub_of_add_eq b_ne_top ?_
   simp only [add_assoc, add_comm c b]
   simpa only [← add_assoc] using (add_left_inj c_top).mpr <| tsub_add_cancel_of_le hab
diff --git a/Mathlib/Data/EReal/Operations.lean b/Mathlib/Data/EReal/Operations.lean
@@ -764,7 +764,7 @@ lemma toENNReal_mul {x y : EReal} (hx : 0 ≤ x) :
     · simp_all [mul_top_of_pos hx]
   · rename_i a
     rcases lt_trichotomy a 0 with (ha | ha | ha)
-    · simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]
+    · simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha), eqComm]
     · simp [ha]
     · simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]
 
diff --git a/Mathlib/Data/Fin/Tuple/Sort.lean b/Mathlib/Data/Fin/Tuple/Sort.lean
@@ -63,7 +63,7 @@ def graphEquiv₁ (f : Fin n → α) : Fin n ≃ graph f where
   invFun p := p.1.2
   left_inv i := by simp
   right_inv := fun ⟨⟨x, i⟩, h⟩ => by
-    simpa [graph, eq_comm] using h
+    simpa [graph, eq_comm, eqComm] using h
 
 @[simp]
 theorem proj_equiv₁' (f : Fin n → α) : graph.proj ∘ graphEquiv₁ f = f :=
diff --git a/Mathlib/Data/Matrix/Diagonal.lean b/Mathlib/Data/Matrix/Diagonal.lean
@@ -89,7 +89,7 @@ theorem diagonal_eq_zero [Zero α] {d : n → α} : diagonal d = 0 ↔ d = 0 :=
 @[simp]
 theorem diagonal_transpose [Zero α] (v : n → α) : (diagonal v)ᵀ = diagonal v := by
   ext i j
-  by_cases h : i = j <;> simp [h, transpose]
+  by_cases h : i = j <;> simp [h, transpose, eqComm]
 
 @[simp]
 theorem diagonal_add [AddZeroClass α] (d₁ d₂ : n → α) :
diff --git a/Mathlib/Data/Set/Pairwise/Lattice.lean b/Mathlib/Data/Set/Pairwise/Lattice.lean
@@ -171,15 +171,7 @@ lemma Set.pairwiseDisjoint_pair_insert {s : Set α} {a : α} (ha : a ∉ s) :
   rw [pairwiseDisjoint_iff]
   rintro i hi j hj
   have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)
-  -- FIXME: was `aesop`
-  unfold Set.Nonempty
-  simp only [mem_inter_iff, mem_insert_iff, mem_singleton_iff, exists_eq_or_imp, ↓existsAndEq,
-    true_and]
-  rintro ((h | rfl) | (rfl | h))
-  · assumption
-  · simp at this; simp [this]
-  · simp at this; simp [this]
-  · exact this h
+  aesop (add simp [Set.Nonempty, Set.subset_def])
 
 theorem Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion (h₀ : (s ∪ t).PairwiseDisjoint f)
     (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t := by
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -378,8 +378,7 @@ theorem orderOf_frobeniusAlgHom : orderOf (frobeniusAlgHom K L) = Module.finrank
       have := DFunLike.congr_fun eq x
       rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← sub_eq_zero] at this
       refine ⟨fun h ↦ ?_, this⟩
-      have := congr_arg (coeff · 1) h
-      simpa [Fintype.one_lt_card.ne, pos.ne] using congr_arg (coeff · 1) h
+      simpa [Fintype.one_lt_card.ne, pos.ne, eqComm] using congr_arg (coeff · 1) h
     refine this.not_gt (((natDegree_sub_le ..).trans_eq ?_).trans_lt <|
       (Nat.pow_lt_pow_right Fintype.one_lt_card lt).trans_eq Module.card_eq_pow_finrank.symm)
     simp [Nat.one_le_pow _ _ Fintype.card_pos]
diff --git a/Mathlib/FieldTheory/Finite/Polynomial.lean b/Mathlib/FieldTheory/Finite/Polynomial.lean
@@ -94,7 +94,7 @@ theorem indicator_mem_restrictDegree (c : σ → K) :
   trans
   · refine Finset.sum_eq_single n ?_ ?_
     · intro b _ ne
-      simp [ne]
+      simp [ne, eqComm]
     · intro h; exact (h <| Finset.mem_univ _).elim
   · rw [Multiset.count_singleton_self, mul_one]
 
diff --git a/Mathlib/Geometry/Euclidean/Angle/Bisector.lean b/Mathlib/Geometry/Euclidean/Angle/Bisector.lean
@@ -303,7 +303,7 @@ lemma two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq {p p₁ p₂ p₃
       convert ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_
       · simp
         grind
-      · simpa using Eq.symm <| Fact.out
+      · simpa using Fact.out
     have hp : orthogonalProjection (line[ℝ, p₁, p₂]) p = p₁ := by
       suffices (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈ affineSpan ℝ {p₁} by
         simpa using this
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
@@ -573,7 +573,7 @@ theorem eq_update_iff {a : α} {b : β a} {f g : ∀ a, β a} :
 
 @[simp] lemma update_eq_self_iff : update f a b = f ↔ b = f a := by simp [update_eq_iff]
 
-lemma eq_update_self_iff : f = update f a b ↔ f a = b := by simp
+lemma eq_update_self_iff : f = update f a b ↔ f a = b := by simp [eqComm]
 
 lemma ne_update_self_iff : f ≠ update f a b ↔ f a ≠ b := eq_update_self_iff.not
 
diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean
@@ -235,7 +235,7 @@ lemma zmodRepr_natCast_zmodRepr (x : ℤ_[p]) :
 lemma norm_natCast_zmodRepr_eq_iff {x : ℤ_[p]} :
     ‖(x.zmodRepr : ℤ_[p])‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0 := by
   rcases norm_natCast_zmodRepr_eq x with h | h
-  · simp_all [eq_comm, -eqComm]
+  · simp_all [eq_comm]
   · rw [eq_comm, h]
     simp [← norm_natCast_zmodRepr_eq_one_iff, h]
 
diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean
@@ -759,7 +759,7 @@ theorem aleph_one_eq_lift : ℵ₁ = lift.{v} c ↔ ℵ₁ = c := by
 
 @[simp]
 theorem lift_eq_aleph_one : lift.{v} c = ℵ₁ ↔ c = ℵ₁ := by
-  simp
+  simp [eqComm]
 
 @[deprecated (since := "2025-12-22")] alias lift_eq_aleph1 := lift_eq_aleph_one
 
@@ -785,7 +785,7 @@ theorem aleph_natCast_eq_lift : ℵ_ n = lift.{v} c ↔ ℵ_ n = c := by
 
 @[simp]
 theorem lift_eq_aleph_natCast : lift.{v} c = ℵ_ n ↔ c = ℵ_ n := by
-  simp
+  simp [eqComm]
 
 @[simp]
 theorem aleph_ofNat_le_lift [n.AtLeastTwo] : ℵ_ ofNat(n) ≤ lift.{v} c ↔ ℵ_ ofNat(n) ≤ c :=
@@ -833,7 +833,7 @@ theorem beth_natCast_eq_lift : ℶ_ n = lift.{v} c ↔ ℶ_ n = c := by
 
 @[simp]
 theorem lift_eq_beth_natCast : lift.{v} c = ℶ_ n ↔ c = ℶ_ n := by
-  simp
+  simp [eqComm]
 
 @[simp]
 theorem beth_ofNat_le_lift [n.AtLeastTwo] : ℶ_ ofNat(n) ≤ lift.{v} c ↔ ℶ_ ofNat(n) ≤ c :=
@@ -888,7 +888,7 @@ theorem omega_one_eq_lift : ω₁ = lift.{v} o ↔ ω₁ = o := by
 
 @[simp]
 theorem lift_eq_omega_one : lift.{v} o = ω₁ ↔ o = ω₁ := by
-  simp
+  simp [eqComm]
 
 @[simp]
 theorem omega_natCast_le_lift : ω_ n ≤ lift.{v} o ↔ ω_ n ≤ o := by
@@ -912,7 +912,7 @@ theorem omega_natCast_eq_lift : ω_ n = lift.{v} o ↔ ω_ n = o := by
 
 @[simp]
 theorem lift_eq_omega_natCast : lift.{v} o = ω_ n ↔ o = ω_ n := by
-  simp
+  simp [eqComm]
 
 @[simp]
 theorem omega_ofNat_le_lift [n.AtLeastTwo] : ω_ ofNat(n) ≤ lift.{v} o ↔ ω_ ofNat(n) ≤ o :=
diff --git a/Mathlib/SetTheory/Cardinal/Order.lean b/Mathlib/SetTheory/Cardinal/Order.lean
@@ -607,7 +607,7 @@ theorem aleph0_eq_lift {c : Cardinal.{u}} : ℵ₀ = lift.{v} c ↔ ℵ₀ = c :
 
 @[simp]
 theorem lift_eq_aleph0 {c : Cardinal.{u}} : lift.{v} c = ℵ₀ ↔ c = ℵ₀ := by
-  simp
+  simp [eqComm]
 
 /-! ### Properties about the cast from `ℕ` -/
 
@@ -638,12 +638,12 @@ theorem nat_eq_lift_iff {n : ℕ} {a : Cardinal.{u}} :
 @[simp]
 theorem zero_eq_lift_iff {a : Cardinal.{u}} :
     (0 : Cardinal) = lift.{v} a ↔ 0 = a := by
-  simp
+  simp [eqComm]
 
 @[simp]
 theorem one_eq_lift_iff {a : Cardinal.{u}} :
     (1 : Cardinal) = lift.{v} a ↔ 1 = a := by
-  simp
+  simp [eqComm]
 
 @[simp]
 theorem ofNat_eq_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean
@@ -881,7 +881,7 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o
   · rcases m with - | m
     · by_cases h : o₂ = 0
       · simp [opow_def, opowAux2, e₁, h, r₁]
-      · simpa [opow_def, opowAux2, e₁, h, r₁] using mt repr_inj.1 h
+      · simpa [opow_def, opowAux2, e₁, h, r₁, eqComm] using mt repr_inj.1 h
     · rcases e₂ : split' o₂ with ⟨b', k⟩
       obtain ⟨_, r₂⟩ := nf_repr_split' e₂
       by_cases h : m = 0
