From a9bb646d4fea81ea59241abe2e15e3e586b514dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Feb 2022 17:35:07 -0800
Subject: [PATCH] chore: cleanup

---
 src/Lean/Meta/Tactic/Simp/Main.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 26b2342ce0..305a40f7c7 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -284,6 +284,9 @@ where
       return { expr := eNew, proof? := proof }
 
   mkCongrSimp? (f : Expr) : M (Option CongrTheorem) := do
+    if f.isConst then if (← isMatcher f.constName!) then
+      -- We always use simple congruence theorems for auxiliary match applications
+      return none
     let info ← getFunInfo f
     let kinds := getCongrSimpKinds info
     if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
@@ -299,7 +302,6 @@ where
 
   /-- Try to use automatically generated congruence theorems. See `mkCongrSimp?`. -/
   tryAutoCongrTheorem? (e : Expr) : M (Option Result) := do
-    if (← isMatcherApp e) then return none
     let f := e.getAppFn
     -- TODO: cache
     let some cgrThm ← mkCongrSimp? f | return none