diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index 2b5f0f2b2ff385..510a81a1a090d1 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -460,6 +460,9 @@ where
     return e
   visitApp (e : Expr) := e.withApp fun f args ↦ do
     let env ← getEnv
+    if f.isLambda && !args.isEmpty then
+      if ← isProof f then
+        return ← visit (f.beta args)
     match f with
     | .proj n i b =>
       let some info := getStructureInfo? env n |
diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean
index 0b7f15495acb17..b9bb47f4ad4a2b 100644
--- a/MathlibTest/ToDual.lean
+++ b/MathlibTest/ToDual.lean
@@ -382,3 +382,8 @@ info: eq_of_max_of_min {α : Type} [PartialOrder α] (a b : α) (hmin : ∀ (x :
 -/
 #guard_msgs in
 #check eq_of_max_of_min
+
+-- Test that the heuristic applies even when proofs are beta expanded
+@[to_dual (dont_translate := β) le_of_lt_and_le_of_lt']
+theorem le_of_lt_and_le_of_lt {β} [Preorder β] (a b : α) (c d : β) : (a < b → a ≤ b) ∧ (c < d → c ≤ d) :=
+  ⟨le_of_lt, (fun γ [Preorder γ] (c d : γ) ↦ @le_of_lt γ _ c d) β c d⟩