chore(*): tweaks taken from gh-8889 (#10829)

That PR is stale, but contained some trivial changes we should just take.

src/analysis/complex/circle.lean

@@ -102,6 +102,7 @@ subtype.ext $ by simp only [exp_map_circle_apply, submonoid.coe_mul, of_real_add
 
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`, considered as a homomorphism of
 groups. -/
+@[simps]
 def exp_map_circle_hom : ℝ →+ (additive circle) :=
 { to_fun := additive.of_mul ∘ exp_map_circle,
   map_zero' := exp_map_circle_zero,

src/group_theory/quotient_group.lean

@@ -124,10 +124,12 @@ lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
 @[simp, to_additive quotient_add_group.coe_sub]
 lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := by simp [div_eq_mul_inv]
 
-@[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n :=
+@[simp, to_additive quotient_add_group.coe_nsmul]
+lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n :=
 (mk' N).map_pow a n
 
-@[simp] lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n :=
+@[simp, to_additive quotient_add_group.coe_zsmul]
+lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n :=
 (mk' N).map_zpow a n
 
 /-- A group homomorphism `φ : G →* H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a