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

@@ -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)

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