feat(Logic): declare optional simprocs for commuting equality and iff

Archive/Imo/Imo2024Q5.lean

@@ -938,8 +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
-        lia
+      · 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

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, eq_comm]
+  simp [range_eq_top, exact_iff, eqComm]
 
 end LinearMap
 

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 [Function.update_of_ne h.symm, h]
+  · simp [h, eqComm]
 
 @[to_additive]
 theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {M : Type*} [CommMonoid M]

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -307,8 +307,8 @@ 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. -/
-@[simp]
-theorem zero_eq_mul : 0 = a * b ↔ a = 0 ∨ b = 0 := by rw [eq_comm, mul_eq_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 [eqComm]
 
 /-- If `α` has no zero divisors, then the product of two elements is nonzero iff both of them
 are nonzero. -/
@@ -325,7 +325,7 @@ theorem mul_ne_zero_comm : a * b ≠ 0 ↔ b * a ≠ 0 := mul_eq_zero_comm.not
 
 theorem mul_self_eq_zero : a * a = 0 ↔ a = 0 := by simp
 
-theorem zero_eq_mul_self : 0 = a * a ↔ a = 0 := by simp
+theorem zero_eq_mul_self : 0 = a * a ↔ a = 0 := by simp [eq_comm]
 
 theorem mul_self_ne_zero : a * a ≠ 0 ↔ a ≠ 0 := mul_self_eq_zero.not
 

Mathlib/Algebra/MvPolynomial/Nilpotent.lean

@@ -72,7 +72,7 @@ theorem isUnit_iff : IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ i ≠ 0, IsNilpoten
     simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)
 
 instance : IsLocalHom (C : _ →+* MvPolynomial σ R) where
-  map_nonunit := by classical simp +contextual [isUnit_iff, coeff_C, apply_ite]
+  map_nonunit := by classical simp +contextual [isUnit_iff, coeff_C]
 
 instance : IsLocalHom (algebraMap R (MvPolynomial σ R)) :=
   inferInstanceAs (IsLocalHom C)

Mathlib/Algebra/Order/Antidiag/Finsupp.lean

@@ -56,7 +56,7 @@ lemma mem_finsuppAntidiag' :
   rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]
 
 @[simp] lemma finsuppAntidiag_empty_zero : finsuppAntidiag (∅ : Finset ι) (0 : μ) = {0} := by
-  ext f; simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]
+  ext f; simp
 
 @[simp] lemma finsuppAntidiag_empty_of_ne_zero (hn : n ≠ 0) :
     finsuppAntidiag (∅ : Finset ι) n = ∅ :=
@@ -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]
+  ext f; simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]
 
 end CanonicallyOrderedAddCommMonoid
 end Finset

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 simpa [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]
 

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 =>
-    simpa [cfcₙ_apply_of_not_map_zero _ hf₀] using Prod.mk_zero_zero.symm
+    simp [cfcₙ_apply_of_not_map_zero _ hf₀, eqComm]
 
 end nonunital_prod
 

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
@@ -41,8 +39,7 @@ theorem sameRay_iff : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg := b
   rcases eq_or_ne y 0 with (rfl | hy)
   · simp
   simp only [hx, hy, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
-  simp [field, hx]
-  rw [mul_comm, eq_comm]
+  simp [field, hx, mul_comm, eq_comm]
 
 theorem sameRay_iff_arg_div_eq_zero : SameRay ℝ x y ↔ arg (x / y) = 0 := by
   rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]

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

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]

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
 

Mathlib/CategoryTheory/Preadditive/Biproducts.lean

@@ -295,9 +295,8 @@ def biproduct.reindex {β γ : Type} [Finite β] (ε : β ≃ γ)
     cases nonempty_fintype β
     ext g g'
     by_cases h : g' = g <;>
-      simp [Preadditive.sum_comp, biproduct.lift_desc,
-        biproduct.ι_π, comp_dite, Equiv.apply_eq_iff_eq_symm_apply,
-        h]
+      simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
+        Equiv.apply_eq_iff_eq_symm_apply, h]
 
 /-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
 any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

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] using ENNReal.eq_sub_of_add_eq b_ne_top rfl
+  · 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

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)]
 

Mathlib/Data/Fin/Tuple/Sort.lean

@@ -63,11 +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
-    -- Porting note: was `simpa [graph] using h`
-    simp only [graph, Finset.mem_image, Finset.mem_univ, true_and] at h
-    obtain ⟨i', hi'⟩ := h
-    obtain ⟨-, rfl⟩ := Prod.mk_inj.mp hi'
-    simpa
+    simpa [graph, eq_comm, eqComm] using h
 
 @[simp]
 theorem proj_equiv₁' (f : Fin n → α) : graph.proj ∘ graphEquiv₁ f = f :=

Mathlib/Data/Matrix/Diagonal.lean

@@ -89,9 +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]
-  · simp [h, transpose, diagonal_apply_ne' _ h]
+  by_cases h : i = j <;> simp [h, transpose, eqComm]
 
 @[simp]
 theorem diagonal_add [AddZeroClass α] (d₁ d₂ : n → α) :

Mathlib/Data/Set/Prod.lean

@@ -963,7 +963,7 @@ lemma graphOn_comp (s : Set α) (f : α → β) (g : β → γ) :
 lemma graphOn_univ_eq_range : univ.graphOn f = range fun x ↦ (x, f x) := image_univ
 
 @[simp] lemma graphOn_inj {g : α → β} : s.graphOn f = s.graphOn g ↔ s.EqOn f g := by
-  simp [Set.ext_iff, forall_comm, EqOn]
+  simp [Set.ext_iff, forall_comm (α := β), EqOn]
 
 lemma graphOn_prod_graphOn (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
     s.graphOn f ×ˢ t.graphOn g = Equiv.prodProdProdComm .. ⁻¹' (s ×ˢ t).graphOn (Prod.map f g) := by

Mathlib/FieldTheory/Finite/Basic.lean

@@ -378,7 +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⟩
-      simpa [if_neg (Nat.one_lt_pow pos.ne' Fintype.one_lt_card).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]

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 [Multiset.count_singleton, ne, if_neg (Ne.symm _)]
+      simp [ne, eqComm]
     · intro h; exact (h <| Finset.mem_univ _).elim
   · rw [Multiset.count_singleton_self, mul_one]
 

Mathlib/FieldTheory/SeparablyGenerated.lean

@@ -87,7 +87,8 @@ include HF
 lemma irreducible_of_forall_totalDegree_le (hF0 : F ≠ 0) (hFa : F.aeval a = 0) : Irreducible F := by
   refine ⟨fun h' ↦ (h'.map (aeval a)).ne_zero hFa, fun q₁ q₂ e ↦ ?_⟩
   wlog h₁ : aeval a q₁ = 0 generalizing q₁ q₂
-  · exact .symm (this q₂ q₁ (e.trans (mul_comm ..)) <| by simpa [h₁, hFa] using congr(aeval a $e))
+  · exact .symm (this q₂ q₁ (e.trans (mul_comm ..)) <| by
+      simpa [h₁, hFa] using Eq.symm <| congr(aeval a $e))
   have ne := mul_ne_zero_iff.mp (e ▸ hF0)
   have := HF q₁ ne.1 h₁
   rw [e, totalDegree_mul_of_isDomain ne.1 ne.2, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -396,7 +396,7 @@ theorem isCycle_swap_mul_aux₂ {α : Type*} [DecidableEq α] :
       rw [mul_apply, swap_apply_def]
       split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at * <;> tauto
     obtain ⟨i, hi⟩ := isCycle_swap_mul_aux₁ n hb <| by
-      rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply] using h
+      rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply (x := x)] using h
     refine ⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩
     convert hi using 1
     · rw [zpow_neg, ← inv_zpow, ← mul_apply, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul]

Mathlib/Lean/Meta/Simp.lean

@@ -161,4 +161,30 @@ def getAllSimpAttrs (decl : Name) : CoreM (Array Name) := do
       simpAttrs := simpAttrs.push simpAttr
   return simpAttrs
 
+/-- Run `e` while the entries in `declNames` are erased from the `simp` set, while preserving the
+rest of the `simp` configuration.
+
+Performance note: the code in `e` will be run with a new cache (which is discarded at the end of the
+function). The original cache is restored when this function returns.
+-/
+meta def Simp.withoutTheorems {α} (declNames : Array Name) (e : SimpM α) : SimpM α := do
+  let mut theorems ← getSimpTheorems
+  let mut procs ← getSimprocs
+  for name in declNames do
+    -- Erase all variants of the theorem, not just the forward post-proc.
+    theorems := theorems
+      |>.eraseTheorem (.decl name)
+      |>.eraseTheorem (.decl name (inv := true))
+      |>.eraseTheorem (.decl name (post := false))
+      |>.eraseTheorem (.decl name (inv := true) (post := false))
+    procs := procs.erase name
+  let oldMethods ← getMethods
+  let methods := mkMethods #[procs] oldMethods.discharge? oldMethods.wellBehavedDischarge
+  -- Preserve the cache, otherwise a deleted theorem might continue firing,
+  -- or conversely a failure inside `e` could be propagated outside.
+  withPreservedCache <| withSimpTheorems theorems do
+    let (x, s) ← e.run (← getContext) (← get) methods
+    set s
+    return x
+
 end Lean.Meta

Mathlib/LinearAlgebra/Matrix/Permutation.lean

@@ -79,7 +79,7 @@ lemma permMatrix_mulVec {v : n → R} [CommRing R] :
 lemma vecMul_permMatrix {v : n → R} [CommRing R] :
     v ᵥ* σ.permMatrix R = v ∘ σ.symm := by
   ext j
-  simp [vecMul_eq_sum, Pi.single, Function.update, ← Equiv.symm_apply_eq]
+  simp [vecMul_eq_sum, Pi.single, Function.update, ← Equiv.symm_apply_eq σ]
 
 @[simp]
 lemma permMatrix_mul [NonAssocSemiring R] :
@@ -114,7 +114,7 @@ See `Matrix.permMatrix_l2_opNorm_le` for the inequality version of the empty cas
 theorem permMatrix_l2_opNorm_eq [Nonempty n] : ‖σ.permMatrix 𝕜‖ = 1 :=
   le_antisymm (permMatrix_l2_opNorm_le σ) <| by
     inhabit n
-    simpa [EuclideanSpace.norm_eq, permMatrix_mulVec, ← Equiv.eq_symm_apply, apply_ite] using
+    simpa [EuclideanSpace.norm_eq, permMatrix_mulVec, ← Equiv.eq_symm_apply σ, apply_ite] using
       (σ.permMatrix 𝕜).l2_opNorm_mulVec (WithLp.toLp _ (Pi.single default 1))
 
 end Matrix

Mathlib/LinearAlgebra/Matrix/Stochastic.lean

@@ -213,7 +213,7 @@ lemma permMatrix_mem_colStochastic {σ : Equiv.Perm n} :
   rw [mem_colStochastic_iff_sum]
   refine ⟨fun i j => ?g1, ?g2⟩
   case g1 => aesop
-  case g2 => simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply]
+  case g2 => simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply σ]
 
 /-- The transpose of a matrix is row stochastic matrix if it is column stochastic. -/
 @[grind =]

Mathlib/Logic/Basic.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 -/
 module
 
+public import Mathlib.Lean.Meta.Simp
 public import Mathlib.Tactic.AdaptationNote
 public import Batteries.Logic
 public import Batteries.Util.LibraryNote
@@ -28,6 +29,75 @@ open Function
 
 section Miscellany
 
+section CommSimproc
+
+open Lean Meta Simp
+
+theorem eq_comm_eq {α : Sort*} (a b : α) : (a = b) = (b = a) := by rw [@eq_comm _ a b]
+theorem iff_comm_eq (a b : Prop) : (a ↔ b) = (b ↔ a) := by rw [@iff_comm a b]
+
+/-- On a goal of the form of `x = y`, also try to simplify `y = x`.
+
+If simplifying `y = x` gives `y' = x'` then this simproc returns `x' = y'` (so that the use of
+commutativity is transparent), otherwise it returns the result of simplifying `y = x` unmodified.
+-/
+simproc_decl eqComm (_ = _) := fun e => do
+  let_expr Eq _ x y := e | return .continue
+  let symmExpr ← mkEq y x
+  let r ← withoutTheorems #[`eqComm,
+    -- These theorems would cause an infinite loop:
+    ``eq_comm, ``Bool.not_eq_eq_eq_not, `inv_eq_iff_eq_inv, `eq_inv_mul_iff_mul_eq,
+    `eq_mul_inv_iff_mul_eq, `neg_eq_iff_eq_neg, `Function.Involutive.eq_iff,
+    `vadd_eq_iff_eq_neg_vadd, `Equiv.apply_eq_iff_eq_symm_apply,
+    -- These theorems aren't commute-resistant (they turn an equality into a non-equality in a
+    -- non-commutative way.)
+    ``beq_iff_eq, ``funext_iff, ``eq_iff_iff, `Prod.swap_eq_iff_eq_swap, ``left_eq_dite_iff,
+    ``right_eq_dite_iff] do
+    withTraceNode `Meta.Tactic.simp (fun _ => return m!"commuting equality: {e}") <| simp symmExpr
+  -- If no actual progress happened (modulo commutativity), return early.
+  match_expr r.expr with
+  | Eq _ y' x' =>
+    if (y' == y && x' == x) || (y' == x && x' == y) then do
+      return .continue none
+  | _ => pure ()
+  let symmR ← Result.mkEqTrans { expr := symmExpr, proof? := ← mkAppM ``eq_comm_eq #[x, y] } r
+  -- If we started with `x = y`, and the result of simplifying `y = x` was `y' = x'`, then we want
+  -- to end up with `x' = y'`.
+  match_expr r.expr with
+  | Eq _ y' x' =>
+    return .visit (← symmR.mkEqTrans
+      { expr := ← mkEq x' y', proof? := ← mkAppM ``eq_comm_eq #[y', x'] })
+  | _ => return .done symmR
+
+/-- On a goal of the form of `x ↔ y`, also try to simplify `y ↔ x`.
+
+If simplifying `y ↔ x` gives `y' ↔ x'` then this simproc returns `x' ↔ y'` (so that the use of
+commutativity is transparent), otherwise it returns the result of simplifying `y ↔ x` unmodified.
+-/
+simproc_decl iffComm (_ ↔ _) := fun e => do
+  let_expr Iff x y := e | return .continue
+  let symmExpr := .app (.app (.const ``Iff []) y) x
+  let r ← withoutTheorems #[`iffComm,
+      -- These theorems would cause an infinite loop:
+      ``Iff.comm,
+      -- These theorems aren't commute-resistant (they turn an iff into a non-iff in a
+      -- non-commutative way).
+      ``and_congr_left_iff, ``and_congr_right_iff,  ``iff_def, ``iff_def',
+      ``iff_iff_implies_and_implies, ``Bool.coe_iff_coe] do
+    withTraceNode `Meta.Tactic.simp (fun _ => return m!"commuting iff: {e}") <| simp symmExpr
+  -- If no actual progress happened (modulo commutativity), return early.
+  if r.expr == symmExpr || r.expr == e then return .continue
+  let symmR ← Result.mkEqTrans { expr := symmExpr, proof? := ← mkAppM ``iff_comm_eq #[x, y] } r
+  -- If we started with `x ↔ y`, and the result of simplifying `y ↔ x` was `y' ↔ x'`, then we want
+  -- to end up with `x' ↔ y'`.
+  match_expr r.expr with
+  | Iff y' x' =>
+    return .visit (← symmR.mkEqTrans
+      { expr := .app (.app (.const ``Iff []) x') y', proof? := ← mkAppM ``iff_comm_eq #[y', x'] })
+  | _ => return .done symmR
+
+end CommSimproc
+
 -- attribute [refl] HEq.refl -- FIXME This is still rejected after https://github.com/leanprover-community/mathlib4/pull/857
 
 /-- An identity function with its main argument implicit. This will be printed as `hidden` even

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]
 
-@[simp] lemma eq_update_self_iff : f = update f a b ↔ f a = b := by simp [eq_update_iff]
+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
 

Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

@@ -191,7 +191,7 @@ theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0
     have hxp : x.1 < p := lt_of_le_of_lt (b := p / 2)
       (by grind) (Nat.div_lt_self hp.1.pos (by decide))
     have : (x.1 : ZMod p) = 0 := by
-      simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
+      simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hqp hpq)
     apply_fun ZMod.val at this
     rw [val_cast_of_lt hxp, val_zero] at this
     simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] at hx