Skip to content

Commit 8837bbe

Browse files
gasparattilab-mehta
authored andcommitted
chore: use skip instead of -failIfUnchanged in the default tactic of Homeomorph (leanprover-community#39758)
This way, we do not try to call `fun_prop` again when `dsimp` could not make any simplification. This makes a difference only when the default tactic fails, so this change should not affect working code.
1 parent af27b81 commit 8837bbe

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/Topology/Homeomorph/Defs.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,10 +44,10 @@ structure Homeomorph (X : Type*) (Y : Type*) [TopologicalSpace X] [TopologicalSp
4444
extends X ≃ Y where
4545
/-- The forward map of a homeomorphism is a continuous function. -/
4646
continuous_toFun : Continuous toFun := by
47-
first | fun_prop | eta_expand; dsimp -failIfUnchanged; fun_prop
47+
first | fun_prop | eta_expand; dsimp; fun_prop | skip
4848
/-- The inverse map of a homeomorphism is a continuous function. -/
4949
continuous_invFun : Continuous invFun := by
50-
first | fun_prop | eta_expand; dsimp -failIfUnchanged; fun_prop
50+
first | fun_prop | eta_expand; dsimp; fun_prop | skip
5151

5252
@[inherit_doc]
5353
infixl:25 " ≃ₜ " => Homeomorph

0 commit comments

Comments
 (0)