Commit 2026-06-05 14:31 89ce8bf5

feat(Tactic): convert discharges side goals reducibly (#39928) This PR implements the main behaviour change from #39039: convert now discharges side goals at reducible transparency. convert!, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: convert_to and ac_change). The main trick in this PR is in allowing convert! to have different configuration options than convert, but still allow the user to override those options too. So convert! (postTransparency := .instances) will have transparency set to .instances, not .default. We achieve this by having two new structures that copy Congr!.Config but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an !. I got this trick from Jovan's #38071 which also changes settings in Convert.Config. This PR should be mostly compatible with #38071 and I'd like to get both this one and #38071 in before wrapping up #39039 by replacing unnecessary calls to convert! with convert.