From dd8c65e3abbac7e13030d9494f6779a6d456fce9 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 7 Nov 2024 10:34:21 +0100
Subject: [PATCH] Less invasive changes to mkCongrSimp?

---
 src/Lean/Meta/Tactic/Simp/Types.lean | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index d2c16eb6279f..add598d2af60 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -475,7 +475,7 @@ def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
     let mut r := r
     let mut i := 0
     for arg in args do
-      if isIte && !cfg.underLambda && i > 2 then
+      if isIte && !cfg.underLambda && (i == 3 || i == 4) then
         -- Do not traverse then/else arguments when underLambda := false
         r ← mkCongrFun r arg
       else if h : i < infos.size then
@@ -509,10 +509,7 @@ using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a
 -/
 def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
   if f.isConst then
-    let n := f.constName!
-    -- We always use simple congruence theorems for auxiliary match applications
-    -- (and the match-like ite and dite)
-    if n = ``ite || n = ``dite || (← isMatcher n) then
+    if (← isMatcher f.constName!) then
       return none
   let info ← getFunInfo f
   let kinds ← getCongrSimpKinds f info
@@ -531,6 +528,7 @@ Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
 -/
 def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   let f := e.getAppFn
+  let isIte := f.isConstOf ``ite
   -- TODO: cache
   let some cgrThm ← mkCongrSimp? f | return none
   if cgrThm.argKinds.size != e.getAppNumArgs then return none
@@ -551,6 +549,11 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
         argsNew := argsNew.push arg
         i := i + 1
         continue
+    if !config.underLambda && isIte && (i = 3 || i = 4) then
+        -- Do not visit arms of an ite when `underLambda := false`
+        argsNew := argsNew.push arg
+        i := i + 1
+        continue
     match kind with
     | CongrArgKind.fixed =>
       let argNew ← dsimp arg