fix(Tactic/Convert): support over-applications again (#40740)

This PR fixes a regression introduced in #38071, which had caused the congruence algorithm of `convert` to not support over-applications.

I added a test to show this now works again.

Author: JovanGerb

Mathlib/Tactic/CongrExclamation.lean

@@ -130,7 +130,7 @@ structure Congr!.Config where
   This can be used to control which side's definitions are expanded when applying the
   congruence lemma (if `preferLHS = true` then the RHS can be expanded). -/
   preferLHS : Bool := true
-  /-- Allow both sides to be partial applications.
+  /-- Allow both sides to be partial applications, and allow overapplications.
   When false, given an equality `f a b = g x y z` this means we never consider
   proving `f a = g x y`.
 

Mathlib/Tactic/Convert.lean

@@ -77,7 +77,6 @@ between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags
 -/
 structure Convert.CheapConfig extends Congr!.Config where
   postTransparency := .reducible
-  partialApp := false
   sameFun := true
 
 /-- Internal elaborator for `Convert.CheapConfig`: use `Convert.elabConfig` instead. -/

MathlibTest/Tactic/Convert/Basic.lean

@@ -2,6 +2,7 @@ module
 import Mathlib.Tactic.Convert
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Data.Set.Image
+import Mathlib.Algebra.Notation.Pi.Defs
 
 private axiom test_sorry : ∀ {α}, α
 set_option autoImplicit true
@@ -153,4 +154,10 @@ example (P : ℕ → Prop) {a b : ℕ} (hab : b = a) (h : P a) : P (semireducibl
 example (P : ℕ → Prop) {a b : ℕ} (hab : b = a) (h : P (semireducibleId a)) : P b := by
   convert! h
 
+-- Test that overapplications are supported
+example (f g h k : Nat → Nat) (H : (f + g) 1 = 0) : (h + k) 1 = 0 := by
+  convert H
+  guard_target =ₛ h = f
+  all_goals exact test_sorry
+
 end Tests