decidable instance not found by typeclass search

Stream: new members

[Eric Wieser]

I'm finding that the instance docs#monoid_hom.monoid_hom.decidable_mem_range (name is corrected in #5378) isn't being found when I need it:

import group_theory.perm.basic
import group_theory.subgroup
import data.fintype.basic

open equiv

/-- `equiv.perm.sum_congr` as a `monoid_hom`. -/
@[simps apply]
def sum_congr_hom (α β : Type*) :
  perm α × perm β →* perm (α ⊕ β) :=
{ to_fun := λ a, a.1.sum_congr a.2,
  map_one' := sorry,
  map_mul' := sorry}

-- fails
example (α β : Type*)
  [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] : decidable_pred (λ x, x ∈ (sum_congr_hom α β).range) :=
infer_instance

-- ok
example (α β : Type*)
  [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] : decidable_pred (λ x, x ∈ (sum_congr_hom α β).range) :=
monoid_hom.monoid_hom.decidable_mem_range _

Why can't it find it?