diff --git a/Mathlib/AlgebraicGeometry/AffineSpace.lean b/Mathlib/AlgebraicGeometry/AffineSpace.lean
index 805e43c4928d2..7751d57d64eda 100644
--- 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
index 08a4f0b16172f..a049787977d46 100644
--- 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)