chore: fix tests

tests/lean/run/alg.lean

@@ -73,4 +73,4 @@ theorem mul_inv_rev [Group α] (a b : α) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
   rw [mul_assoc, ← mul_assoc b, mul_right_inv, one_mul, mul_right_inv]
 
 theorem mul_inv [CommGroup α] (a b : α) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
-  rw [mul_inv_rev, mul_comm]; rfl
+  rw [mul_inv_rev, mul_comm]

tests/lean/scopedunifhint.lean

@@ -40,7 +40,7 @@ open Algebra -- activate unification hints
 
 section Sec1
 
-set_option trace.Meta.debug true
+-- set_option trace.Meta.debug true
 -- This hint is only active in this section
 local unif_hint (s : Magma) (m : Magma) (n : Magma) (β : Type u) (δ : Type v) where
   m.α =?= β