fix: missing dsimp simplification when applying auto-congr theorems

closes #4339

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -522,7 +522,11 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
         i := i + 1
         continue
     match kind with
-    | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg)
+    | CongrArgKind.fixed =>
+      let argNew ← dsimp arg
+      if arg != argNew then
+        simplified := true
+      argsNew := argsNew.push argNew
     | CongrArgKind.cast  => hasCast := true; argsNew := argsNew.push arg
     | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg
     | CongrArgKind.eq =>
@@ -558,19 +562,26 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
     equal using `TransparencyMode.reducible` (`Nat.pred` is not reducible).
     Thus, we decided to return here only if the auto generated congruence theorem does not introduce casts.
   -/
-  if !hasProof && !hasCast then return some { expr := mkAppN f argsNew }
+  if !hasProof && !hasCast then
+    return some { expr := mkAppN f argsNew }
   let mut proof := cgrThm.proof
   let mut type  := cgrThm.type
   let mut j := 0 -- index at argResults
   let mut subst := #[]
-  for arg in args, kind in cgrThm.argKinds do
+  for arg in args, argNew in argsNew, kind in cgrThm.argKinds do
     proof := mkApp proof arg
-    subst := subst.push arg
     type := type.bindingBody!
     match kind with
-    | CongrArgKind.fixed => pure ()
-    | CongrArgKind.cast  => pure ()
+    | CongrArgKind.fixed =>
+      /-
+      We use `argNew` here because `dsimp` may have simplified the fixed argument.
+      See issue #4339
+      -/
+      subst := subst.push argNew
+    | CongrArgKind.cast  =>
+      subst := subst.push arg
     | CongrArgKind.subsingletonInst =>
+      subst := subst.push arg
       let clsNew := type.bindingDomain!.instantiateRev subst
       let instNew ← if (← isDefEq (← inferType arg) clsNew) then
         pure arg
@@ -584,6 +595,7 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
       subst := subst.push instNew
       type := type.bindingBody!
     | CongrArgKind.eq =>
+      subst := subst.push arg
       let argResult := argResults[j]!
       let argProof ← argResult.getProof' arg
       j := j + 1

tests/lean/run/4339.lean

@@ -0,0 +1,40 @@
+def mid {α} (T : α) := T
+
+structure HH (A B : Nat) where
+  toFun : Nat
+  prop : True
+
+set_option pp.explicit true
+
+/--
+info: S T f : Nat
+⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial))
+-/
+#guard_msgs in
+example {S T : Nat} (f : Nat) :
+  HH.mk (B := T) f trivial = id (α := HH S T) (HH.mk (B := mid T) f trivial) := by
+  simp only [mid]
+  trace_state
+  rfl
+
+/--
+info: S T f : Nat
+⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial))
+-/
+#guard_msgs in
+example {S T : Nat} (f : Nat) :
+  HH.mk (B := T) f trivial = id (α := HH S T) (HH.mk (B := mid T) f trivial) := by
+  dsimp only [mid]
+  trace_state
+  rfl
+
+/--
+info: S T f : Nat
+⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial))
+-/
+#guard_msgs in
+example {S T : Nat} (f : Nat) :
+  HH.mk (B := T) f trivial = id (α := HH S T) (HH.mk (B := mid T) f trivial) := by
+  unfold mid
+  trace_state
+  rfl