diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
index ea97fa57864dd..f6d6816a75d61 100644
--- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
+++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
@@ -394,7 +394,7 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v}
     refine' (F.obj (unop X)).presheaf.mapIso (eqToIso _)
     simp only [Functor.op_obj, unop_op, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
       Set.preimage_preimage]
-    refine congr_arg (Set.preimage . U.1) (funext fun x => ?_)
+    refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
     erw [← TopCat.comp_app]
     congr
     exact ι_preservesColimitsIso_inv (forget C) F (unop X)
diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean
index 1e8e851e63c1d..819ecf6d7655e 100644
--- a/Mathlib/RingTheory/Ideal/Over.lean
+++ b/Mathlib/RingTheory/Ideal/Over.lean
@@ -396,7 +396,7 @@ theorem exists_ideal_over_prime_of_isIntegral_of_isPrime
   refine' _root_.trans _ (_root_.trans (congr_arg (comap (Ideal.Quotient.mk
     (comap (algebraMap R S) I))) hQ') _)
   · rw [comap_comap]
-    exact congr_arg (comap . Q') (RingHom.ext fun r => rfl)
+    exact congr_arg (comap · Q') (RingHom.ext fun r => rfl)
   · refine' _root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 _)
     simpa [← RingHom.ker_eq_comap_bot] using hIP