From 8d418201a646ee86987deb925d8c58c482aaba89 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 16 Sep 2025 18:07:42 +0200
Subject: [PATCH] fix: use with_reducible in deriving_LawfulEq_tactic_step
 (#10417)

This PR changes the automation in `deriving_LawfulEq_tactic_step` to use
`with_reducible` when asserting the shape of the goal using `change`, so
that we do not accidentally unfold `x == x'` calls here. Fixes #10416.
---
 src/Init/LawfulBEqTactics.lean |  7 ++++---
 tests/lean/run/issue10416.lean | 12 ++++++++++++
 2 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/issue10416.lean

diff --git a/src/Init/LawfulBEqTactics.lean b/src/Init/LawfulBEqTactics.lean
index 10208f003f..6e60f5621d 100644
--- a/src/Init/LawfulBEqTactics.lean
+++ b/src/Init/LawfulBEqTactics.lean
@@ -66,7 +66,7 @@ macro_rules
   `(tactic| fail "deriving_LawfulEq_tactic_step failed")
 macro_rules
 | `(tactic| deriving_LawfulEq_tactic_step) =>
-  `(tactic| ( change dite (_ == _) _ _ = true → _
+  `(tactic| ( with_reducible change dite (_ == _) _ _ = true → _
               refine DerivingHelpers.deriving_lawful_beq_helper_dep ?_ ?_
               · solve | apply_assumption | simp | fail "could not discharge eq_of_beq assumption"
               intro h
@@ -75,7 +75,7 @@ macro_rules
     ))
 macro_rules
 | `(tactic| deriving_LawfulEq_tactic_step) =>
-  `(tactic| ( change (_ == _) = true → _
+  `(tactic| ( with_reducible change (_ == _) = true → _
               refine DerivingHelpers.deriving_lawful_beq_helper_nd ?_ ?_
               · solve | apply_assumption | simp | fail "could not discharge eq_of_beq assumption"
               intro h
@@ -83,7 +83,8 @@ macro_rules
     ))
 macro_rules
 | `(tactic| deriving_LawfulEq_tactic_step) =>
-  `(tactic| refine DerivingHelpers.and_true_curry ?_)
+  `(tactic| ( with_reducible change (_ == _ && _) = true → _
+              refine DerivingHelpers.and_true_curry ?_))
 macro_rules
 | `(tactic| deriving_LawfulEq_tactic_step) =>
   `(tactic| rfl)
diff --git a/tests/lean/run/issue10416.lean b/tests/lean/run/issue10416.lean
new file mode 100644
index 0000000000..539a4c3a10
--- /dev/null
+++ b/tests/lean/run/issue10416.lean
@@ -0,0 +1,12 @@
+
+structure Power where
+  x : String
+  k : Nat
+  deriving BEq, ReflBEq, LawfulBEq
+
+inductive Mon where
+  | unit
+  | mult (p : Power)
+  deriving BEq, ReflBEq
+
+deriving instance LawfulBEq for Mon