diff --git a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
index eaab0810122e68..17452ef1441df0 100644
--- a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
+++ b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
@@ -371,7 +371,7 @@ def interUnionPullbackConeLift : s.pt ⟶ F.1.obj (op (U ⊔ V)) := by
 set_option backward.isDefEq.respectTransparency false in
 theorem interUnionPullbackConeLift_left :
     interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_left).op = s.fst := by
-  erw [Category.assoc]
+  rw [interUnionPullbackConeLift, Category.assoc]
   simp_rw [← F.1.map_comp]
   exact
     (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
@@ -380,7 +380,7 @@ theorem interUnionPullbackConeLift_left :
 set_option backward.isDefEq.respectTransparency false in
 theorem interUnionPullbackConeLift_right :
     interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_right).op = s.snd := by
-  erw [Category.assoc]
+  rw [interUnionPullbackConeLift, Category.assoc]
   simp_rw [← F.1.map_comp]
   exact
     (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
@@ -409,10 +409,10 @@ def isLimitPullbackCone : IsLimit (interUnionPullbackCone F U V) := by
     apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext
     rintro ((_ | _) | (_ | _)) <;>
     rw [Category.assoc, Category.assoc]
-    · erw [← F.1.map_comp]
+    · rw [Functor.mapCone_π_app, ← F.1.map_comp]
       convert h₁
       apply interUnionPullbackConeLift_left
-    · erw [← F.1.map_comp]
+    · rw [Functor.mapCone_π_app, ← F.1.map_comp]
       convert h₂
       apply interUnionPullbackConeLift_right
     all_goals