Stay with default reducibility in congr! and only change it in convert

Author: Vierkantor

Mathlib/Tactic/CongrExclamation.lean

@@ -117,8 +117,9 @@ structure Congr!.Config where
   preTransparency : TransparencyMode := TransparencyMode.reducible
   /-- The transparency level to use when trying to close goals after no more congruence lemmas can
   be applied. This includes trying to prove the goal by `rfl` and using the `assumption` tactic.
-  By default this is `.reducible`, which prevents unfolding of most definitions. -/
-  postTransparency : TransparencyMode := TransparencyMode.reducible
+  For backwards compatibility this is set to `.default`, which will be changed soon to `.reducible`.
+  -/
+  postTransparency : TransparencyMode := TransparencyMode.default
   /-- For passes that synthesize a congruence lemma using one side of the equality,
   we run the pass both for the left-hand side and the right-hand side. If `preferLHS` is `true`
   then we start with the left-hand side.

Mathlib/Tactic/Convert.lean

@@ -77,6 +77,14 @@ public meta section
 
 open Lean Meta Elab Tactic
 
+/-- Configuration for the `convert` family of tactics.
+This is `Congr!.Config` with different, less aggressive, defaults.
+-/
+structure Convert.Config extends Congr!.Config where
+  postTransparency := .reducible
+
+declare_config_elab Convert.elabConfig Convert.Config
+
 /--
 Close the goal `g` using `Eq.mp v e`,
 where `v` is a metavariable asserting that the type of `g` and `e` are equal.
@@ -201,7 +209,7 @@ def elabTermForConvert (term : Syntax) (expectedType? : Option Expr) :
 elab_rules : tactic
 | `(tactic| convert%$tk $[!%$semired]? $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
   withMainContext do
-    let baseConfig ← Congr!.elabConfig (mkOptionalNode cfg)
+    let baseConfig := { ← Convert.elabConfig cfg with }
     let mut config := baseConfig
     if semired.isSome then
       config := { config with
@@ -276,7 +284,7 @@ elab_rules : tactic
 | `(tactic| convert_to $[!%$semireducible]? $cfg $[←%$sym]? $newType $[using $n]?
     $[with $ps?*]? $[$loc?:location]?) => do
   let n : ℕ := n |>.map (·.getNat) |>.getD 1
-  let config ← Congr!.elabConfig (mkOptionalNode cfg)
+  let config := { ← Convert.elabConfig cfg with }
   let patterns := (ps?.getD #[]).toList
   withLocation (expandOptLocation (mkOptionalNode loc?))
     (atLocal := fun fvarId ↦ do
@@ -321,7 +329,9 @@ syntax (name := acChange) "ac_change " term (" using " num)? : tactic
 syntax (name := acChange!) "ac_change! " term (" using " num)? : tactic
 
 macro_rules
-| `(tactic| ac_change $t $[using $n]?) => `(tactic| convert_to $t:term $[using $n]? <;> try ac_rfl)
-| `(tactic| ac_change! $t $[using $n]?) => `(tactic| convert_to! $t:term $[using $n]? <;> try ac_rfl)
+| `(tactic| ac_change $t $[using $n]?) =>
+    `(tactic| convert_to $t:term $[using $n]? <;> try ac_rfl)
+| `(tactic| ac_change! $t $[using $n]?) =>
+    `(tactic| convert_to! $t:term $[using $n]? <;> try ac_rfl)
 
 end Mathlib.Tactic