chore: turn erw into rw for free (#19689)

The `erw` linter from #17638 caught these `erw`s that can become `rw` without breaking the proofs.
leanprover-community · Dec 2, 2024 · de7196a · de7196a
1 parent ceca167
commit de7196a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/AlgebraicGeometry/AffineSpace.lean b/Mathlib/AlgebraicGeometry/AffineSpace.lean
@@ -297,7 +297,7 @@ lemma map_comp {S S' S'' : Scheme} (f : S ⟶ S') (g : S' ⟶ S'') :
   · simp
   · simp only [TopologicalSpace.Opens.map_top, Scheme.comp_coeBase,
       TopologicalSpace.Opens.map_comp_obj, Scheme.comp_app, CommRingCat.comp_apply]
-    erw [map_appTop_coord, map_appTop_coord, map_appTop_coord]
+    rw [map_appTop_coord, map_appTop_coord, map_appTop_coord]
 
 lemma map_Spec_map {R S : CommRingCat.{max u v}} (φ : R ⟶ S) :
     map n (Spec.map φ) =

diff --git a/Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean b/Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@@ -554,8 +554,8 @@ lemma moebius_inversion_top (f g : α → 𝕜) (h : ∀ x, g x = ∑ y ∈ Ici
       rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
     _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
     _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
-      erw [sum_sigma' (Ici x) fun y ↦ Ici y]
-      erw [sum_sigma' (Ici x) fun z ↦ Icc x z]
+      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
+      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
       simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]
       apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
         aesop (add simp mul_assoc) (add unsafe le_trans)