From 86fc089e07c58d14c5178cd8e40725518b2ae98e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Mar 2022 14:04:28 -0700 Subject: [PATCH] fix: `tryAutoCongrTheorem?` may still use `dsimp` for fixed arguments Reviewed-by: Leonardo de Moura --- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index bfcf686861..93bef111cf 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -317,7 +317,7 @@ where let args := e.getAppArgs for arg in args, kind in cgrThm.argKinds do match kind with - | CongrArgKind.fixed => argsNew := argsNew.push arg + | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg) | CongrArgKind.cast => hasCast := true; argsNew := argsNew.push arg | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg | CongrArgKind.eq =>