feat: solve equalities of instances in convert

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -95,7 +95,7 @@ noncomputable abbrev NormalizationMonoid.ofRightInverse {α : Type*} [MonoidWith
   { normUnit a := if a = 0 then 1 else (assoc a).choose
     normUnit_zero := if_pos rfl
     normUnit_one := by
-      nontriviality α; rw [← Units.val_inj]; convert ← (assoc 1).choose_spec <;> simp [out_one]
+      nontriviality α; rw [← Units.val_inj]; convert ← (assoc 1).choose_spec; simp [out_one]
     normUnit_mul_units {a} u ha := by
       simp_rw [Units.mul_left_eq_zero, if_neg ha, eq_inv_mul_iff_mul_eq, ← Units.val_inj]
       rw [Units.val_mul, ← (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha).eq_iff,

Mathlib/Analysis/SpecialFunctions/Log/InvLog.lean

@@ -79,7 +79,7 @@ theorem differentiableOn_inv_log : DifferentiableOn ℝ (fun x ↦ (log x)⁻¹)
 
 theorem inv_log_isLittleO_one : (fun x ↦ (log x)⁻¹) =o[atTop] fun _ ↦ (1 : ℝ) := by
   rw [isLittleO_one_iff]
-  convert tendsto_log_atTop.inv_tendsto_atTop; simp
+  convert tendsto_log_atTop.inv_tendsto_atTop
 
 /- ## Derivative of the iterated logarithm -/
 

Mathlib/Tactic/Convert.lean

@@ -76,6 +76,10 @@ To elaborate config options for `convert`, use `Convert.elabConfig` which choose
 between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags.
 -/
 structure Convert.CheapConfig extends Congr!.Config where
+  /-- Solve instance equality at the pre-step, since there are no cases where doing so at the
+  post-step solves more goals, and doing this earlier means less work for the congruence algorithm.
+  -/
+  preTransparency := .instances
   postTransparency := .reducible
   sameFun := true
 

MathlibTest/Tactic/Convert/Instances.lean

@@ -0,0 +1,34 @@
+import Mathlib.RingTheory.UniqueFactorizationDomain.Nat
+import Mathlib.Tactic.Convert
+
+private axiom test_sorry : ∀ {α}, α
+
+/-! `convert` should not pop up goals about instances. -/
+example {a b c : ℕ} (hab : instLTNat.lt a b) : Nat.instLinearOrder.toLT.lt a c := by
+  convert (preTransparency := .reducible) hab
+  · guard_target =ₛ Nat.instLinearOrder.toLT = instLTNat
+    exact test_sorry
+  · guard_target =ₛ c = b
+    exact test_sorry
+
+#guard_msgs in
+example {a b c : ℕ} (hab : instLTNat.lt a b) : Nat.instLinearOrder.toLT.lt a c := by
+  convert (preTransparency := .instances) hab
+  guard_target =ₛ c = b
+  exact test_sorry
+
+example (q z : Nat) : semigroupDvd.dvd q z := by
+  convert_to (preTransparency := .reducible) q ^ 1 ∣ z
+  · guard_target =ₛ semigroupDvd = Nat.instDvd
+    exact test_sorry
+  · guard_target =ₛ q = q ^ 1
+    exact test_sorry
+  · guard_target =ₛ q ^ 1 ∣ z
+    exact test_sorry
+
+example (q z : Nat) : semigroupDvd.dvd q z := by
+  convert_to (preTransparency := .instances) q ^ 1 ∣ z
+  · guard_target =ₛ q = q ^ 1
+    exact test_sorry
+  · guard_target =ₛ q ^ 1 ∣ z
+    exact test_sorry