Instance search for nat pow times out

Stream: mathlib4

[Yakov Pechersky]

This appears in mathlib4#549

import Mathlib.Algebra.Group.Basic

structure Units (α : Type u) [Monoid α] where
  val : α

-- comment out any of the instances below to have `mul_pow'` not time out
instance (priority := low) [Monoid α] : Coe (Units α) α :=
  ⟨Units.val⟩

instance [Monoid α] : Group (Units α) where
  one := ⟨One.one⟩
  mul u₁ u₂ := ⟨u₁.val * u₂.val⟩
  inv := fun u => ⟨u.1⟩
  one_mul u := sorry
  mul_one u := sorry
  mul_left_inv := sorry
  mul_assoc := sorry

instance {α} [CommMonoid α] : CommGroup (Units α) where
  one := ⟨One.one⟩
  mul u₁ u₂ := ⟨u₁.val * u₂.val⟩
  inv := fun u => ⟨u.1⟩
  one_mul u := sorry
  mul_one u := sorry
  mul_left_inv := sorry
  mul_assoc := sorry
  mul_comm := sorry

variable {M : Type _}

theorem mul_pow' [CommMonoid M] (a b : M) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := sorry

[Yakov Pechersky]

I am trying to minimize

[Yakov Pechersky]

Frustratingly, theorem mul_pow'' [CommMonoid M] (a b : M) (n : ℕ) : Pow.pow (a * b) n = Pow.pow a n * Pow.pow b n := sorry is fine.

[Yakov Pechersky]

Similarly, theorem mul_pow'' [CommMonoid M] (a b : M) (n : ℕ) : HPow.hPow (a * b) n = HPow.hPow a n * HPow.hPow b n := sorry is fine