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.
@@ -202,7 +210,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
@@ -277,7 +285,9 @@ 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 cfg
+  let mut config := { ← Convert.elabConfig cfg with }
+  if semireducible.isSome then
+    config := { config with postTransparency := .default }
   let patterns := (ps?.getD #[]).toList
   withLocation (expandOptLocation (mkOptionalNode loc?))
     (atLocal := fun fvarId ↦ do