∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] [inst_1 : DecidableEq η]
  {H : (i : η) → Submonoid (f i)} (i : η) (x : (i : η) → f i)
  (motive : x ∈ Submonoid.map (MonoidHom.mulSingle f i) (H i) → Prop)
  (x_1 : x ∈ Submonoid.map (MonoidHom.mulSingle f i) (H i)),
  (∀ (x_2 : f i) (hx : x_2 ∈ ↑(H i)) (H_1 : (MonoidHom.mulSingle f i) x_2 = x), motive ⋯) → motive x_1