diff --git a/Mathlib/Tactic/CongrExclamation.lean b/Mathlib/Tactic/CongrExclamation.lean
index dbad9c4977c1c8..fdf409fcf2fed4 100644
--- a/Mathlib/Tactic/CongrExclamation.lean
+++ b/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`.
 
diff --git a/Mathlib/Tactic/Convert.lean b/Mathlib/Tactic/Convert.lean
index eb74ff924a4cec..7af3d0a8cb73da 100644
--- a/Mathlib/Tactic/Convert.lean
+++ b/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. -/
diff --git a/MathlibTest/Tactic/Convert/Basic.lean b/MathlibTest/Tactic/Convert/Basic.lean
index 6c41f450e271e8..a6ccf70ca7e7a3 100644
--- a/MathlibTest/Tactic/Convert/Basic.lean
+++ b/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