From 72f8cd4d03d88b0b17b7033373f0396cb042ffe9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Sat, 23 May 2026 21:52:26 +0200
Subject: [PATCH] chore: use `skip` instead of `-failIfUnchanged` in the
 default tactic of `Homeomorph`

---
 Mathlib/Topology/Homeomorph/Defs.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Homeomorph/Defs.lean b/Mathlib/Topology/Homeomorph/Defs.lean
index bc16027728b168..b447ded44f1fe1 100644
--- a/Mathlib/Topology/Homeomorph/Defs.lean
+++ b/Mathlib/Topology/Homeomorph/Defs.lean
@@ -44,10 +44,10 @@ structure Homeomorph (X : Type*) (Y : Type*) [TopologicalSpace X] [TopologicalSp
     extends X ≃ Y where
   /-- The forward map of a homeomorphism is a continuous function. -/
   continuous_toFun : Continuous toFun := by
-    first | fun_prop | eta_expand; dsimp -failIfUnchanged; fun_prop
+    first | fun_prop | eta_expand; dsimp; fun_prop | skip
   /-- The inverse map of a homeomorphism is a continuous function. -/
   continuous_invFun : Continuous invFun := by
-    first | fun_prop | eta_expand; dsimp -failIfUnchanged; fun_prop
+    first | fun_prop | eta_expand; dsimp; fun_prop | skip
 
 @[inherit_doc]
 infixl:25 " ≃ₜ " => Homeomorph